Equational Formulas with Membership Constraints
| Autor: | Hubert Comon, C. Delor |
|---|---|
| Jazyk: | angličtina |
| Předmět: |
Discrete mathematics
Class (set theory) Algebraic specification Mathematical proof Computer Science Applications Theoretical Computer Science Decidability Algebra Computational Theory and Mathematics Closure (mathematics) Quantifier elimination Regular expression Axiom Information Systems Mathematics |
| Zdroj: | Information and Computation. (2):167-216 |
| ISSN: | 0890-5401 |
| DOI: | 10.1006/inco.1994.1056 |
| Popis: | We propose a set of transformation rules for first order formulae whose atoms are either equations between terms or "membership constraints" t∈ζ. ζ can be interpreted as a regular tree language (ζ is called a sort in the algebraic specification community) or as a tree language in any class of languages which satisfies some adequate closure and decidability properties. This set of rules is proved to be correct, terminating, and complete. This provides a quantifier elimination procedure: for every regular tree language L, the first order theory of some structure defining L is decidable. This extends the results of several previously published results. We also show how to apply our results to automatic inductive proofs in equational theories. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|