{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:24:42Z","timestamp":1725456282205},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540629207"},{"type":"electronic","value":"9783540690467"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027417","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:34:36Z","timestamp":1132641276000},"page":"231-245","source":"Crossref","is-referenced-by-count":0,"title":["On quasitautologies"],"prefix":"10.1007","author":[{"given":"J\u00e1n","family":"Komara","sequence":"first","affiliation":[]},{"given":"Paul J.","family":"Voda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"J. Barwise. An introduction to first-order logic. In J. Barwise, editor, Handbook of Mathematical Logic, pages 5\u201346. North-Holland, 1977.","DOI":"10.1016\/S0049-237X(08)71097-8"},{"key":"17_CR2","unstructured":"G. S. Boolos and R. C. Jeffrey. Computability and Logic. Cambridge University Press, second edition, 1980."},{"key":"17_CR3","unstructured":"S. R. Buss. An introduction to proof theory. To appear in Handbook of Proof Theory (ed. S. Buss), 1996."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak's decision procedure for combinations of theories. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of CADE-13, number 1104 in LNAI, pages 463\u2013477. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_107"},{"key":"17_CR5","unstructured":"A. Degtyarev, Y. Gurevich, and A. Voronkov. Herbrand's theorem and equational reasoning: Problems and solutions. In Bulletin of the European Association for Theoretical Computer Science, volume 60, October 1996. The \u201dLogic in Computer Science\u201d column."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995.","DOI":"10.1007\/3-540-61377-3_38"},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"A. Degtyarev and A. Voronkov. The undecidability of simultaneous rigid E-unification. Theoretical Computer Science, 166:291\u2013300, 1996.","journal-title":"Theoretical Computer Science"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"P. H\u00e1jek and P. Pudl\u00e1k. Metamathematics of First-Order Arithmetic. Springer Verlag, 1993.","DOI":"10.1007\/978-3-662-22156-3"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"J. Komara and P. J. Voda. Syntactic reduction of predicate tableaux to propositional tableaux. In P. Baumgartner, R. Haehnle, and J. Posegga, editors, Proceedings of TABLEAUX '95, number 918 in LNAI, pages 231\u2013246. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_39"},{"key":"17_CR10","volume-title":"Technical report","author":"J. Komara","year":"1996","unstructured":"J. Komara and P. J. Voda. On Skolem axioms. Technical report, Institute of Informatics, Faculty of Mathematics and Physics, Comenius University, Bratislava, November 1996."},{"issue":"2","key":"17_CR11","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"17_CR12","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356\u2013364, 1980.","journal-title":"Journal of the ACM"},{"key":"17_CR13","unstructured":"J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967."},{"issue":"7","key":"17_CR14","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. E. Shostak","year":"1978","unstructured":"R. E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583\u2013585, July 1978.","journal-title":"Communications of the ACM"},{"issue":"1","key":"17_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"R. Smullyan. First Order Logic. Springer Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"17_CR17","unstructured":"G. Takeuti. Proof Theory. North-Holland, 1975."},{"key":"17_CR18","volume-title":"Technical report","author":"P. J. Voda","year":"1995","unstructured":"P. J. Voda and J. Komara. On Herbrand skeletons. Technical report, Institute of Informatics, Faculty of Mathematics and Physics, Comenius University, Bratislava, July 1995. Revised January 1996. Submitted for publication."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027417","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:46:17Z","timestamp":1586573177000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027417"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540629207","9783540690467"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0027417","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}