Theorem proving modulo associativity

DOI10.1007/3-540-61377-3_53MaRDI QIDQ6560183zbMATHFDO

Authors Albert Rubio

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

• Equational theorem proving modulo
• Automated deduction with associative-commutative operators
• Associative-commutative deduction with constraints
• A general refutational completeness result for an inference procedure based on associative-commutative unification
• Theorem proving with ordering and equality constrained clauses

Cites work

• scientific article; zbMATH DE number 3827173 (Why is no real title available?)
• scientific article; zbMATH DE number 4078851 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• A total AC-compatible ordering based on RPO
• AC-superposition with constraints: no AC-unifiers needed
• Any ground associative-commutative theory has a finite canonical system
• Associative-commutative deduction with constraints
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Theorem proving with ordering and equality constrained clauses

Cited in

(1)

• Equational theorem proving modulo

This page was built for publication: Theorem proving modulo associativity

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