Rewrite methods for clausal and non-clausal theorem proving
- 25 January 2006
- book chapter
- Published by Springer Nature
- p. 331-346
- https://doi.org/10.1007/bfb0036919
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Comparison of natural deduction and locking resolution implementationsPublished by Springer Nature ,2005
- A Unification Algorithm for Associative-Commutative FunctionsJournal of the ACM, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Proofs by induction in equational theories with constructorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1980
- A Catalogue of Canonical Term Rewriting Systems.Published by Defense Technical Information Center (DTIC) ,1980
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974
- Experiment with an automatic theorem-prover having partial ordering inference rulesCommunications of the ACM, 1973
- The complexity of theorem-proving proceduresPublished by Association for Computing Machinery (ACM) ,1971
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965