{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:49:45Z","timestamp":1725662985008},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540095262"},{"type":"electronic","value":"9783540350880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1979]]},"DOI":"10.1007\/3-540-09526-8_12","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:46:50Z","timestamp":1330188410000},"page":"160-169","source":"Crossref","is-referenced-by-count":3,"title":["Axioms or algorithms"],"prefix":"10.1007","author":[{"given":"Vaughan R.","family":"Pratt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,26]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Constable, R.L., On the Theory of Programming Logics, Proc. 9th Ann. ACM Symp. on Theory of Computing, 269\u2013285, Boulder, Col., May 1977.","DOI":"10.1145\/800105.803417"},{"key":"12_CR2","unstructured":"Constable, R.L. and M.J. O'Donnell, A Programming Logic, Winthrop Publishers, Inc., 17 Dunster St., Cambridge, Mass., 1978."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Downey, P., H. Samet, and R. Sethi, Off-line and On-line Algorithms for Deducing Equalities, Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, 158\u2013170, Tucson, Arizona, Jan. 1978.","DOI":"10.1145\/512760.512777"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Lewis, H., Complexity of Solvable Cases of the Decision Problem for the Predicate Calculus, 19th Annual Symposium on Foundations of Computer Science, Ann Arbor, Michigan, Oct., 1978.","DOI":"10.1109\/SFCS.1978.9"},{"key":"12_CR5","unstructured":"Litvintchouk, S.D. and V.R. Pratt, A Proof-checker for Dynamic Logic, Proc. 5th Int. Joint Conf. on AI, 552\u2013558, Boston, Aug. 1977."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Nelson, G. and D.C. Oppen., A Simplifier Based on Efficient Decision Algorithms, Proceedings of the Fifth Annual ACM Symposium on Principles of Programming Languages, 141\u2013150, Tucson, Arizona, Jan. 1978.","DOI":"10.1145\/512760.512775"},{"key":"12_CR7","unstructured":"Oppen, D.C., Complexity of Combinations of Quantifier-Free Theories, Proceedings of the Fourth Workshop on Automated Deduction, 67\u201372, Austin, Texas, Feb. 1979."},{"key":"12_CR8","unstructured":"Pratt, V.R., A Near Optimal Method for Reasoning About Action, MIT\/LCS\/TM-113, M.I.T., Sept. 1978."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Shostak, R., Deciding Linear Inequalities by Computing Loop Residues, Proceedings of the Fourth Workshop on Automated Deduction, 81\u201389, Austin, Texas, Feb. 1979.","DOI":"10.21236\/ADA055868"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1979"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-09526-8_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:01:23Z","timestamp":1605643283000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-09526-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979]]},"ISBN":["9783540095262","9783540350880"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-09526-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1979]]}}}