{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:34Z","timestamp":1725663334294},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_128","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:46:48Z","timestamp":1330206408000},"page":"657-658","source":"Crossref","is-referenced-by-count":2,"title":["The theorem prover of the program verifier Tatzelwurm"],"prefix":"10.1007","author":[{"given":"Thomas","family":"K\u00e4ufl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Zabel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"54_CR1","unstructured":"W. Ackermann: Solvable Cases of the Decision Problem Studies in Logic and the Foundations of Mathematics, Amsterdam: 1954"},{"key":"54_CR2","unstructured":"Th. K\u00e4ufl: Vereinfachung logischer Formeln in einem Vorbeweiser Dissertation, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe: 1988"},{"key":"54_CR3","series-title":"Lecture Notes on Computer Science","volume-title":"Reasoning About Systems of Linear Inequalities 9th International Conference on Automated Deduction","author":"T. K\u00e4ufl","year":"1988","unstructured":"Th. K\u00e4ufl: Reasoning About Systems of Linear Inequalities 9th International Conference on Automated Deduction, Lecture Notes on Computer Science; Berlin, Heidelberg, New York: 1988; Springer"},{"key":"54_CR4","unstructured":"Th. K\u00e4ufl: Simplification and Decision of Linear Inequalities over the Integers Technical Report 9\/88, University of Karlsruhe, Institut f\u00fcr Logik, Komplexit\u00e4t und Deduktionssysteme: 1988"},{"key":"54_CR5","unstructured":"Th. K\u00e4ufl: Cooperation of Decision Procedures in a Tableau-Based Theorem Prover Technical Report 16\/89, University of Karlsruhe, Institut f\u00fcr Logik, Komplexit\u00e4t und Deduktionssysteme: 1989"},{"key":"54_CR6","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"C.G. Nelson","year":"1979","unstructured":"C.G. Nelson, D.C. Oppen: Simplification by Cooperating Decision Procedures, ACM TOPLAS 1, pp. 245\u2013257: 1979","journal-title":"ACM TOPLAS"},{"key":"54_CR7","doi-asserted-by":"crossref","unstructured":"K. Sch\u00fctte: Proof Theory, Berlin, Heidelberg, New York: 1977","DOI":"10.1007\/978-3-642-66473-1"},{"key":"54_CR8","doi-asserted-by":"crossref","unstructured":"R.M. Smullyan: First-Order Logic Berlin, Heidelberg, New York: 1968","DOI":"10.1007\/978-3-642-86718-7"}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_128.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:33Z","timestamp":1605648333000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_128","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}