Theorem proving modulo associativity

DOI10.1007/3-540-61377-3_53zbMATH Open1540.03026MaRDI QIDQ6560183

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)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A total AC-compatible ordering based on RPO
• Theorem proving with ordering and equality constrained clauses
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Any ground associative-commutative theory has a finite canonical system
• Associative-commutative deduction with constraints
• AC-superposition with constraints: No AC-unifiers needed

This page was built for publication: Theorem proving modulo associativity