{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:29Z","timestamp":1725664709959},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:36:02Z","timestamp":1330292162000},"page":"52-63","source":"Crossref","is-referenced-by-count":1,"title":["Deduction by combining semantic tableaux and integer programming"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Dantzig, George B. 1963. Linear Programming and Extensions. Princeton University Press.","DOI":"10.7249\/R366"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Fitting, Melvin C. 1996. First-Order Logic and Automated Theorem Proving. 2nd edn. Springer.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"4_CR3","unstructured":"H\u00e4hnle, Reiner. 1994a. Automated Deduction in Multiple-valued Logics. International Series of Monographs on Computer Science, vol. 10. Oxford University Press."},{"issue":"34","key":"4_CR4","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/BF01530787","volume":"12","author":"R. H\u00e4hnle","year":"1994","unstructured":"H\u00e4hnle, Reiner. 1994b. Many-Valued Logic and Mixed Integer Programming. Annals of Mathematics and Artificial Intelligence, 12(3,4), 231\u2013264.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, Reiner, & Ibens, Ortrun. 1994. Improving Temporal Logic Tableaux Using Integer Constraints. Pages 535\u2013539 of: Proceedings, International Conference on Temporal Logic, Bonn, Germany. Springer LNCS 827.","DOI":"10.1007\/BFb0014007"},{"issue":"2","key":"4_CR6","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\u00e4hnle","year":"1994","unstructured":"H\u00e4hnle, Reiner, & Schmitt, Peter H. 1994. The liberalized \u03b4-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2), 211\u2013222.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Hooker, John N. 1993. New Methods for Computing Inferences in First Order Logic. Annals of Operations Research, 43.","DOI":"10.1007\/BF02027814"},{"issue":"1\u20133","key":"4_CR8","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0168-0072(94)90010-8","volume":"67","author":"V. Kagan","year":"1994","unstructured":"Kagan, Vadim, Nerode, Anil, & Subrahmanian, V. S. 1994. Computing Definite Logic Programs by Partial Instantiation. Annals of Pure and Applied Logic, 67(1\u20133), 161\u2013182.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"4_CR9","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, Reinhold, Schumann, Johann, Bayerl, Stephan, & Bibel, Wolf-Gang. 1992. Setheo: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2), 183\u2013212.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR10","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"Plaisted, David A., & Greenbaum, Steven. 1986. A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 2, 293\u2013304.","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR11","unstructured":"Rago, Gabriella. 1994 (Mar.). Optimization, Hypergraphs and Logical Inference. Ph.D. thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa. Available as Tech Report TD-4\/94."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:05:47Z","timestamp":1605647147000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}