Equational methods in first order predicate calculus

DOI10.1016/S0747-7171(85)80026-2MaRDI QIDQ1065783zbMATH OpenFDO

Authors Etienne Paul

Publication date 1985

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

resolutionconfluencenarrowingequational rewriting systemsKnuth-Bendix completion algorithmproof proceduresquantifier free first order logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05)

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

Cites work

• scientific article; zbMATH DE number 3891336 (Why is no real title available?)
• scientific article; zbMATH DE number 3829296 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• scientific article; zbMATH DE number 3019695 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A remark on functionally free algebras
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Complete Sets of Reductions for Some Equational Theories

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
• scientific article; zbMATH DE number 3871320 (Why is no real title available?)
• scientific article; zbMATH DE number 3851084 (Why is no real title available?)
• 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)