Positive deduction modulo regular theories
From MaRDI portal
Publication:6560184
DOI10.1007/3-540-61377-3_54zbMATH Open1540.03027MaRDI QIDQ6560184FDOQ6560184
Authors: Laurent Vigneron 
Publication date: 21 June 2024
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)
