Associative-commutative deduction with constraints

DOI10.1007/3-540-58156-1_39MaRDI QIDQ5210795zbMATH OpenOpenAlexFDO

Authors Laurent Vigneron

Publication date 21 January 2020

Published in Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58156-1_39

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Automated deduction with associative-commutative operators
• Termination and completion modulo associativity, commutativity and identity
• Paramodulation with built-in AC-theories and symbolic constraints
• AC-superposition with constraints: no AC-unifiers needed
• A general refutational completeness result for an inference procedure based on associative-commutative unification

Cites work

• scientific article; zbMATH DE number 4072440 (Why is no real title available?)
• scientific article; zbMATH DE number 1348468 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 500953 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A general refutational completeness result for an inference procedure based on associative-commutative unification
• A precedence-based total AC-compatible ordering
• Any ground associative-commutative theory has a finite canonical system
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Complete Sets of Reductions for Some Equational Theories
• Complete sets of reductions with constraints
• On restrictions of ordered paramodulation with simplification
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Ordered rewriting and confluence
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Semi-Automated Mathematics
• Theorem-proving with resolution and superposition

Cited in

(16)

• AC-complete unification and its application to theorem proving
• On narrowing, refutation proofs and constraints
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Positive deduction modulo regular theories
• Theorem proving modulo associativity
• Local simplification
• Equational theorem proving modulo
• Theorem proving in cancellative abelian monoids (extended abstract)
• Local simplification
• Superposition theorem proving for abelian groups represented as integer modules
• Superposition with completely built-in abelian groups
• Associative-Commutative Deducibility Constraints
• Superposition theorem proving for abelian groups represented as integer modules
• AC-superposition with constraints: no AC-unifiers needed
• Automated deduction with associative-commutative operators
• Constrained equational deduction

This page was built for publication: Associative-commutative deduction with constraints

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