We give a decision procedure for the satisfiability of finite sets of ground equations and disequations in the constructor theory: the terms used may contain both uninterpreted and constructor function symbols. Constructor function symbols are by definition injective and terms built with distinct constructors are themselves distinct. This corresponds to properties of (co-) inductive type constructors in inductive type theory. We do this in a framework where function symbols can be partially applied and equations between functions are allowed. We describe our algorithm as an extension of congruence-closure and give correctness, completeness and termination arguments. We then proceed to discuss its limits and extension possibilities by describing its implementation in the Coq proof assistant. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Corbineau, P. (2007). Deciding equality in the constructor theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4502 LNCS, pp. 78–92). Springer Verlag. https://doi.org/10.1007/978-3-540-74464-1_6
Mendeley helps you to discover research relevant for your work.