An ordered theory resolution calculus
- 23 November 2005
- book chapter
- Published by Springer Nature
- p. 119-130
- https://doi.org/10.1007/bfb0013054
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- First-order theorem proving using conditional rewrite rulesPublished by Springer Nature ,2005
- Rigid E-unification: NP-completeness and applications to equational matingsInformation and Computation, 1990
- Theory links: Applications to automated theorem provingJournal of Symbolic Computation, 1987
- Termination of rewritingJournal of Symbolic Computation, 1987
- A new method for establishing refutational completeness in theorem provingPublished by Springer Nature ,1986
- Automated deduction by theory resolutionJournal of Automated Reasoning, 1985
- Krypton: A Functional Approach to Knowledge RepresentationComputer, 1983
- Theorem Proving via General MatingsJournal of the ACM, 1981
- A Linear Format for Resolution With Merging and a New Technique for Establishing CompletenessJournal of the ACM, 1970
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965