On solving the equality problem in theories defined by Horn clauses
- 31 December 1986
- journal article
- Published by Elsevier in Theoretical Computer Science
- Vol. 44 (2) , 127-153
- https://doi.org/10.1016/0304-3975(86)90114-3
Abstract
No abstract availableKeywords
This publication has 13 references indexed in Scilit:
- Equational methods in first order predicate calculusJournal of Symbolic Computation, 1985
- Oriented equational clauses as a programming languageThe Journal of Logic Programming, 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
- A complete proof of correctness of the Knuth-Bendix completion algorithmJournal of Computer and System Sciences, 1981
- The Semantics of Predicate Logic as a Programming LanguageJournal of the ACM, 1976
- Problems and Experiments for and with Automated Theorem-Proving ProgramsIEEE Transactions on Computers, 1976
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Unit Refutations and Horn SetsJournal of the ACM, 1974
- The Unit Proof and the Input Proof in Theorem ProvingJournal of the ACM, 1970