Abstract
We investigate a hierarchical combination approach to the unification problem in non-disjoint unions of equational theories. In this approach, the idea is to extend a base theory with some additional axioms given by rewrite rules in such way that the unification algorithm known for the base theory can be reused without loss of completeness. Additional techniques are required to solve a combined problem by reducing it to a problem in the base theory. In this paper we show that the hierarchical combination approach applies successfully to some classes of syntactic theories, such as shallow theories since the required unification algorithms needed for the combination algorithm can always be obtained. We also consider the matching problem in syntactic extensions of a base theory. Due to the more restricted nature of the matching problem, we obtain several improvements over the unification problem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York (1998)
Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation 21(2), 211–243 (1996)
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)
Boudet, A.: Combining unification algorithms. Journal of Symbolic Computation 16(6), 597–626 (1993)
Boudet, A., Contejean, E.: On n-syntactic equational theories. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 446–457. Springer, Heidelberg (1992)
Comon, H., Haberstrau, M., Jouannaud, J.: Syntacticness, cycle-syntacticness, and shallow theories. Inf. Comput. 111(1), 154–191 (1994)
Erbatur, S., Kapur, D., Marshall, A.M., Narendran, P., Ringeissen, C.: Hierarchical combination. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 249–266. Springer, Heidelberg (2013)
Erbatur, S., Kapur, D., Marshall, A.M., Narendran, P., Ringeissen, C.: Hierarchical combination of matching algorithms. In: Twentyeighth International Workshop on Unification (UNIF 2014), Vienna, Austria (2014)
Erbatur, S., Marshall, A.M., Kapur, D., Narendran, P.: Unification over distributive exponentiation (sub)theories. Journal of Automata, Languages and Combinatorics (JALC) 16(2–4), 109–140 (2011)
Gallier, J.H., Snyder, W.: Complete sets of transformations for general E-unification. Theoretical Computer Science 67(2–3), 203–260 (1989)
Jouannaud, J.-P.: Syntactic theories. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol. 452, pp. 15–25. Springer, Heidelberg (1990)
Kirchner, C., Klay, F.: Syntactic theories and unification. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science Logic in Computer Science, LICS 1990, pp. 270–277, June1990
Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002)
Nieuwenhuis, R.: Decidability and complexity analysis by basic paramodulation. Inf. Comput. 147(1), 1–21 (1998)
Nipkow, T.: Proof transformations for equational theories. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science Logic in Computer Science, LICS 1990, pp. 278–288, June 1990
Nipkow, T.: Combining matching algorithms: The regular case. J. Symb. Comput. 12(6), 633–654 (1991)
Ringeissen, C.: Combining decision algorithms for matching in the union of disjoint equational theories. Inf. Comput. 126(2), 144–160 (1996)
Schmidt-Schauß, M.: Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation 8, 51–99 (1989)
Snyder, W.: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic, vol. 11. Birkhäuser (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Erbatur, S., Kapur, D., Marshall, A.M., Narendran, P., Ringeissen, C. (2015). Unification and Matching in Hierarchical Combinations of Syntactic Theories. In: Lutz, C., Ranise, S. (eds) Frontiers of Combining Systems. FroCoS 2015. Lecture Notes in Computer Science(), vol 9322. Springer, Cham. https://doi.org/10.1007/978-3-319-24246-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-24246-0_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24245-3
Online ISBN: 978-3-319-24246-0
eBook Packages: Computer ScienceComputer Science (R0)