{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T02:57:46Z","timestamp":1761620266434,"version":"build-2065373602"},"reference-count":273,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780444522115"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1016\/s1574-6526(07)03001-5","type":"book-chapter","created":{"date-parts":[[2008,9,12]],"date-time":"2008-09-12T16:06:55Z","timestamp":1221235615000},"page":"3-88","source":"Crossref","is-referenced-by-count":22,"title":["Chapter 1 Knowledge Representation and Classical Logic"],"prefix":"10.1016","member":"78","reference":[{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib001","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/j.artint.2003.07.001","article-title":"Logic-based subsumption architecture","volume":"153","author":"Amir","year":"2004","journal-title":"Artificial Intelligence"},{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib002","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/j.artint.2004.11.004","article-title":"Partition-based logical reasoning for first-order and propositional theories","volume":"162","author":"Amir","year":"2005","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib003","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib004","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BF00252180","article-title":"TPS: A theorem proving system for classical type theory","volume":"16","author":"Andrews","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1574-6526(07)03001-5_bib005","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","article-title":"TPS: A hybrid automatic-interactive system for developing proofs","volume":"4","author":"Andrews","year":"2006","journal-title":"Journal of Applied Logic"},{"issue":"3\u20134","key":"10.1016\/S1574-6526(07)03001-5_bib006","first-page":"151","article-title":"Dislop: A research project on disjunctive logic programming","volume":"10","author":"Aravindan","year":"1997","journal-title":"AI Commun."},{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib007","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","article-title":"Termination of term rewriting using dependency pairs","volume":"236","author":"Arts","year":"2000","journal-title":"Theoretical Computer Science"},{"year":"2003","series-title":"The Description Logic Handbook: Theory, Implementation, Applications","author":"Baader","key":"10.1016\/S1574-6526(07)03001-5_bib008"},{"key":"10.1016\/S1574-6526(07)03001-5_bib009","first-page":"445","article-title":"Unification theory","volume":"vol. I","author":"Baader","year":"2001"},{"volume":"vol. 2741","year":"2003","series-title":"CADE-19, 19th International Conference on Automated Deduction","key":"10.1016\/S1574-6526(07)03001-5_bib010"},{"year":"1998","series-title":"Term Rewriting and All That","author":"Baader","key":"10.1016\/S1574-6526(07)03001-5_bib011"},{"key":"10.1016\/S1574-6526(07)03001-5_bib012","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","article-title":"Termination orderings for associative\u2013commutative rewriting systems","volume":"1","author":"Bachmair","year":"1985","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/S1574-6526(07)03001-5_bib013","doi-asserted-by":"crossref","unstructured":"L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In J.H. Siekmann, editor. Proceedings of the Eighth International Conference on Automated Deduction, pages 5\u201320, 1986","DOI":"10.1007\/3-540-16780-3_76"},{"key":"10.1016\/S1574-6526(07)03001-5_bib014","unstructured":"L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceedings of the Symposium on Logic in Computer Science, pages 346\u2013357, 1986"},{"key":"10.1016\/S1574-6526(07)03001-5_bib015","series-title":"Resolution of Equations in Algebraic Structures 2: Rewriting Techniques","first-page":"1","article-title":"Completion without failure","author":"Bachmair","year":"1989"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib016","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib017","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Resolution theorem proving. In Robinson and Voronkov [231], pages 19\u201399","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib018","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","article-title":"Basic paramodulation","volume":"121","author":"Bachmair","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1574-6526(07)03001-5_bib019","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BFb0054259","article-title":"Elimination of equality via transformation with ordering constraints","volume":"1421","author":"Bachmair","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib020","series-title":"International Semantic Web Conference","first-page":"454","article-title":"Consistency checking of semantic web ontologies","volume":"vol. 2342","author":"Baclawski","year":"2002"},{"key":"10.1016\/S1574-6526(07)03001-5_bib021","series-title":"Formalizing Common Sense","first-page":"17","article-title":"Discussion of the paper: Programs with common sense","author":"Bar-Hillel","year":"1998"},{"issue":"1\u20133","key":"10.1016\/S1574-6526(07)03001-5_bib022","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/0004-3702(84)90044-4","article-title":"Verify: A program for proving correctness of digital hardware designs","volume":"24","author":"Barrow","year":"1984","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib023","first-page":"200","article-title":"FDPLL\u2014A first-order Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure","volume":"vol. 1831","author":"Baumgartner","year":"2000"},{"key":"10.1016\/S1574-6526(07)03001-5_bib024","doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. PROTEIN: A PROver with a theory extension INterface. In Proceedings of the Conference on Automated Deduction, 1994","DOI":"10.1007\/3-540-58156-1_57"},{"key":"10.1016\/S1574-6526(07)03001-5_bib025","series-title":"CADE-19: The 19th International Conference on Automated Deduction","first-page":"350","article-title":"The model evolution calculus","volume":"vol. 2741","author":"Baumgartner","year":"2003"},{"key":"10.1016\/S1574-6526(07)03001-5_bib026","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1023\/A:1006050629424","article-title":"Computer proofs in G\u00f6del's class theory with equational definitions for composite and cross","volume":"22","author":"Belinfante","year":"1999","journal-title":"Journal of Automated Reasoning"},{"year":"1971","series-title":"Computer Structures: Readings and Examples","author":"Bell","key":"10.1016\/S1574-6526(07)03001-5_bib027"},{"year":"1987","series-title":"Automated Theorem Proving","author":"Bibel","key":"10.1016\/S1574-6526(07)03001-5_bib028"},{"key":"10.1016\/S1574-6526(07)03001-5_bib029","series-title":"Proceedings of TABLEAUX-96","first-page":"110","article-title":"The disconnection method","volume":"vol. 1071","author":"Billon","year":"1996"},{"key":"10.1016\/S1574-6526(07)03001-5_bib030","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","article-title":"On the structure of abstract algebras","volume":"31","author":"Birkhoff","year":"1935","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"10.1016\/S1574-6526(07)03001-5_bib031","series-title":"CADE-16: Proceedings of the 16th International Conference on Automated Deduction Trento, Italy, 1999","first-page":"359","article-title":"A breadth-first strategy for mating search","volume":"vol. 1632","author":"Bishop","year":"1999"},{"key":"10.1016\/S1574-6526(07)03001-5_bib032","doi-asserted-by":"crossref","unstructured":"M. Bishop and P.B. Andrews. Selectively instantiating definitions. In Proceedings of the 15th International Conference on Automated Deduction, pages 365\u2013380, 1998","DOI":"10.1007\/BFb0054272"},{"key":"10.1016\/S1574-6526(07)03001-5_bib033","first-page":"751","article-title":"Solving numerical constraints","volume":"vol. 1","author":"Bockmayr","year":"2001"},{"issue":"4","key":"10.1016\/S1574-6526(07)03001-5_bib034","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1006\/jsco.1996.0028","article-title":"On the reconstruction of proofs in distributed theorem proving: a modified clause-diffusion method","volume":"21","author":"Bonacina","year":"1996","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib035","doi-asserted-by":"crossref","unstructured":"J. Bos and K. Markert. Recognising textual entailment with logical inference. In HLT\/EMNLP. The Association for Computational Linguistics, 2005","DOI":"10.3115\/1220575.1220654"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib036","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0898-1221(94)00215-7","article-title":"The Boyer\u2013Moore theorem prover and its interactive enhancement","volume":"29","author":"Boyer","year":"1995","journal-title":"Computers and Mathematics with Applications"},{"key":"10.1016\/S1574-6526(07)03001-5_bib037","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","article-title":"Set theory in first-order logic: Clauses for G\u00f6del's axioms","volume":"2","author":"Boyer","year":"1986","journal-title":"Journal of Automated Reasoning"},{"year":"1979","series-title":"A Computational Logic","author":"Boyer","key":"10.1016\/S1574-6526(07)03001-5_bib038"},{"year":"2004","series-title":"Knowledge Representation and Reasoning","author":"Brachman","key":"10.1016\/S1574-6526(07)03001-5_bib039"},{"key":"10.1016\/S1574-6526(07)03001-5_bib040","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","article-title":"Proving theorems with the modification method","volume":"4","author":"Brand","year":"1975","journal-title":"SIAM J. Comput."},{"year":"2000","series-title":"Prolog Programming for Artificial Intelligence","author":"Bratko","key":"10.1016\/S1574-6526(07)03001-5_bib041"},{"issue":"1\u20133","key":"10.1016\/S1574-6526(07)03001-5_bib042","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0004-3702(91)90053-M","article-title":"Intelligence without representation","volume":"47","author":"Brooks","year":"1991","journal-title":"Artificial Intelligence"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib043","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1574-6526(07)03001-5_bib044","series-title":"Multidimensional Systems Theory","first-page":"184","article-title":"Gr\u00f6bner bases: An algorithmic method in polynomial ideal theory","author":"Buchberger","year":"1985"},{"year":"1983","series-title":"The Computer Modelling of Mathematical Reasoning","author":"Bundy","key":"10.1016\/S1574-6526(07)03001-5_bib045"},{"key":"10.1016\/S1574-6526(07)03001-5_bib046","first-page":"845","article-title":"The automation of proof by mathematical induction","volume":"vol. I","author":"Bundy","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib047","article-title":"Rippling: Meta-Level Guidance for Mathematical Reasoning","volume":"vol. 56","author":"Bundy","year":"2005"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib048","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S1574-6526(07)03001-5_bib049","series-title":"TARK","first-page":"325","article-title":"Authentication: A practical study in belief and action","author":"Burrows","year":"1988"},{"key":"10.1016\/S1574-6526(07)03001-5_bib050","series-title":"Semantic Ambiguity and Underspecification","article-title":"Resolving lexical ambiguity using a formal theory of context","author":"Buvac","year":"1996"},{"year":"2004","series-title":"Automated Model Building","author":"Caferra","key":"10.1016\/S1574-6526(07)03001-5_bib051"},{"year":"1998","series-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","key":"10.1016\/S1574-6526(07)03001-5_bib052"},{"year":"1973","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","key":"10.1016\/S1574-6526(07)03001-5_bib053"},{"year":"1993","series-title":"Statistical Language Learning","author":"Charniak","key":"10.1016\/S1574-6526(07)03001-5_bib054"},{"key":"10.1016\/S1574-6526(07)03001-5_bib055","first-page":"707","article-title":"Automated reasoning in geometry","volume":"vol. I","author":"Chou","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib056","doi-asserted-by":"crossref","first-page":"40","DOI":"10.2307\/2269326","article-title":"A note on the Entscheidungsproblem","volume":"1","author":"Church","year":"1936","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1574-6526(07)03001-5_bib057","series-title":"Logic and Data Bases","first-page":"293","article-title":"Negation as failure","author":"Clark","year":"1978"},{"issue":"4","key":"10.1016\/S1574-6526(07)03001-5_bib058","first-page":"25","article-title":"The DARPA high-performance knowledge bases project","volume":"19","author":"Cohen","year":"1998","journal-title":"AI Magazine"},{"key":"10.1016\/S1574-6526(07)03001-5_bib059","first-page":"913","article-title":"Inductionless induction","volume":"vol. I","author":"Comon","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib060","series-title":"Proc. 12th IEEE Symp. Logic in Computer Science (LICS'97)","first-page":"26","article-title":"Ground reducibility is EXPTIME-complete","author":"Comon","year":"1997"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib061","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/601775.601777","article-title":"Deciding the confluence of ordered term rewrite systems","volume":"4","author":"Comon","year":"2003","journal-title":"ACM Trans. Comput. Logic"},{"year":"1986","series-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"Constable","key":"10.1016\/S1574-6526(07)03001-5_bib062"},{"key":"10.1016\/S1574-6526(07)03001-5_bib063","series-title":"Proceedings of the 3rd International Conference on Rewriting Techniques and Applications","first-page":"109","article-title":"Simulation of Turing machines by a left-linear rewrite rule","volume":"vol. 355","author":"Dauchet","year":"1989"},{"year":"1990","series-title":"Representations of Commonsense Knowledge","author":"Davis","key":"10.1016\/S1574-6526(07)03001-5_bib064"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib065","first-page":"51","article-title":"The naive physics perplex","volume":"19","author":"Davis","year":"1998","journal-title":"AI Magazine"},{"key":"10.1016\/S1574-6526(07)03001-5_bib066","doi-asserted-by":"crossref","unstructured":"M. Davis. Eliminating the irrelevant from mechanical proofs. In: Proceedings Symp. of Applied Math. vol. 15, pages 15\u201330, 1963","DOI":"10.1090\/psapm\/015\/0170497"},{"key":"10.1016\/S1574-6526(07)03001-5_bib067","article-title":"The prehistory and early history of automated deduction","volume":"vol. 1","author":"Davis","year":"1983"},{"key":"10.1016\/S1574-6526(07)03001-5_bib068","first-page":"31","article-title":"First order logic","volume":"vol. 1","author":"Davis","year":"1993"},{"key":"10.1016\/S1574-6526(07)03001-5_bib069","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib070","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib071","first-page":"179","article-title":"The inverse method","volume":"vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib072","doi-asserted-by":"crossref","unstructured":"E. Deplagne, C. Kirchner, H. Kirchner, and Q.H. Nguyen. Proof search and proof check for equational and inductive theorems. In Baader [10], pages 297\u2013316","DOI":"10.1007\/978-3-540-45085-6_26"},{"key":"10.1016\/S1574-6526(07)03001-5_bib073","unstructured":"N. Dershowitz. On representing ordinals up to \u03b30. Unpublished note, 1980"},{"key":"10.1016\/S1574-6526(07)03001-5_bib074","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib075","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"Journal of Symbolic Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib076","series-title":"Handbook of Theoretical Computer Science","article-title":"Rewrite systems","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S1574-6526(07)03001-5_bib077","first-page":"535","article-title":"Rewriting","volume":"vol. I","author":"Dershowitz","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib078","unstructured":"N. Dershowitz, J. Hsiang, N. Josephson, and D.A. Plaisted. Associative\u2013commutative rewriting. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, pages 940\u2013944, August 1983"},{"key":"10.1016\/S1574-6526(07)03001-5_bib079","series-title":"Proceedings of the 4th International Conference on Rewriting Techniques and Applications","article-title":"AC-unification through order-sorted AC1-unification","volume":"vol. 488","author":"Domenjoud","year":"1991"},{"key":"10.1016\/S1574-6526(07)03001-5_bib080","first-page":"39","article-title":"Number of minimal unifiers of the equation \u03b1x1+\u22ef+\u03b1xp=AC\u03b2y1+\u22ef+\u03b2yq","volume":"8","author":"Domenjoud","year":"1992","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"10.1016\/S1574-6526(07)03001-5_bib081","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","article-title":"Variations on the common subexpression problem","volume":"27","author":"Downey","year":"1980","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib082","doi-asserted-by":"crossref","unstructured":"J. Endrullis, J. Waldmann, and H. Zantema. Matrix interpretations for proving termination of term rewriting. In Furbach and Shankar [91], pages 574\u2013588","DOI":"10.1007\/11814771_47"},{"key":"10.1016\/S1574-6526(07)03001-5_bib083","unstructured":"R.S. Engelmore. Knowledge-based systems in Japan, 1993. http:\/\/www.wtec.org\/loyola\/kb\/"},{"key":"10.1016\/S1574-6526(07)03001-5_bib084","series-title":"EUROVAV","first-page":"107","article-title":"Specifying and verifying knowledge-based systems with KIV","author":"Fensel","year":"1997"},{"issue":"3\u20134","key":"10.1016\/S1574-6526(07)03001-5_bib085","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","article-title":"Strips: A new approach to the application of theorem proving to problem solving","volume":"2","author":"Fikes","year":"1971","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib086","article-title":"Deduction-based software component retrieval","volume":"vol. 3","author":"Fischer","year":"1998"},{"year":"1990","series-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","key":"10.1016\/S1574-6526(07)03001-5_bib087"},{"key":"10.1016\/S1574-6526(07)03001-5_bib088","series-title":"LPAR","first-page":"561","article-title":"Census data repair: a challenging application of disjunctive logic programming","volume":"vol. 2250","author":"Franconi","year":"2001"},{"year":"1879","series-title":"Begriffsschrift, eine der arithmetischen nachgebildete Formelschprache des reinen Denkens","author":"Frege","key":"10.1016\/S1574-6526(07)03001-5_bib089"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib090","first-page":"303","article-title":"The Munich rent advisor: A success for logic programming on the Internet","volume":"1","author":"Fr\u00fchwirth","year":"2001","journal-title":"TPLP"},{"volume":"vol. 4130","year":"2006","series-title":"Automated Reasoning, Third International Joint Conference, IJCAR 2006","key":"10.1016\/S1574-6526(07)03001-5_bib091"},{"key":"10.1016\/S1574-6526(07)03001-5_bib092","doi-asserted-by":"crossref","unstructured":"J.-M. Gaillourdet, T. Hillenbrand, B. L\u00f6chner, and H. Spies. The new Waldmeister loop at work. In Baader [10], pages 317\u2013321","DOI":"10.1007\/978-3-540-45085-6_27"},{"key":"10.1016\/S1574-6526(07)03001-5_bib093","series-title":"Proc. 18th IEEE Symposium on Logic in Computer Science, (LICS'03)","first-page":"55","article-title":"New directions in instantiation-based theorem proving","author":"Ganzinger","year":"2003"},{"key":"10.1016\/S1574-6526(07)03001-5_bib094","series-title":"Computers and Thought","first-page":"153","article-title":"Empirical explorations of the geometry theorem proving machine","author":"Gelernter","year":"1963"},{"year":"1987","series-title":"Logical Foundations of Artificial Intelligence","author":"Genesereth","key":"10.1016\/S1574-6526(07)03001-5_bib095"},{"key":"10.1016\/S1574-6526(07)03001-5_bib096","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/S1574-6526(07)03001-5_bib097","doi-asserted-by":"crossref","unstructured":"J. Giesl and D. Kapur. Deciding inductive validity of equations. In Baader [10], pages 17\u201331","DOI":"10.1007\/978-3-540-45085-6_3"},{"key":"10.1016\/S1574-6526(07)03001-5_bib098","doi-asserted-by":"crossref","unstructured":"J. Giesl, P. Schneider-Kamp, and R. Thiemann. Automatic termination proofs in the dependency pair framework. In Furbach and Shankar [91], pages 281\u2013286","DOI":"10.1007\/11814771_24"},{"key":"10.1016\/S1574-6526(07)03001-5_bib099","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1147\/rd.41.0028","article-title":"A proof method for quantification theory","volume":"4","author":"Gilmore","year":"1960","journal-title":"IBM Journal of Research and Development"},{"key":"10.1016\/S1574-6526(07)03001-5_bib100","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF01696781","article-title":"Die Vollst\u00e4ndigkeit fer Axiome des logischen Funktionenkalk\u00fcls","volume":"37","author":"G\u00f6del","year":"1930","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"year":"1993","series-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","key":"10.1016\/S1574-6526(07)03001-5_bib101"},{"key":"10.1016\/S1574-6526(07)03001-5_bib102","article-title":"Automatic partitioning of owl ontologies using-connections","author":"Grau","year":"2005","journal-title":"CEUR Workshop Proceedings"},{"year":"1969","series-title":"The Applications of Theorem Proving to Question-Answering Systems","author":"Green","key":"10.1016\/S1574-6526(07)03001-5_bib103"},{"key":"10.1016\/S1574-6526(07)03001-5_bib104","doi-asserted-by":"crossref","unstructured":"C.C. Green. Application of theorem proving to problem solving. In IJCAI, pages 219\u2013240, 1969","DOI":"10.21236\/ADA459656"},{"key":"10.1016\/S1574-6526(07)03001-5_bib105","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1137\/0212012","article-title":"On proving uniform termination and restricted termination of rewriting systems","volume":"12","author":"Guttag","year":"1983","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib106","first-page":"100","article-title":"Tableaux and related methods","volume":"vol. I","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib107","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib108","article-title":"An error in a lookup table created the infamous bug in Intel's latest processor","author":"Halfhill","year":"1995","journal-title":"BYTE"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib109","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/logcom\/11.1.41","article-title":"Multi-agent only knowing","volume":"11","author":"Halpern","year":"2001","journal-title":"J. Logic Comput."},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib110","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1016\/0004-3702(87)90043-9","article-title":"Nonmonotonic logic and temporal projection","volume":"33","author":"Hanks","year":"1987","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib111","series-title":"Formal Theories of the Commonsense World","first-page":"71","article-title":"Naive physics I: Ontology for liquids","author":"Hayes","year":"1975"},{"key":"10.1016\/S1574-6526(07)03001-5_bib112","unstructured":"P.J. Hayes. In defence of logic. In IJCAI, pages 559\u2013565, 1977"},{"key":"10.1016\/S1574-6526(07)03001-5_bib113","series-title":"Expert Systems in the Microelectronic Age","article-title":"The naive physics manifesto","author":"Hayes","year":"1979"},{"key":"10.1016\/S1574-6526(07)03001-5_bib114","series-title":"Formal Theories of the Commonsense World","first-page":"1","article-title":"The second naive physics manifesto","author":"Hayes","year":"1985"},{"key":"10.1016\/S1574-6526(07)03001-5_bib115","series-title":"K-CAP","first-page":"99","article-title":"Collaborative knowledge capture in ontologies","author":"Hayes","year":"2005"},{"key":"10.1016\/S1574-6526(07)03001-5_bib116","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/BF00264362","article-title":"The undecidability of the unification and matching problem for canonical theories","volume":"24","author":"Heilbrunner","year":"1987","journal-title":"Acta Informatica"},{"year":"1965","series-title":"Aspects of Scientific Explanation and Other Essays in the Philosophy of Science","author":"Hempel","key":"10.1016\/S1574-6526(07)03001-5_bib117"},{"key":"10.1016\/S1574-6526(07)03001-5_bib118","series-title":"Aspects of Scientific Explanation and Other Essays in the Philosophy of Science","first-page":"245","article-title":"Studies in the logic of explanation","author":"Hempel","year":"1965"},{"key":"10.1016\/S1574-6526(07)03001-5_bib119","doi-asserted-by":"crossref","unstructured":"J. Hendrix, J. Meseguer, and H. Ohsaki. A sufficient completeness checker for linear order-sorted specifications modulo axioms. In Furbach and Shankar [91], pages 151\u2013155","DOI":"10.1007\/11814771_14"},{"key":"10.1016\/S1574-6526(07)03001-5_bib120","doi-asserted-by":"crossref","unstructured":"N. Hirokawa and A. Middeldorp. Automating the dependency pair method. In Baader [10], pages 32\u201346","DOI":"10.1007\/978-3-540-45085-6_4"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib121","article-title":"An overview of the TACITUS project","volume":"12","author":"Hobbs","year":"1986","journal-title":"Computational Linguistics"},{"key":"10.1016\/S1574-6526(07)03001-5_bib122","doi-asserted-by":"crossref","unstructured":"J.R. Hobbs, D.E. Appelt, J. Bear, D.J. Israel, M. Kameyama, M.E. Stickel, and M. Tyson. Fastus: A cascaded finite-state transducer for extracting information from natural-language text. CoRR, cmp-lg\/9705013, 1997. Earlier version available as SRI Technical Report 519","DOI":"10.7551\/mitpress\/3007.003.0015"},{"year":"1985","series-title":"Formal Theories of the Commonsense World","author":"Hobbs","key":"10.1016\/S1574-6526(07)03001-5_bib123"},{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib124","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0004-3702(93)90015-4","article-title":"Interpretation as abduction","volume":"63","author":"Hobbs","year":"1993","journal-title":"Artificial Intelligence"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib125","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","article-title":"Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method","volume":"38","author":"Hsiang","year":"1991","journal-title":"Journal of the ACM"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib126","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of correctness of the Knuth\u2013Bendix completion algorithm","volume":"23","author":"Huet","year":"1981","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/S1574-6526(07)03001-5_bib127","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","article-title":"Proofs by induction in equational theories with constructors","volume":"25","author":"Huet","year":"1982","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1574-6526(07)03001-5_bib128","unstructured":"G. Huet and D. Lankford. On the uniform halting problem for term rewriting systems. Technical Report Rapport Laboria 283, IRIA, Le Chesnay, France, 1978"},{"key":"10.1016\/S1574-6526(07)03001-5_bib129","doi-asserted-by":"crossref","unstructured":"F. Jacquemard, M. Rusinowitch, and L. Vigneron. Compiling and verifying security protocols. In Logic Programming and Automated Reasoning, pages 131\u2013160, 2000","DOI":"10.1007\/3-540-44404-1_10"},{"key":"10.1016\/S1574-6526(07)03001-5_bib130","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","article-title":"Completion of a set of rules modulo a set of equations","volume":"15","author":"Jouannaud","year":"1986","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib131","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(82)90107-7","article-title":"On multiset orderings","volume":"15","author":"Jouannaud","year":"1982","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1574-6526(07)03001-5_bib132","series-title":"Proceedings of the Second IFIP Workshop on Formal Description of Programming Concepts","first-page":"331","article-title":"Recursive decomposition ordering","author":"Jouannaud","year":"1982"},{"key":"10.1016\/S1574-6526(07)03001-5_bib133","series-title":"Computational Logic: Essays in Honor of Alan Robinson","article-title":"Solving equations in abstract algebras: A rule-based survey of unification","author":"Jouannaud","year":"1991"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib134","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","article-title":"Automatic proofs by induction in theories without constructors","volume":"82","author":"Jouannaud","year":"1989","journal-title":"Inform. and Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib135","first-page":"137","article-title":"Zur\u00fcckf\u00fchrung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, bindren, Funktionsvariablen","volume":"4","author":"Kalm\u00e1r","year":"1936","journal-title":"Compositio Mathematica"},{"key":"10.1016\/S1574-6526(07)03001-5_bib136","unstructured":"S. Kamin and J.-J. Levy. Two generalizations of the recursive path ordering. Unpublished, February 1980"},{"key":"10.1016\/S1574-6526(07)03001-5_bib137","doi-asserted-by":"crossref","unstructured":"D. Kapur and P. Narendran. Double-exponential complexity of computing a complete set of AC-unifiers. In Proceedings 7th IEEE Symposium on Logic in Computer Science, pages 11\u201321. Santa Cruz, CA, 1992","DOI":"10.1109\/LICS.1992.185515"},{"key":"10.1016\/S1574-6526(07)03001-5_bib138","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","article-title":"On sufficient completeness and related properties of term rewriting systems","volume":"24","author":"Kapur","year":"1987","journal-title":"Acta Informatica"},{"key":"10.1016\/S1574-6526(07)03001-5_bib139","series-title":"Proc. of Tenth Conference on Foundations of Software Technology and Theoretical Computer Science","first-page":"133","article-title":"A new method for proving termination of AC-rewrite systems","volume":"vol. 472","author":"Kapur","year":"1990"},{"key":"10.1016\/S1574-6526(07)03001-5_bib140","series-title":"CADE-17: Proceedings of the 17th International Conference on Automated Deduction, vol. 1831","first-page":"324","article-title":"Extending decision procedures with induction schemes","author":"Kapur","year":"2000"},{"year":"2000","series-title":"Computer-Aided Reasoning: ACL2 Case Studies","key":"10.1016\/S1574-6526(07)03001-5_bib141"},{"year":"2000","series-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann","key":"10.1016\/S1574-6526(07)03001-5_bib142"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib143","first-page":"9","article-title":"Deduction with symbolic constraints","volume":"4","author":"Kirchner","year":"1990","journal-title":"Revue Francaise d'Intelligence Artificielle"},{"key":"10.1016\/S1574-6526(07)03001-5_bib144","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/S1574-6526(07)03001-5_bib145","doi-asserted-by":"crossref","unstructured":"A. Koprowski and H. Zantema. Automation of recursive path ordering for infinite labelled rewrite systems. In Furbach and Shankar [91], pages 332\u2013346","DOI":"10.1007\/11814771_30"},{"key":"10.1016\/S1574-6526(07)03001-5_bib146","doi-asserted-by":"crossref","unstructured":"K. Korovin and A. Voronkov. An AC-compatible Knuth\u2013Bendix order. In Baader [10], pages 47\u201359","DOI":"10.1007\/978-3-540-45085-6_5"},{"year":"1980","series-title":"Logic for Problem Solving","author":"Kowalski","key":"10.1016\/S1574-6526(07)03001-5_bib147"},{"key":"10.1016\/S1574-6526(07)03001-5_bib148","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1574-6526(07)03001-5_bib149","unstructured":"D. Lankford. Canonical algebraic simplification in computational logic. Technical Report Memo ATP-25, Automatic Theorem Proving Project. University of Texas, Austin, TX, 1975"},{"key":"10.1016\/S1574-6526(07)03001-5_bib150","unstructured":"D. Lankford. On proving term rewriting systems are Noetherian. Technical Report Memo MTP-3, Mathematics Department, Louisiana Tech., University, Ruston, LA, 1979"},{"key":"10.1016\/S1574-6526(07)03001-5_bib151","unstructured":"D. Lankford and A.M. Ballantyne. Decision problems for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Technical Report Memo ATP-39, Department of Mathematics and Computer Science, University of Texas, Austin, TX, 1977"},{"key":"10.1016\/S1574-6526(07)03001-5_bib152","series-title":"Proceedings of the 7th International Conference on Automated Deduction","first-page":"128","article-title":"A progress report on new decision algorithms for finitely presented abelian groups","volume":"vol. 170","author":"Lankford","year":"1984"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib153","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/BF00247825","article-title":"Eliminating duplication with the hyper-linking strategy","volume":"9","author":"Lee","year":"1992","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1574-6526(07)03001-5_bib154","first-page":"217","article-title":"Use of replace rules in theorem proving","volume":"1","author":"Lee","year":"1994","journal-title":"Methods of Logic in Computer Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib155","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","article-title":"The Resolution Calculus","author":"Leitsch","year":"1997"},{"issue":"11","key":"10.1016\/S1574-6526(07)03001-5_bib156","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/219717.219745","article-title":"Cyc: A large-scale investment in knowledge infrastructure","volume":"38","author":"Lenat","year":"1995","journal-title":"Communications of the ACM"},{"year":"1990","series-title":"Building Large Knowledge Based Systems: Representation and Inference in the Cyc Project","author":"Lenat","key":"10.1016\/S1574-6526(07)03001-5_bib157"},{"key":"10.1016\/S1574-6526(07)03001-5_bib158","first-page":"2015","article-title":"Model elimination and connection tableau procedures","volume":"vol. II","author":"Letz","year":"2001"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib159","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00245018","article-title":"What is the inverse method?","volume":"5","author":"Lifschitz","year":"1989","journal-title":"J. Autom. Reason."},{"key":"10.1016\/S1574-6526(07)03001-5_bib160","unstructured":"V. Lifschitz. Pointwise circumscription: Preliminary report. In AAAI, pages 406\u2013410, 1986"},{"key":"10.1016\/S1574-6526(07)03001-5_bib161","doi-asserted-by":"crossref","unstructured":"V. Lifschitz. Formal theories of action (preliminary report). In IJCAI, pages 966\u2013972, 1987","DOI":"10.1016\/B978-0-934613-32-3.50009-5"},{"key":"10.1016\/S1574-6526(07)03001-5_bib162","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","article-title":"A simplified format for the model elimination procedure","volume":"16","author":"Loveland","year":"1969","journal-title":"Journal of the ACM"},{"year":"1978","series-title":"Automated Theorem Proving: A Logical Basis","author":"Loveland","key":"10.1016\/S1574-6526(07)03001-5_bib163"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib164","first-page":"77","article-title":"Automated deduction: looking ahead","volume":"20","author":"Loveland","year":"1999","journal-title":"AI Magazine"},{"key":"10.1016\/S1574-6526(07)03001-5_bib165","series-title":"IJCAI","first-page":"89","article-title":"Practical partition-based theorem proving for large knowledge bases","author":"MacCartney","year":"2003"},{"year":"1999","series-title":"Foundations of Statistical Natural Language Processing","author":"Manning","key":"10.1016\/S1574-6526(07)03001-5_bib166"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib167","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1574-6526(07)03001-5_bib168","first-page":"1420","article-title":"An inverse method of establishing deducibilities in the classical predicate calculus","volume":"159","author":"Maslov","year":"1964","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"10.1016\/S1574-6526(07)03001-5_bib169","unstructured":"C. Matuszek, J. Cabral, M.J. Witbrock, and J. DeOliviera. An introduction to the syntax and content of cyc. In Proceedings of the AAAI 2006 Spring Symposium on Formalizing and Compiling Background Knowledge and its Applications to Knowledge Representation and Question Answering, 2006"},{"key":"10.1016\/S1574-6526(07)03001-5_bib170","series-title":"AAAI","first-page":"1430","article-title":"Searching for common sense: Populating cyc from the web","author":"Matuszek","year":"2005"},{"key":"10.1016\/S1574-6526(07)03001-5_bib171","unstructured":"J. McCarthy. Programs with common sense. In Proceedings of the Teddington Conference on the Mechanization of Thought Processes, pages 75\u201391. London, 1959"},{"key":"10.1016\/S1574-6526(07)03001-5_bib172","series-title":"Computer Programming and Formal Systems","article-title":"A basis for a mathematical theory of computation","author":"McCarthy","year":"1963"},{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib173","first-page":"23","article-title":"Circumscription: A form of non-monotonic reasoning","volume":"13","author":"McCarthy","year":"1980","journal-title":"Artificial Intelligence"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib174","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/0004-3702(86)90032-9","article-title":"Applications of circumscription to formalizing common sense knowledge","volume":"26","author":"McCarthy","year":"1986","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib175","series-title":"Machine Intelligence 4","first-page":"463","article-title":"Some philosophical problems from the standpoint of artificial intelligence","author":"McCarthy","year":"1969"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib176","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","article-title":"Solution of the Robbins problem","volume":"19","author":"McCune","year":"1997","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib177","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","article-title":"Otter\u2014the CADE-13 competition incarnations","volume":"18","author":"McCune","year":"1997","journal-title":"J. Autom. Reason."},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib178","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1207\/s15516709cog0203_5","article-title":"Tarskian semantics, or no notation without denotation!","volume":"2","author":"McDermott","year":"1978","journal-title":"Cognitive Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib179","first-page":"101","article-title":"A temporal logic for reasoning about processes and plans","volume":"6","author":"McDermott","year":"1982","journal-title":"Cognitive Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib180","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1111\/j.1467-8640.1987.tb00183.x","article-title":"A critique of pure reason","volume":"3","author":"McDermott","year":"1987","journal-title":"Computational Intelligence"},{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib181","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0004-3702(80)90012-0","article-title":"Non-monotonic logic I","volume":"13","author":"McDermott","year":"1980","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib182","unstructured":"A. Middeldorp. Modular properties of term rewriting systems. PhD thesis, Vrije Universiteit, Amsterdam, 1990"},{"key":"10.1016\/S1574-6526(07)03001-5_bib183","unstructured":"R. Miller and L. Morgenstern. The commonsense problem page, 1997. http:\/\/www-formal.stanford.edu\/leora\/commonsense"},{"key":"10.1016\/S1574-6526(07)03001-5_bib184","unstructured":"S. Miller and D.A. Plaisted. Performance of OSHL on problems requiring definition expansion. In R. Letz, editor. 7th International Workshop on First-Order Theorem Proving, Koblenz, Germany, September 15\u201317, 2005"},{"key":"10.1016\/S1574-6526(07)03001-5_bib185","series-title":"The Psychology of Computer Vision","article-title":"A framework for representing knowledge","author":"Minsky","year":"1975"},{"key":"10.1016\/S1574-6526(07)03001-5_bib186","unstructured":"R.C. Moore. The role of logic in knowledge representation and commonsense reasoning. In AAAI, pages 428\u2013433, 1982"},{"key":"10.1016\/S1574-6526(07)03001-5_bib187","series-title":"The Robot's Dilemma Revisited","article-title":"The problems with solutions to the frame problem","author":"Morgenstern","year":"1996"},{"key":"10.1016\/S1574-6526(07)03001-5_bib188","unstructured":"L. Morgenstern. A first-order axiomatization of the surprise birthday present problem: Preliminary report. In Proceedings of the Seventh International Symposium on Logical Formalizations of Commonsense Reasoning, 2005. Also published as Dresden Technical Report, ISSN 1430-211X"},{"key":"10.1016\/S1574-6526(07)03001-5_bib189","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1016\/0743-1066(94)90035-3","article-title":"Inductive logic programming: Theory and methods","volume":"19\/20","author":"Muggleton","year":"1994","journal-title":"J. Logic Program."},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib190","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","article-title":"Simplification by cooperating decision procedures","volume":"1","author":"Nelson","year":"1979","journal-title":"ACM TOPLAS"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib191","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast decision procedures based on congruence closure","volume":"27","author":"Nelson","year":"1980","journal-title":"Journal of the ACM"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib192","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of \u2018equivalence\u2019","volume":"43","author":"Newman","year":"1942","journal-title":"Annals of Mathematics"},{"key":"10.1016\/S1574-6526(07)03001-5_bib193","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"vol. I","author":"Nieuwenhuis","year":"2001"},{"issue":"4","key":"10.1016\/S1574-6526(07)03001-5_bib194","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","article-title":"Theorem proving with ordering and equality constrained clauses","volume":"19","author":"Nieuwenhuis","year":"1995","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S1574-6526(07)03001-5_bib195","unstructured":"N.J. Nilsson. Shakey the robot. Technical Report 323. SRI International, 1984"},{"key":"10.1016\/S1574-6526(07)03001-5_bib196","doi-asserted-by":"crossref","unstructured":"T. Nipkow, G. Bauer, and P. Schultz. Flyspeck I: Tame graphs. In Furbach and Shankar [91], pages 21\u201335","DOI":"10.1007\/11814771_4"},{"year":"2003","series-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow","key":"10.1016\/S1574-6526(07)03001-5_bib197"},{"key":"10.1016\/S1574-6526(07)03001-5_bib198","doi-asserted-by":"crossref","unstructured":"M. Nogueira, M. Balduccini, M. Gelfond, R. Watson, and M. Barry. An A-Prolog decision support system for the Space Shuttle. In Proceedings of International Symposium on Practical Aspects of Declarative Languages (PADL), pages 169\u2013183, 2001","DOI":"10.1007\/3-540-45241-9_12"},{"year":"2002","series-title":"Advanced Topics in Term Rewriting","author":"Ohlebusch","key":"10.1016\/S1574-6526(07)03001-5_bib199"},{"key":"10.1016\/S1574-6526(07)03001-5_bib200","series-title":"STOC'73: Proceedings of the Fifth Annual ACM Symposium on Theory of Computing","first-page":"34","article-title":"Elementary bounds for Presburger Arithmetic","author":"Oppen","year":"1973"},{"key":"10.1016\/S1574-6526(07)03001-5_bib201","series-title":"Proceedings of the Eleventh Conference on Automated Deduction","first-page":"748","article-title":"PVS: A prototype verification system","volume":"vol. 607","author":"Owrie","year":"1992"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib202","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","article-title":"Linear unification","volume":"16","author":"Paterson","year":"1978","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S1574-6526(07)03001-5_bib203","article-title":"Isabelle: A Generic Theorem Prover","volume":"vol. 828","author":"Paulson","year":"1994"},{"key":"10.1016\/S1574-6526(07)03001-5_bib204","unstructured":"G. Peano. Arithmetices principia, nova methodo exposita. Turin, 1889. English translation: [261, pp. 83\u201397]"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib205","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for some equational theories","volume":"28","author":"Peterson","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib206","unstructured":"L. Pike. Formal verification of time-triggered systems. PhD thesis, Indiana University, 2005"},{"key":"10.1016\/S1574-6526(07)03001-5_bib207","unstructured":"D. Plaisted. A recursively defined ordering for proving termination of term rewriting systems. Technical report R-78-943, University of Illinois at Urbana-Champaign, Urbana, IL, 1978"},{"key":"10.1016\/S1574-6526(07)03001-5_bib208","unstructured":"D. Plaisted. Well-founded orderings for proving termination of systems of rewrite rules. Technical report R-78-932, University of Illinois at Urbana-Champaign, Urbana, IL, 1978"},{"key":"10.1016\/S1574-6526(07)03001-5_bib209","unstructured":"D. Plaisted. An associative path ordering. In Proceedings of an NSF Workshop on the Rewrite Rule Laboratory, pages 123\u2013136, April 1984"},{"issue":"2\u20133","key":"10.1016\/S1574-6526(07)03001-5_bib210","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","article-title":"Semantic confluence tests and completion methods","volume":"65","author":"Plaisted","year":"1985","journal-title":"Information and Control"},{"key":"10.1016\/S1574-6526(07)03001-5_bib211","series-title":"Intelligent Systems: State of the Art and Future Directions","first-page":"200","article-title":"Inference by clause matching","author":"Plaisted","year":"1990"},{"year":"1997","series-title":"The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis","author":"Plaisted","key":"10.1016\/S1574-6526(07)03001-5_bib212"},{"issue":"3","key":"10.1016\/S1574-6526(07)03001-5_bib213","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1006376231563","article-title":"Ordered semantic hyperlinking","volume":"25","author":"Plaisted","year":"2000","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1574-6526(07)03001-5_bib214","first-page":"73","article-title":"Building-in equational theories","volume":"vol. 7","author":"Plotkin","year":"1972"},{"year":"1959","series-title":"The Logic of Scientific Discovery","author":"Popper","key":"10.1016\/S1574-6526(07)03001-5_bib215"},{"key":"10.1016\/S1574-6526(07)03001-5_bib216","doi-asserted-by":"crossref","first-page":"163","DOI":"10.2307\/2370324","article-title":"Introduction to a general theory of elementary propositions","volume":"43","author":"Post","year":"1921","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/S1574-6526(07)03001-5_bib217","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/S1574-6526(07)03001-5_bib218","series-title":"Proceedings of the Twelfth International Conference on Automated Deduction","first-page":"238","article-title":"The QED manifesto","volume":"vol. 814","author":"QED Group","year":"1994"},{"key":"10.1016\/S1574-6526(07)03001-5_bib219","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00263451","article-title":"Automated deduction in von Neumann\u2013Bernays\u2013G\u00f6del set theory","volume":"8","author":"Quaife","year":"1992","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1574-6526(07)03001-5_bib220","unstructured":"D. Ramachandran, P. Reagan, and K. Goolsbey. First-orderized researchcyc: Expressivity and efficiency in a common-sense ontology. Working Papers of the AAAI Workshop on Contexts and Ontologies: Theory, Practice, and Applications, 2005"},{"key":"10.1016\/S1574-6526(07)03001-5_bib221","unstructured":"D. Ramachandran, P. Reagan, K. Goolsbey, K. Keefe, and E. Amir. Inference-friendly translation of researchcyc to first order logic, 2005. Unpublished"},{"key":"10.1016\/S1574-6526(07)03001-5_bib222","first-page":"1853","article-title":"Term indexing","volume":"vol. II","author":"Ramakrishnan","year":"2001"},{"key":"10.1016\/S1574-6526(07)03001-5_bib223","series-title":"K-CAP","first-page":"121","article-title":"Modularisation of domain ontologies implemented in description logics and related formalisms including owl","author":"Rector","year":"2003"},{"issue":"1\u20132","key":"10.1016\/S1574-6526(07)03001-5_bib224","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","article-title":"A logic for default reasoning","volume":"13","author":"Reiter","year":"1980","journal-title":"Artificial Intelligence"},{"year":"2001","series-title":"Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems","author":"Reiter","key":"10.1016\/S1574-6526(07)03001-5_bib225"},{"key":"10.1016\/S1574-6526(07)03001-5_bib226","unstructured":"A. Riazanov. Implementing an efficient theorem prover. PhD thesis, The University of Manchester, Manchester, July 2003"},{"issue":"2\u20133","key":"10.1016\/S1574-6526(07)03001-5_bib227","first-page":"91","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov","year":"2002","journal-title":"AI Communications"},{"key":"10.1016\/S1574-6526(07)03001-5_bib228","first-page":"135","article-title":"Paramodulation and theorem-proving in first order theories with equality","volume":"vol. 4","author":"Robinson","year":"1969"},{"key":"10.1016\/S1574-6526(07)03001-5_bib229","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/321160.321166","article-title":"Theorem proving on the computer","volume":"10","author":"Robinson","year":"1963","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib230","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"year":"2001","series-title":"Handbook of Automated Reasoning (in 2 volumes)","key":"10.1016\/S1574-6526(07)03001-5_bib231"},{"key":"10.1016\/S1574-6526(07)03001-5_bib232","unstructured":"J.F. Rulifson, J.A. Derksen, and R.J. Waldinger. Qa4: A procedural calculus for intuitive reasoning. Technical Report 73, AI Center, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94025, Nov. 1972"},{"year":"2003","series-title":"Artificial Intelligence: A Modern Approach","author":"Russell","key":"10.1016\/S1574-6526(07)03001-5_bib233"},{"year":"1989","series-title":"Four Decades of Scientific Explanation","author":"Salmon","key":"10.1016\/S1574-6526(07)03001-5_bib234"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib235","first-page":"111","article-title":"E\u2014a brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Communications"},{"key":"10.1016\/S1574-6526(07)03001-5_bib236","series-title":"DEXA Workshops","first-page":"228","article-title":"English as a formal specification language","author":"Schwitter","year":"2002"},{"year":"1997","series-title":"Solving the Frame Problem","author":"Shanahan","key":"10.1016\/S1574-6526(07)03001-5_bib237"},{"key":"10.1016\/S1574-6526(07)03001-5_bib238","unstructured":"Y. Shoham. Chronological ignorance: Time, nonmonotonicity, necessity and causal theories. In AAAI, pages 389\u2013393, 1986"},{"key":"10.1016\/S1574-6526(07)03001-5_bib239","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","article-title":"Unification theory","volume":"7","author":"Siekmann","year":"1989","journal-title":"Journal of Symbolic Computation"},{"issue":"4","key":"10.1016\/S1574-6526(07)03001-5_bib240","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","article-title":"Computer supported mathematics with Omega","volume":"4","author":"Siekmann","year":"2006","journal-title":"Journal of Applied Logic"},{"key":"10.1016\/S1574-6526(07)03001-5_bib241","series-title":"Automating Software Design","first-page":"483","article-title":"KIDS: A knowledge-based software development system","author":"Smith","year":"1991"},{"key":"10.1016\/S1574-6526(07)03001-5_bib242","series-title":"CSFW","first-page":"153","article-title":"Cryptographically sound theorem proving","author":"Sprenger","year":"2006"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib243","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(94)90061-2","article-title":"Motivated action theory: A formal theory of causal reasoning","volume":"71","author":"Stein","year":"1994","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib244","series-title":"Proceedings of the 3rd International Conference on rewriting techniques and applications","first-page":"434","article-title":"Extensions and comparison of simplification orderings","volume":"vol. 355","author":"Steinbach","year":"1989"},{"key":"10.1016\/S1574-6526(07)03001-5_bib245","series-title":"Proc. of the International Joint Conference on Automated Reasoning","first-page":"381","article-title":"DCTP\u2014a disconnection calculus theorem prover","volume":"vol. 2083","author":"Stenz","year":"2001"},{"issue":"4","key":"10.1016\/S1574-6526(07)03001-5_bib246","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","article-title":"A Prolog technology theorem prover: Implementation by an extended Prolog compiler","volume":"4","author":"Stickel","year":"1988","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1574-6526(07)03001-5_bib247","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF01531174","article-title":"A Prolog-like inference system for computing minimum-cost abductive explanation in natural-language interpretation","volume":"4","author":"Stickel","year":"1991","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/S1574-6526(07)03001-5_bib248","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(92)90168-F","article-title":"A Prolog technology theorem prover: A new exposition and implementation in Prolog","volume":"104","author":"Stickel","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1574-6526(07)03001-5_bib249","unstructured":"M.E. Stickel, R.J. Waldinger, and V.K. Chaudhri. A guide to SNARK. Technical report, SRI International, 2000"},{"key":"10.1016\/S1574-6526(07)03001-5_bib250","series-title":"CADE","first-page":"341","article-title":"Deductive composition of astronomical software from subroutine libraries","volume":"vol. 814","author":"Stickel","year":"1994"},{"key":"10.1016\/S1574-6526(07)03001-5_bib251","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","article-title":"A unification algorithm for associative\u2013commutative functions","volume":"28","author":"Stickel","year":"1981","journal-title":"J. of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib252","doi-asserted-by":"crossref","unstructured":"M.E. Stickel. A Prolog technology theorem prover: Implementation by an extended Prolog compiler. In Proceedings of the 8th International Conference on Automated Deduction, pages 573\u2013587, 1986","DOI":"10.1007\/3-540-16780-3_122"},{"key":"10.1016\/S1574-6526(07)03001-5_bib253","series-title":"Proc. of the International Joint Conference on Automated Reasoning","first-page":"572","article-title":"CASC-J3: The 3rd IJCAR ATP system competition","volume":"vol. 4130","author":"Sutcliffe","year":"2006"},{"issue":"2","key":"10.1016\/S1574-6526(07)03001-5_bib254","first-page":"173","article-title":"The CADE-20 automated theorem proving competition","volume":"19","author":"Sutcliffe","year":"2006","journal-title":"AI Communications"},{"key":"10.1016\/S1574-6526(07)03001-5_bib255","unstructured":"C.B. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.0.0). Technical Report AR-97-01, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany, 1997"},{"key":"10.1016\/S1574-6526(07)03001-5_bib256","article-title":"Term Rewriting Systems","volume":"vol. 55","author":"Terese","year":"2003"},{"key":"10.1016\/S1574-6526(07)03001-5_bib257","series-title":"Stanford Encyclopedia of Philosophy","article-title":"Logic and artificial intelligence","author":"Thomason","year":"2003"},{"issue":"1","key":"10.1016\/S1574-6526(07)03001-5_bib258","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","article-title":"On the Church\u2013Rosser property for the direct sum of term rewriting systems","volume":"34","author":"Toyama","year":"1987","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1574-6526(07)03001-5_bib259","series-title":"Proceedings of the 3rd International Conference on Rewriting Techniques and Applications","first-page":"477","article-title":"Termination for the direct sum of left-linear term rewriting systems","volume":"vol. 355","author":"Toyama","year":"1989"},{"key":"10.1016\/S1574-6526(07)03001-5_bib260","series-title":"Logic of Programs","article-title":"Computer aided reasoning with Mizar","volume":"vol. 193","author":"Trybulec","year":"1985"},{"year":"1967","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","key":"10.1016\/S1574-6526(07)03001-5_bib261"},{"key":"10.1016\/S1574-6526(07)03001-5_bib262","doi-asserted-by":"crossref","unstructured":"E.M. Voorhees and L.P. Buckland, editors. The Eleventh Text Retrieval Conference, 2002","DOI":"10.6028\/NIST.SP.500-250"},{"key":"10.1016\/S1574-6526(07)03001-5_bib263","doi-asserted-by":"crossref","unstructured":"E.M. Voorhees and L.P. Buckland, editors. The Twelfth Text Retrieval Conference, 2003","DOI":"10.6028\/NIST.SP.500-251"},{"key":"10.1016\/S1574-6526(07)03001-5_bib264","doi-asserted-by":"crossref","unstructured":"E.M. Voorhees and L.P. Buckland, editors. The Thirteenth Text Retrieval Conference, 2004","DOI":"10.6028\/NIST.SP.500-255"},{"key":"10.1016\/S1574-6526(07)03001-5_bib265","doi-asserted-by":"crossref","unstructured":"E.M. Voorhees and L.P. Buckland, editors. The Fourteenth Text Retrieval Conference, 2005","DOI":"10.6028\/NIST.SP.500-261"},{"key":"10.1016\/S1574-6526(07)03001-5_bib266","doi-asserted-by":"crossref","unstructured":"E.M. Voorhees and L.P. Buckland, editors. The Fifteenth Text Retrieval Conference, 2006","DOI":"10.6028\/NIST.SP.500-266"},{"key":"10.1016\/S1574-6526(07)03001-5_bib267","unstructured":"Y. Wang, P. Haase, and J. Bao. A survey of formalisms for modular ontologies. In Workshop on Semantic Web for Collaborative Knowledge Acquisition, 2007"},{"key":"10.1016\/S1574-6526(07)03001-5_bib268","doi-asserted-by":"crossref","unstructured":"C. Weidenbach. Combining superposition, sorts and splitting. In Robinson and Voronkov [231], pages 1965\u20132013","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"10.1016\/S1574-6526(07)03001-5_bib269","series-title":"CADE","first-page":"275","article-title":"S pass version 2.0","volume":"vol. 2392","author":"Weidenbach","year":"2002"},{"year":"1957","series-title":"Principia Mathematica","author":"Whitehead","key":"10.1016\/S1574-6526(07)03001-5_bib270"},{"year":"1984","series-title":"Automated Reasoning: Introduction and Applications","author":"Wos","key":"10.1016\/S1574-6526(07)03001-5_bib271"},{"key":"10.1016\/S1574-6526(07)03001-5_bib272","first-page":"159","article-title":"On the decision problem and the mechanization of theorem proving in elementary geometry","volume":"21","author":"Wu","year":"1978","journal-title":"Scientia Sinica"},{"key":"10.1016\/S1574-6526(07)03001-5_bib273","unstructured":"P. Youn, B. Adida, M. Bon, J. Clulow, J. Herzog, A. Lin, R.L. Rivest, and R. Anderson. Robbing the bank with a theorem prover. Technical report 644, University of Cambridge Computer Laboratory, August 2005"}],"container-title":["Foundations of Artificial Intelligence","Handbook of Knowledge Representation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1574652607030015?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1574652607030015?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T02:54:29Z","timestamp":1761620069000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1574652607030015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9780444522115"],"references-count":273,"URL":"https:\/\/doi.org\/10.1016\/s1574-6526(07)03001-5","relation":{},"ISSN":["1574-6526"],"issn-type":[{"type":"print","value":"1574-6526"}],"subject":[],"published":{"date-parts":[[2008]]}}}