{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:09Z","timestamp":1725456069595},"publisher-location":"Berlin\/Heidelberg","reference-count":55,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055789X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023767","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T10:11:10Z","timestamp":1132395070000},"page":"184-200","source":"Crossref","is-referenced-by-count":7,"title":["Logical inference and polyhedral projection"],"prefix":"10.1007","author":[{"given":"J. N.","family":"Hooker","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Andersen, K. A., and J. N. Hooker, Bayesian logic, to appear in Decision Support Systems."},{"key":"14_CR2","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0020-0190(87)90200-6","volume":"24","author":"V. Arvind","year":"1987","unstructured":"Arvind, V. and S. Biswas, An O(n 2) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences, Information Processing Letters 24 (1987) 67\u201369.","journal-title":"Information Processing Letters"},{"key":"14_CR3","unstructured":"Billionnet, A., and A. Sutter, An efficient algorithm for the 3-satisfiability problem, Research Report 89-13, Centre d'\u00e9tudes et de recherche en informatique, 292 rue Saint-Martin, 75141 Paris Cedex 03, 1989."},{"key":"14_CR4","unstructured":"E. Boros, P. Hammer and J. N. Hooker, Boolean regression, working paper 1991-30, Graduate School of Industrial Administration, Carnegie Mellon University, Pittsburgh, PA 15213 USA."},{"key":"14_CR5","unstructured":"E. Boros, P. L. Hammer, and J. N. Hooker, Predicting cause-effect relationships from incomplete discrete observations, working paper 1991-22, Graduate School of Industrial Administration, Carnegie Mellon University, Pittsburgh, PA 15213 USA."},{"key":"14_CR6","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1016\/0305-0548(86)90056-0","volume":"13","author":"C. Blair","year":"1988","unstructured":"Blair, C., R. G. Jeroslow, and J. K. Lowe, Some results and experiments in programming techniques for propositional logic, Computers and Operations Research 13 (1988) 633\u2013645.","journal-title":"Computers and Operations Research"},{"key":"14_CR7","unstructured":"Chandru, V., and J. N. Hooker, Logical inference: A mathematical programming perspective, in S. T. Kumara, R. L. Kashyap, and A. L. Soyster, eds., Artificial Intelligence: Manufacturing Theory and Practice, Institute of Industrial Engineers (1988) 97\u2013120."},{"key":"14_CR8","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/102782.102789","volume":"38","author":"V. Chandru","year":"1991","unstructured":"Chandru, V., and J. N. Hooker, Extended Horn sets in propositional logic, Journal of the ACM 38 (1991) 203\u2013221.","journal-title":"Journal of the ACM"},{"key":"14_CR9","unstructured":"Chandru, V., and J. N. Hooker, Optimization Methods for Logical Inference, Wiley, to appear."},{"key":"14_CR10","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0012-365X(73)90167-2","volume":"4","author":"V. Chv\u00e1tal","year":"1973","unstructured":"Chv\u00e1tal, V., Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305\u2013337.","journal-title":"Discrete Mathematics"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Cook, S. A., The complexity of theorem-proving procedures, Proceedings of the Third Annual ACM Symposium on the Theory of Computing (1971) 151\u2013158.","DOI":"10.1145\/800157.805047"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Dantzig, G. B., Linear Programming and Extensions, Princeton University Press (1963).","DOI":"10.7249\/R366"},{"key":"14_CR13","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., and H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7 (1960) 201\u2013215.","journal-title":"Journal of the ACM"},{"key":"14_CR14","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W. F. Dowling","year":"1984","unstructured":"Dowling, W. F., and J. H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, Journal of Logic Programming 1 (1984) 267\u2013284.","journal-title":"Journal of Logic Programming"},{"key":"14_CR15","volume-title":"Working paper","author":"G. Gallo","year":"1990","unstructured":"G. Gallo and G. Rago, A hypergraph approach to logical inference for datalog formulae, working paper, Dip. di Informatica, University of Pisa, Italy (September 1990)."},{"key":"14_CR16","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0020-0190(88)90113-5","volume":"29","author":"G. Gallo","year":"1988","unstructured":"Gallo, G., and M. G. Scutella, Polynomially soluble satisfiability problems, Information Processing Letters 29 (1988) 221\u2013227.","journal-title":"Information Processing Letters"},{"key":"14_CR17","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","volume":"7","author":"G. Gallo","year":"1989","unstructured":"Gallo, G., and G. Urbani, Algorithms for testing the satisfiability of propositional formulae, Journal of Logic Programming 7 (1989) 45\u201361.","journal-title":"Journal of Logic Programming"},{"key":"14_CR18","volume-title":"Logical Foundations of Artificial Intelligence","author":"M. R. Genesereth","year":"1987","unstructured":"Genesereth, M. R., and N. J. Nilsson, Logical Foundations of Artificial Intelligence, Morgan Kaufmann (Los Altos, CA, 1987)."},{"key":"14_CR19","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/BF02186367","volume":"12","author":"F. Glover","year":"1988","unstructured":"Glover, F., and H. J. Greenberg, Logical testing for rule-based management, Annals of Operations Research 12 (1988) 199\u2013215.","journal-title":"Annals of Operations Research"},{"key":"14_CR20","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A., The intractability of resolution, Theoretical Computer Science 39 (1985) 297\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"14_CR21","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/0020-0190(76)90079-X","volume":"5","author":"P. Hansen","year":"1976","unstructured":"Hansen, P., A cascade algorithm for the logical closure of a set of binary relations, Information Processing Letters 5 (1976) 50\u201355.","journal-title":"Information Processing Letters"},{"key":"14_CR22","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF01580586","volume":"34","author":"P. Hansen","year":"1986","unstructured":"Hansen, P., B. Jaumard and M. Minoux, A linear expected-time algorithm for deriving all logical conclusions implied by a set of boolean inequalities, Mathematical Programming 34 (1986) 223\u2013231.","journal-title":"Mathematical Programming"},{"key":"14_CR23","volume-title":"Working paper 1991-27","author":"F. Harche","year":"1991","unstructured":"Harche, F., J. N. Hooker and G. L. Thompson, A computational study of satisfiability algorithms for propositional logic, working paper 1991-27, Graduate School of Industrial Administration, Carnegie Mellon University, Pittsburgh, PA 15213 USA, 1991."},{"key":"14_CR24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","volume":"7","author":"J. N. Hooker","year":"1988","unstructured":"Hooker, J. N., Resolution vs. cutting plane solution of inference problems: Some omputational experience, Operations Research Letters 7 (1988) 1\u20137.","journal-title":"Operations Research Letters"},{"key":"14_CR25","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0167-9236(88)90097-8","volume":"4","author":"J. N. Hooker","year":"1988","unstructured":"Hooker, J. N., A quantitative approach to logical inference, Decision Support Systems 4 (1988) 45\u201369.","journal-title":"Decision Support Systems"},{"key":"14_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","volume":"7","author":"J. N. Hooker","year":"1988","unstructured":"Hooker, J. N., Resolution vs. cutting plane solution of inference problems: some computational experience, Operations Research Letters 7 (1988) 1\u20137.","journal-title":"Operations Research Letters"},{"key":"14_CR27","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF02186368","volume":"12","author":"J. N. Hooker","year":"1988","unstructured":"Hooker, J. N., Generalized resolution and cutting planes, Annals of Operations Research 12 (1988) 217\u2013239.","journal-title":"Annals of Operations Research"},{"key":"14_CR28","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1287\/ijoc.1.3.137","volume":"1","author":"J. N. Hooker","year":"1989","unstructured":"Hooker, J. N., Input proofs and rank one cutting planes, ORSA Journal on Computing 1 (1989) 137\u2013145.","journal-title":"ORSA Journal on Computing"},{"key":"14_CR29","unstructured":"Hooker, J. N., Generalized resolution for 0\u20131 linear inequalities, to appear in Annals of Mathematics and AI."},{"key":"14_CR30","volume-title":"Working paper 1991-11","author":"J. N. Hooker","year":"1991","unstructured":"Hooker, J. N., New methods for inference in first-order predicate logic, working paper 1991-11, Graduate School of Industrial Administration, Carnegie Mellon University, Pittsburgh, PA 15213 USA, 1991."},{"key":"14_CR31","unstructured":"Hooker, J. N. and C. Fedjki, Branch-and-cut solution of inference problems in propositional logic, to appear in Annals of Mathematics and AI."},{"key":"14_CR32","volume-title":"Working paper 1991-29","author":"J. N. Hooker","year":"1988","unstructured":"Hooker, J. N., and H. Yan, Verifying logic circuits by Benders decomposition, working paper 1991-29, Graduate School of Industrial Administration, Carnegie Mellon University, Pittsburgh, USA, August 1988."},{"key":"14_CR33","unstructured":"Jaumard, B., P. Hansen and M. P. Araga\u00f6, Column generation methods for probabilistic logic, to appear in ORSA Journal on Computing."},{"key":"14_CR34","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0167-9236(88)90128-5","volume":"4","author":"R. E. Jeroslow","year":"1988","unstructured":"Jeroslow, R. E., Computation-oriented reductions of predicate to propositional logic, Decision Support Systems 4 (1988) 183\u2013197.","journal-title":"Decision Support Systems"},{"key":"14_CR35","first-page":"167","volume":"1","author":"R. E. Jeroslow","year":"1990","unstructured":"Jeroslow, R. E., and J. Wang, Solving propositional satisfiability problems, Annals of Mathematics and AI 1 (1990) 167\u2013187.","journal-title":"Annals of Mathematics and AI"},{"key":"14_CR36","first-page":"333","volume-title":"Integer Programming and Combinatorial Optimization","author":"A. P. Kamath","year":"1990","unstructured":"Kamath, A. P., N. K. Karmarkar, K. G. Ramakrishnan, and M. G. C. Resende, Computational experience with an interior point algorithm on the satisfiability problem, in R. Kannan and W. R. Pulleyblank, eds., Integer Programming and Combinatorial Optimization, University of Waterloo Press (Waterloo, Ont., 1990) 333\u2013349."},{"key":"14_CR37","volume-title":"A continuous aproach to inductive inference, manuscript","author":"A. P. Kamath","year":"1991","unstructured":"Kamath, A. P., N. K. Karmarkar, K. G. Ramakrishnan, and M. G. C. Resende, A continuous aproach to inductive inference, manuscript, AT&T Bell Labs, Murray Hil, NJ 07974 USA, 1991."},{"key":"14_CR38","unstructured":"Kavvadias, D., and C. H. Papadimitriou, A linear programming approach to reasoning about probabilities, to appear in Annals of Mathematics and Artificial Intelligence."},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Karp, R. M., Reducibility among combinatorial problems, in R. E. Miller and J. W. Thatcher, eds., Complexity of Computer Computations, Plenum Press (1972) 85\u2013103.","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"14_CR40","unstructured":"Loveland, D. W., Automated Theorem Proving: A Logical Basis, North-Holland (1978)."},{"key":"14_CR41","volume-title":"Working paper","author":"I. Mitterreiter","year":"1991","unstructured":"Mitterreiter, I., and F. J. Radermacher, Experiments on the running time behavior of some algorithms solving propositional logic problems, working paper, Forschungsinstitut f\u00fcr anwendungsorientierte Wissensverarbeitung, Ulm, Germany (1991)."},{"key":"14_CR42","unstructured":"Patrizi, G., The equivalence of an LCP to a parametric linear program with a scalar parameter, to appear in European Journal of Operational Research."},{"key":"14_CR43","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1080\/00029890.1952.11988183","volume":"59","author":"W. V. Quine","year":"1952","unstructured":"Quine, W. V., The problem of simplifying truth functions, American Mathematical Monthly 59 (1952) 521\u2013531.","journal-title":"American Mathematical Monthly"},{"key":"14_CR44","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1080\/00029890.1955.11988710","volume":"62","author":"W. V. Quine","year":"1955","unstructured":"Quine, W. V., A way to simplify truth functions, American Mathematical Monthly 62 (1955) 627\u2013631.","journal-title":"American Mathematical Monthly"},{"key":"14_CR45","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A., A machine-oriented logic based on the resolution principle, Journal of the ACM 12 (1965) 23\u201341.","journal-title":"Journal of the ACM"},{"key":"14_CR46","volume-title":"Technical report","author":"C. Spera","year":"1990","unstructured":"Spera, C., Computational results for solving large general satisfiability problems, technical report, Centro di Calcolo Elettronico, Universit\u00e0 degli Studi di Siena, Italy, 1990."},{"key":"14_CR47","volume-title":"Generating logical expressions from positive and negative examples via a branch-and-bound approach, manuscript","author":"E. Triantaphylou","year":"1991","unstructured":"Triantaphylou, E., A. L. Soyster, and S. R. T. Kumara, Generating logical expressions from positive and negative examples via a branch-and-bound approach, manuscript, Industrial and Management Systems Engineering, Pennsylvania State University, University Park, PA 16802 USA, 1991."},{"key":"14_CR48","volume-title":"Technical report UTDCS-34-90","author":"K. Truemper","year":"1990","unstructured":"Truemper, K., Polynomial theorem proving: I. Central matrices, technical report UTDCS-34-90, Computer Science Dept., University of Texas at Dallas, Richardson, TX 75083-0688 USA (1990)."},{"key":"14_CR49","volume-title":"Technical report FAW-TR-90003","author":"K. Truemper","year":"1990","unstructured":"Truemper, K., and F. J. Radermacher, Analyse der Leistungsf\u00e4higkeit eines neuen Systems zur Auswertung aussagenlogisher Probleme, technical report FAW-TR-90003, Forschungsinstitut f\u00fcr anwendungsorientierte Wissensverarbeitung, Ulm, Germany (1990)."},{"key":"14_CR50","doi-asserted-by":"crossref","unstructured":"Tseitin, G. S., On the complexity of derivations in the propositional calculus, in A. O. Slisenko, ed., Structures in Constructive Mathematics and Mathematical Logic, Part II (translated from Russian, 1968) 115\u2013125.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"14_CR51","volume-title":"Working paper","author":"J. Wang","year":"1989","unstructured":"Wang, J., and J. Vande Vate, Question-asking strategies for Horn clause systems, working paper, Georgia Institute of Technology, Atlanta, GA, 1989."},{"key":"14_CR52","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1016\/0097-3165(76)90055-8","volume":"21","author":"H. P. Williams","year":"1976","unstructured":"Williams, H. P., Fourier-Motzkin elimination extension to integer programming problems, Journal of Combinatorial Theory 21 (1976) 118\u2013123.","journal-title":"Journal of Combinatorial Theory"},{"key":"14_CR53","unstructured":"Williams, H. P., Model Building in Mathematical Programming, Wiley (1985)."},{"key":"14_CR54","first-page":"81","volume":"2","author":"H. P. Williams","year":"1987","unstructured":"Williams, H. P., Linear and integer programming applied to the propositional calculus, International Journal of Systems Research and Information Science 2 (1987) 81\u2013100.","journal-title":"International Journal of Systems Research and Information Science"},{"key":"14_CR55","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(83)80027-8","volume":"59","author":"S. Yamasaki","year":"1983","unstructured":"Yamasaki, S. and S. Doshita, The satisfiability problem for a class consisting of Horn sentences and some non-Horn sentences in propositional logic, Information and Control 59 (1983) 1\u201312.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0023767","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T01:50:35Z","timestamp":1586569835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023767"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055789X"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/bfb0023767","relation":{},"subject":[]}}