On solving the equality problem in theories defined by Horn clauses
- 1 January 1985
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- A Narrowing Procedure for Theories with ConstructorsPublished by Springer Nature ,1984
- A Technique for Establishing Completeness Results in Theorem Proving with EqualitySIAM Journal on Computing, 1983
- Proofs by induction in equational theories with constructorsJournal of Computer and System Sciences, 1982
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- The Semantics of Predicate Logic as a Programming LanguageJournal of the ACM, 1976
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974
- Unit Refutations and Horn SetsJournal of the ACM, 1974
- The Unit Proof and the Input Proof in Theorem ProvingJournal of the ACM, 1970
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965