We investigate the problem of deciding first-order theories of finite trees with several distinguished congruence relations, each of them given by some equational axioms. We give an automata-based solution for the case where the different equational axiom systems are linear and variable-disjoint (this includes the case where all axioms are ground), and where the logic does not permit to express tree relations x = f(y, z). We show that the problem is undecidable when these restrictions are relaxed. As motivation and application, we show how to translate the model-checking problem of AπL, a spatial equational logic for the applied pi-calculus, to the validity of first-order formulas in term algebras with multiple congruence relations.
CITATION STYLE
Jacquemard, F., Lozes, É., Treinen, R., & Villard, J. (2015). Multiple congruence relations, first-order theories on terms, and the frames of the applied pi-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6993, pp. 166–185). Springer Verlag. https://doi.org/10.1007/978-3-642-27375-9_10
Mendeley helps you to discover research relevant for your work.