Positive deduction modulo regular theories

DOI10.1007/3-540-61377-3_54MaRDI QIDQ6560184zbMATHFDO

Authors Laurent Vigneron

Publication date 21 June 2024

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1348470
• scientific article; zbMATH DE number 1552532
• Theorem-proving with resolution and superposition
• Equational theorem proving modulo
• Regular Derivations in Basic Superposition-Based Calculi

Cites work

• scientific article; zbMATH DE number 3921960 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A Unification Algorithm for Associative-Commutative Functions
• A precedence-based total AC-compatible ordering
• Associative-commutative deduction with constraints
• Automated deduction with associative-commutative operators
• Basic paramodulation
• Complete Sets of Reductions for Some Equational Theories
• Completion for rewriting modulo a congruence
• Completion of a Set of Rules Modulo a Set of Equations
• Extension of the associative path ordering to a chain of associative commutative symbols
• On restrictions of ordered paramodulation with simplification
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Theorem-proving with resolution and superposition

This page was built for publication: Positive deduction modulo regular theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6560184)