Positive deduction modulo regular theories

DOI10.1007/3-540-61377-3_54zbMATH Open1540.03027MaRDI QIDQ6560184FDOQ6560184

Authors: Laurent Vigneron 

Publication date: 21 June 2024

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

Mathematics Subject Classification ID

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

Cites Work

• A Machine-Oriented Logic Based on the Resolution Principle
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Proving refutational completeness of theorem-proving strategies
• Basic paramodulation
• Theorem-proving with resolution and superposition
• Completion of a Set of Rules Modulo a Set of Equations
• Title not available (Why is that?)
• Completion for rewriting modulo a congruence
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A precedence-based total AC-compatible ordering
• 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
• Title not available (Why is that?)
• Associative-commutative deduction with constraints
• Automated deduction with associative-commutative operators

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)