A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms

We present a tool for checking the sufficient completeness of linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Joe Hendrix, José Meseguer, Hitoshi Ohsaki
• Keywords: CADE 2006, Equational Tree Automata, Logical Reasoning, Sufficient Completeness, Tree Automata