Abstract
Modular higher-order E-unification, as described in [6], produces numerous redundant solutions in many practical cases. We present a refined algorithm for finitary theories with a finite number of non-free constants that avoids most redundant solutions, analyse it theoretically, and give first experimental results. In comparison to [6], the description of the E-unification algorithm is enriched by a definition of the translation process between first and higher-order terms and an explicit handling of new variables. This explicit handling gives deeper insight into the reasons for redundant solutions and thus provides a method for their avoidance. In order to study the efficiency of this method and the performance of the modular approach in general, some benchmark examples are presented and an interpretation of their empirical evaluation is given.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Dougherty, D. and Johann, P.: A Combinatory Logic Approach to Higher-Order E-Unification. Proc. 11th Conf. Automated Deduction, LNCS 607 (1992), 79–93.
Gallier, J. and Snyder, W.: Complete Sets of Transformations for General E- Unification. Theoretical Computer Science, 67 (1988), 203–260.
Huet, G.: A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1 (1975), 27–57.
Müller, O.: Optimierung der modularen E-Unifikation höherer Stufe — Implementierung und Analyse, master thesis, Karlsruhe 1993.
Nipkow, T. and Qian, Z.: Modular Higher-Order E-Unification. Proc. 4th Int. Conf. Rewriting Techniques and Applications, LNCS 488 (1991), 200–214.
Qian, Z. and Wang, K.: Higher-Order E-Unification for Arbitrary Theories. Proc. of 1992 Int. Joint Conf. and Symp. on Logic Programming, MIT Press, 1992.
Snyder, W. and Gallier, J.: Higher-Order Unification Revisited: Complete Sets of Transformations. J. Symbolic Computation 8 (1989), 101–140.
Weber, F.: Softwareentwicklung mit Logik höherer Stufe — eine Anwendung von Theoriededuktion auf interaktives Beweisen, PhD thesis, Karlsruhe 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, O., Weber, F. (1994). Theory and practice of minimal modular higher-order E-unification. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_47
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive