Equational methods in first order predicate calculus
DOI10.1016/S0747-7171(85)80026-2zbMATH Open0577.03003MaRDI QIDQ1065783FDOQ1065783
Authors: Etienne Paul 
Publication date: 1985
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Recommendations
- Equational treatment of first-order logic
- scientific article; zbMATH DE number 3851084
- Complete problems in the first-order predicate calculus
- Equational logic as a tool
- scientific article; zbMATH DE number 1368949
- scientific article; zbMATH DE number 4047723
- Equational Reasoning in Non-Classical Logics
- scientific article; zbMATH DE number 1036757
- Equational reasoning in Isabelle
- Equational inference, canonical proofs, and proof orderings
resolutionconfluencenarrowingequational rewriting systemsKnuth-Bendix completion algorithmproof proceduresquantifier free first order logic
Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05)
Cites Work
- Title not available (Why is that?)
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Complete Sets of Reductions for Some Equational Theories
- Title not available (Why is that?)
- A remark on functionally free algebras
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (12)
- Rewrite method for theorem proving in first order theory with equality
- On the soundness and completeness of equational predicate logics
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Socratic proofs for quantifiers
- Discriminator varieties and symbolic computation
- A categorical critical-pair completion algorithm
- Reduction techniques for first-order reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- History and basic features of the critical-pair/completion procedure
- Linear and unit-resulting refutations for Horn theories
- On solving the equality problem in theories defined by Horn clauses
This page was built for publication: Equational methods in first order predicate calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1065783)
