{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:37:09Z","timestamp":1758274629686},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429579"},{"type":"electronic","value":"9783540456537"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45653-8_10","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T04:57:30Z","timestamp":1181365050000},"page":"142-156","source":"Crossref","is-referenced-by-count":21,"title":["Proof and Model Generation with Disconnection Tableaux"],"prefix":"10.1007","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[]},{"given":"Gernot","family":"Stenz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,11,20]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Peter Baumgartner. FDPLL-A First-Order Davis-Putnam-Logeman-Loveland Procedure. InDavid McAllester, editor, CADE-17-The 17thInternational Conference on Automated Deduction, volume 1831 of Lecture Notes in Artificial Intelligence, pages 200\u2013219. Springer, 2000.","DOI":"10.1007\/10721959_16"},{"key":"10_CR2","first-page":"353","volume-title":"Automated Deduction: A Basis for Applications. Volume I, Foundations:Calculi and Methods","author":"L. Bachmair","year":"1998","unstructured":"Leo Bachmair and Harald Ganzinger. Equational reasoning in saturation based theorem proving. In Wolfgang Bibel and Peter H. Schmidt, editors, Automated Deduction: A Basis for Applications. Volume I, Foundations:Calculi and Methods, pages 353\u2013398. Kluwer Academic Publishers, Dordrecht,1998."},{"key":"10_CR3","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Proceedings of the 5th International Workshop on Theorem Proving with analytic Tableaux and Related Methods (TABLEAUX)","author":"J.-P. Billon","year":"1996","unstructured":"Jean-Paul Billon. The disconnection method: a confluent integration of unification in the analytic framework. In P. Migliolo, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings of the 5th International Workshop on Theorem Proving with analytic Tableaux and Related Methods (TABLEAUX), volume 1071 of LNAI pages 110\u2013126, Berlin, May 15\u201317 1996. Springer."},{"key":"10_CR4","volume-title":"The Decision Problem: Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"Burton Dreben and Warren D. Goldfarb. The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley Publishing Company, Reading, MA, 1979."},{"issue":"3","key":"10_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Martin Davis and Hilary Putman. A computing procedure for quantification theory. Journal of the ACM, 7(3):201\u2013215, July 1960.","journal-title":"Journal of the ACM"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, second edition, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"issue":"1\u20132","key":"10_CR7","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0304-3975(96)00052-7","volume":"176","author":"M. Hermann","year":"1997","unstructured":"Miki Hermann and Roman Galbav\u00ed. Unification of infinite sets of terms schematized by primal grammars. Theoretical Computer Science, 176(1\u20132):111\u2013158, April 1997.","journal-title":"Theoretical Computer Science"},{"key":"10_CR8","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-94-017-1754-0_3","volume-title":"Handbook of Tableau Methods","author":"R. Letz","year":"1999","unstructured":"Reinhold Letz. First-Order Tableaux Methods. In M. D\u2019Agostino, D. Gabbay, R. H\u00e4hnle, and J. Posegga, editors, Handbook of Tableau Methods, pages 125\u2013196. Kluwer, Dordrecht, 1999."},{"issue":"3","key":"10_CR9","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlledin tegration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13(3):297\u2013337,December 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR10","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/3-540-45744-5_30","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001)","author":"R. Letz","year":"2001","unstructured":"Reinhold Letz and Gernot Stenz. DCTP: A Disconnection Calculus Theorem Prover. In Rajeev Gor\u00e9, Alexander Leitsch, and Tobias Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy, volume 2083 of LNAI, pages 381\u2013385. Springer, Berlin, June 2001."},{"key":"10_CR11","volume-title":"A Davis-Putnam program andits application to finite first-order model search: quasigroup existence problems","author":"W. McCune","year":"1994","unstructured":"William McCune. A Davis-Putnam program andits application to finite first-order model search: quasigroup existence problems. Technical Memorandum ANL\/MCS-TM-194, Argonne National Laboratories, IL\/USA, September 1994."},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/jigpal\/7.2.217","volume":"7","author":"N. Peltier","year":"1999","unstructured":"Nicolas Peltier. Pruning the search space andextracting more models in tableaux. Logic Journal of the IGPL, 7(2):217\u2013251, 1999.","journal-title":"Logic Journal of the IGPL"},{"issue":"1","key":"10_CR13","first-page":"25","volume":"9","author":"David. Plaisted A","year":"1992","unstructured":"David A. Plaisted and Shie-Jue Lee. Eliminating duplication with the hyperlinking strategy. Journal of Automated Reasoning, 9(1):25\u201342, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/BFb0013079","volume-title":"Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR\u201992)","author":"G. Salzer","year":"1992","unstructured":"Gernot Salzer. The unification of infinite sets of terms andits applications. InA. Voronkov editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR\u201992), volume 624 of LNAI, pages 409\u2013420, St. Petersburg, Russia, July 1992. Springer Verlag."},{"key":"10_CR15","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Proceedings of the 12th International Conference on Automated Deduction","author":"J. Slaney","year":"1994","unstructured":"John Slaney. FINDER: Finite domain enumerator. In Alan Bundy, editor,Proceedings of the 12th International Conference on Automated Deduction, volume 814 of LNAI, pages 798\u2013801, Berlin, June\/July 1994. Springer."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Raymond Smullyan. First-Order Logic. Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45653-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T09:44:33Z","timestamp":1683884673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45653-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429579","9783540456537"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45653-8_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}