{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171711},"publisher-location":"Berlin\/Heidelberg","reference-count":12,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012857","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"563-572","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning about systems of linear inequalities"],"prefix":"10.1007","author":[{"given":"Thomas","family":"K\u00e4ufl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","unstructured":"W.W. Bledsoe: A New Method for Proving Certain Presburger Formulas 4th Int. Joint Conference on Artificial Intelligence, Tiblisi, pp.15\u201321: 1975"},{"key":"38_CR2","unstructured":"A. Bundy: The Computer Modelling of Mathematical Reasoning London: 1983; Academic Press"},{"key":"38_CR3","unstructured":"D.C. Cooper: Theorem Proving in Arithmetic without Multiplication Machine Intelligence 8, B. Meltzer and D. Michie, eds., New York: 1972"},{"key":"38_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-87362-1","volume-title":"Lineare Programmierung und Erweiterungen Berlin","author":"G.B. Dantzig","year":"1966","unstructured":"G.B. Dantzig: Lineare Programmierung und Erweiterungen Berlin, Heidelberg, New York: 1966"},{"key":"38_CR5","unstructured":"D.B. Judin, E.G. Golstein: Lineare Optimierung I Berlin: 1986"},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"Th. K\u00e4ufl: The Simplifier of the Program Verifier \"Tatzelwurm\" \u00d6sterreichische Artificial Intelligence-Tagung 1985 Informatik-Fachberichte; Berlin, Heidelberg, New York: 1985; Springer","DOI":"10.1007\/978-3-642-46552-9_21"},{"key":"38_CR7","doi-asserted-by":"crossref","unstructured":"Th. K\u00e4ufl: Program Verifier \"Tatzelwurm\": Reasoning about Systems of Linear Inequalities 8th International Conference on Automated Deduction 1986 Berlin, Heidelberg, New York: 1986; Springer","DOI":"10.1007\/3-540-16780-3_98"},{"key":"38_CR8","unstructured":"Th. K\u00e4ufl: Reasoning about Systems of Linear Inequalities Technical Report 16\/87, University of Karlsruhe, Institut f\u00fcr Logik, Komplexit\u00e4t und Deduktionssysteme: 1987"},{"key":"38_CR9","unstructured":"J.C. King: A Program Verifier Ph.D. Thesis, Carnegie Mellon University, Pittsburgh: 1969"},{"key":"38_CR10","doi-asserted-by":"crossref","unstructured":"G. Kreisel, J.-L. Krivine: Modelltheorie Berlin, Heidelberg, New York: 1972","DOI":"10.1007\/978-3-642-65302-5"},{"key":"38_CR11","unstructured":"T.S. Motzkin: Beitr\u00e4ge zur Theorie der linearen Ungleichungen Dissertation Z\u00fcrich: 1936"},{"issue":"4","key":"38_CR12","first-page":"529","volume":"24","author":"R. Shostak","year":"1977","unstructured":"R. Shostak: On the SUP-INF Method for Proving Presburger Formulas JACM 24\/4, pp. 529\u2013543: 1977","journal-title":"On the SUP-INF Method for Proving Presburger Formulas JACM"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012857","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:21Z","timestamp":1586579061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012857"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0012857","relation":{},"subject":[]}}