Tactics for Reasoning Modulo AC in Coq

DOI10.1007/978-3-642-25379-9_14zbMath1350.68227arXiv1106.4448OpenAlexW2096639003MaRDI QIDQ3100211

Thomas Braibant, Damien Pous

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1106.4448

Mathematics Subject Classification ID

Related Items

A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Extensible and Efficient Automation Through Reflective Tactics

Uses Software

• Coq
• Maude
• OCaml
• HOL90

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in Boolean rings and Abelian groups
• Single elementary associative-commutative matching
• Equational reasoning in Isabelle
• External rewriting for skeptical proof assistants
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• First-Class Type Classes
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Complete Sets of Reductions for Some Equational Theories
• How to make ad hoc proof automation less ad hoc
• Theorem Proving in Higher Order Logics
• An Efficient Coq Tactic for Deciding Kleene Algebras
• Rewriting Techniques and Applications