Equational methods in first order predicate calculus
From MaRDI portal
Publication:1065783
DOI10.1016/S0747-7171(85)80026-2zbMath0577.03003MaRDI QIDQ1065783
Publication date: 1985
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
confluenceresolutionnarrowingequational rewriting systemsKnuth-Bendix completion algorithmproof proceduresquantifier free first order logic
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
On solving the equality problem in theories defined by Horn clauses ⋮ Rewrite method for theorem proving in first order theory with equality ⋮ History and basic features of the critical-pair/completion procedure ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Discriminator varieties and symbolic computation ⋮ A categorical critical-pair completion algorithm
Cites Work
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A remark on functionally free algebras
- Complete Sets of Reductions for Some Equational Theories
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- A Machine-Oriented Logic Based on the Resolution Principle
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Equational methods in first order predicate calculus
