Abstract
Most logics of practical interest (e.g., first order, equality) in general are un-decidable. Theorem proving in the context of an undecidable logic means exploring infinite search spaces. To this end, search-guiding heuristics must be employed. The use of so-called fair heuristics basically guarantees that each point in the search space will be reached after a finite period of time. Under these conditions, a proof will eventually be found if it exists (i.e., we have a semi-decision procedure). Note, however, that the notion “fairness” is mainly of theoretic interest. In practice, it is important to find a proof in an “acceptable period of time” rather than “eventually”. Apart from this, resource limitations, in particular memory space, often make it impossible to conduct a fair search. Hence, in practice search procedures that can be unfair for several reasons are quite common.
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
Avenhaus, J. and Madlener, K. (1990): Term Rewriting and Equational Reasoning, in Formal Techniques in Artificial Intelligence, R.B. Banerji (ed.), North Holland, Amsterdam, pp. 1–43.
Avenhaus, J., Denzinger, J., and Fuchs, M. (1995): DISCOUNT: A system for distributed equational deduction, Proc. 6th Conference on Rewriting Techniques and Applications (RTA-95), Kaiserslautern, GER, LNCS 914, pp. 397–402.
Bachmair, L., Dershowitz, N., and Plaisted, D.A. (1989): Completion without Failure, Colloquium on the Resolution of Equations in Algebraic Structures, Austin, USA (1987), Academic Press.
Denzinger, J. (1995): Knowledge-Based Distributed Search Using Teamwork, Proc. 1st International Conference on Multi-agent Systems (ICMAS-95), San Francisco, USA, AAAI-Press, pp. 81–88.
Denzinger, J. and Fuchs, M. (1994): Goal Oriented Equational Theorem Proving Using Teamwork, Proc. KI-94, Saarbrücken, GER, LNAI 861, pp. 343–354.
Denzinger, J. and Fuchs, Marc and Fuchs, M. (1997a): High Performance ATP Systems by Combining Several AI Methods, Proc. 15th International Joint Conference on Artificial Intelligence (IJCAI-97), Nagoya, JAP, Morgan Kaufmann, pp. 102–107.
Denzinger, J. and Kronenburg, M. and Schulz, S. (1997b): DISCOUNT–A distributed and learning equational prover, Journal of Automated Reasoning 18 (2), pp. 189–198.
Denzinger, J. and Schulz, S. (1996): Learning Domain Knowledge to Improve Theorem Proving, Proc. 13th Conference on Automated Deduction (CADE-13), New Brunswick, USA, LNAI 1104, pp. 62–76.
Dershowitz, N. and Jouannaud, J.-P. (1990): Rewrite Systems, in Handbook of Theoretical Computer Science, J. van Leeuwen (ed.), Elsevier, Volume B, Chapter 6, pp. 243–320.
Fuchs, M. (1995): Learning Proof Heuristics By Adapting Parameters, in Machine Learning: Proceedings of the Twelfth International Conference (ICML-95), A. Prieditis and S. Russell (eds.), Morgan Kaufmann Publishers, San Francisco, USA, pp. 235–243.
Fuchs, M. (1996a): Experiments in the Heuristic Use of Past Proof Experience, Proc. 13th Conference on Automated Deduction (CADE-13), New Brunswick, USA, LNAI 1104, pp. 523–537.
Fuchs, M. (1996b): Experiments in the Automatic Selection of Problem-solving Strategies, LSA Report LSA-96–09E, Center for Learning Systems and Applications (LSA), University of Kaiserslautern, URL http://www.uni-kl.de/ AG-AvenhausMadlener/fuchs.html.
Fuchs, M. (1996c): Powerful Search Heuristics Based on Weighted Symbols, Level and Features, Proc. 9th Florida Artificial Intelligence Research Symposium (FLAIRS–96), Key West, USA, ISBN 0–9620–1738–8, pp. 449 – 453.
Fuchs, M. (1997a): Learning Search Heuristics for Automated Deduction,Ph.D. thesis, Verlag Dr. Kovaé, Hamburg, ISBN 3–86064–623–0.
Fuchs, M. (1997b): Flexible Re-enactment of Proofs, Proc. 8th Portuguese Conference on Artificial Intelligence (EPIA-97), Coimbra, POR, LNAI 1323, pp. 13–24.
Fuchs, M. (1997c): Automatic Selection of Search–guiding Heuristics, Proc. 10th Florida Artificial Intelligence Research Symposium (FLAIRS–97), Daytona Beach, USA, ISBN 0–9620–1739–6, pp. 1 – 5.
Fuchs, Marc and Fuchs, M. (1997): Applying Case-based Reasoning to Automated Deduction, Proc. 2nd International Conference on Case-based Reasoning (ICCBR97), Providence, Rhode Island, USA, LNAI 1266, pp. 23–32.
Graf, R (1995): Term Indexing, Springer LNAI 1053.
Hillenbrand, T. and Buch, A. and Fettig, R. (1996): On Gaining Efficiency in Completion-Based Theorem Proving, Proc. 7th Conference on Rewriting Techniques and Applications (RTA-96), New Brunswick, USA, LNCS 1103, pp. 432–435.
Hsiang, J. and Rusinowitch, M. (1987): On word problems in equational theories, Proc. 14th International Colloquium on Automata, Languages and Programming (ICALP-87), Karlsruhe, GER, LNCS 267, pp. 54–71.
Knuth, D.E. and Bendix, P.B. (1970): Simple Word Problems in Universal Algebra, Computational Algebra, J. Leech, Pergamon Press, pp. 263–297.
Kolbe, T. and Walther, C. (1994): Reusing Proofs, Proc. European Conference on Artificial Intelligence (ECAI ‘84), Amsterdam, HOL, pp. 80–84.
McCune, W. and Wos, L. (1992): Experiments in Automated Deduction with Condensed Detachment, Proc. 11th Conference on Automated Deduction (CADE-11), Saratoga Springs, USA, LNAI 607, pp. 209–223.
McCune, W. (1994): OTTER 3.0 Reference Manual and Guide, Techn. Report ANL-94/6, Argonne Natl. Laboratory.
Stickel, M. (1984): A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x3 = x Implies Ring Commutativity, Proc. 7th Conference on Automated Deduction (CADE-7), Napa, USA, LNCS 170, pp. 248–258.
Sutcliffe, G., Suttner, C., and Yemenis, T. (1994): The TPTP Problem Library, Proc. 12th Conference on Automated Deduction (CADE-12), Nancy, FRA, LNAI 814, pp. 252–266.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Denzinger, J., Fuchs, M. (1998). A Comparison of Equality Reasoning Heuristics. In: Bibel, W., Schmitt, P.H. (eds) Automated Deduction — A Basis for Applications. Applied Logic Series, vol 9. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0435-9_13
Download citation
DOI: https://doi.org/10.1007/978-94-017-0435-9_13
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5051-9
Online ISBN: 978-94-017-0435-9
eBook Packages: Springer Book Archive