{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:37Z","timestamp":1725488617047},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_4","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:02:03Z","timestamp":1186171323000},"page":"62-79","source":"Crossref","is-referenced-by-count":1,"title":["Decision Procedures and Model Building or How to Improve Logical Information in Automated Deduction"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Leitsch","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"4_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory, KGC\u201993","author":"L. Bachmair","year":"1993","unstructured":"Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Computational Logic and Proof Theory, KGC\u201993, pages 83\u201396. Springer, LNCS 713, 1993."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"P. Baumgartner, U. Furbach, and I. Niemela. Hyper-tableaux. In Logics in AI, JELIA\u201996. Springer, 1996.","DOI":"10.1007\/3-540-61630-6_1"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ch. Bourely, R. Caferra, and N. Peltier. A method for building models automatically. Experiments with an extension of Otter. In Proceedings of CADE-12, pages 72\u201386. Springer, 1994. LNAI 814.","DOI":"10.1007\/3-540-58156-1_6"},{"key":"4_CR4","series-title":"RISC-Linz Report Series","first-page":"34","volume-title":"Int. Workshop on First-Order Theorem Proving (FTP\u201997)","author":"A. Brandl","year":"1997","unstructured":"A. Brandl, C. Ferm\u00fcller, and G. Salzer. Testing for renamability to classes of clause sets. In M. P. Bonacina and U. Furbach, editors, Int. Workshop on First-Order Theorem Proving (FTP\u201997), RISC-Linz Report Series No. 97-50, pages 34\u201339. Johannes Kepler Universit\u00e4t, Linz (Austria), 1997."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"R. Caferra and N. Zabel. A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613\u2013641, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR6","unstructured":"C. Ferm\u00fcller. Deciding Classes of Clause Sets by Resolution. PhD thesis, Technische Universit\u00e4t Wien, 1991."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem. LNAI 679. Springer, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller and G. Salzer. Ordered paramudulation and resolution as decision procedure. In A. Voronkov, editor, Logic Programming and Automated Reasoning, 4th International Conference, LPAR\u201993, St. Petersburg, Russia, July 1993, Proceedings, volume 698 of Lecture Notes in Artificial Intelligence, pages 122\u2013133. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56944-8_47"},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C.G. Ferm\u00fcller","year":"1996","unstructured":"C.G. Ferm\u00fcller and A. Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2):173\u2013203, 1996.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1093\/jigpal\/6.1.17","volume":"6","author":"C.G. Ferm\u00fcller","year":"1998","unstructured":"C.G. Ferm\u00fcller and A. Leitsch. Decision procedures and model building in equational clause logic. Journal of the IGPL, 6(1):17\u201341, 1998.","journal-title":"Journal of the IGPL"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"W.H. Joyner. Resolution strategies as decision procedures. Journal of the ACM, 23:398\u2013417, 1976.","journal-title":"Journal of the ACM"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Stefan Klingenbeck. Counter Examples in Semantic Tableaux. PhD thesis, University of Karlsruhe, 1996.","DOI":"10.1007\/3-540-59338-1_26"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"A. Leitsch. The resolution calculus. Springer. Texts in Theoretical Computer Science, 1997.","DOI":"10.1007\/978-3-642-60605-2"},{"key":"4_CR14","doi-asserted-by":"crossref","first-page":"163","DOI":"10.3233\/FI-1993-182-406","volume":"18","author":"A. Leitsch","year":"1993","unstructured":"Alexander Leitsch. Deciding clause classes by semantic clash resolution. Fundamenta Informaticae, 18:163\u2013182, 1993.","journal-title":"Fundamenta Informaticae"},{"key":"4_CR15","unstructured":"Donald W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North Holland, 1978."},{"key":"4_CR16","first-page":"250","volume":"98","author":"S.Y. Maslov","year":"1968","unstructured":"S.Y. Maslov. The inverse method for establishing deducibility for logical calculi\u2014. Proc. Steklov Inst. Math., 98:250\u201396, 1968.","journal-title":"Proc. Steklov Inst. Math."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Robert Matzinger. Computational representations of Herbrand models using grammars. In Computer Science Logic, CSL\u201996, 1997.","DOI":"10.1007\/3-540-63172-0_48"},{"key":"4_CR18","unstructured":"Nicolas Peltier. Nouvelles Techniques pour la Construction de Mod\u00e8les finis ou infinis en D\u00e9duction Automatique. PhD thesis, Institut National Polytechnique de Grenoble, 1997."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Nicolas Peltier. Simplifying formulae in tableaux. Pruning the search space and building models. In Proceeding of Tableaux\u201997, pages 313\u2013327. Springer, 1997. LNAI 1227.","DOI":"10.1007\/BFb0027423"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"R. Pichler. Algorithms on atomic representations of herbrand models. In Proc. of JELIA\u201998, pages 199\u2013215. Springer, LNAI 1489, 1998.","DOI":"10.1007\/3-540-49545-2_14"},{"key":"4_CR21","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach., 12:23\u201341, 1965.","journal-title":"J. Assoc. Comput. Mach."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"G. Salzer. Deductive generalization and meta-reasoning, or how to formalize Genesis. In H. Kaindl, editor, Proc. 7th Austrian Conference on Artificial Intelligence, Informatik-Berichte 287, pages 103\u2013115. Springer Verlag, 1991.","DOI":"10.1007\/978-3-642-46752-3_12"},{"key":"4_CR23","volume-title":"Unification of Meta-Terms","author":"G. Salzer","year":"1991","unstructured":"G. Salzer. Unification of Meta-Terms. Dissertation, Technische Universit\u00e4t Wien, Austria, 1991."},{"issue":"4","key":"4_CR24","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Slagle","year":"1974","unstructured":"J.R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. J. Association of Computing Machinery, 21(4):622\u2013642, 1974.","journal-title":"J. Association of Computing Machinery"},{"key":"4_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0019355","volume-title":"Baltic Computer Science","author":"T. Tammet","year":"1991","unstructured":"Tanel Tammet. Using resolution for deciding solvable classes and building finite models. In Baltic Computer Science, pages 33\u201364. Springer, LNCS 502, 1991."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T05:44:59Z","timestamp":1629524699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}