A superposition oriented theorem prover
Author:
- Laurent FribourgLFLaurent Fribourg
- 31 December 1985
- journal article
- Published by Elsevier in Theoretical Computer Science
- Vol. 35, 129-164
Abstract
No abstract availableKeywords
This publication has 10 references indexed in Scilit:
- 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
- Orderings for term-rewriting systemsTheoretical Computer Science, 1982
- A complete proof of correctness of the Knuth-Bendix completion algorithmJournal of Computer and System Sciences, 1981
- A Unification Algorithm for Associative-Commutative FunctionsJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- The Semantics of Predicate Logic as a Programming LanguageJournal of the ACM, 1976
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965