Abstract
Extracting knowledge from hard to prove First-order predicate calculus problems and their solutions may lead to improve the performance of automated theorem provers. In this work, we examine the association between the syntactic characteristics of the theorems and the techniques (inference methods and the control strategies) used by various ATPs (automated theorem provers) when attempted these problems. The aim is to determine the most suitable combination of inference methods and control strategies for classes of problems based on their syntactic characteristics. Data mining classification techniques are used to extract knowledge from ATPs attempts on these problems. Such knowledge identifies meta-strategies that are capable to enhance the performance of ATPs. Design improvements in software engineering often enhance the process of software creation, verification, and maintenance. This is one of the primary objectives of this work.
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
Sutcliffe, G., Fuchs, M., Suttner, C.: Progress in Automated Theorem Proving 1997-1999. In: Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence (2001)
Sutcliffe, G., Suttner, C.: Evaluating General Purpose Automated Theorem Proving Systems. Artificial Intelligence Journal 131, 39–54 (2001)
Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning 8, 183–212 (1992)
Tammet, T.: Gandalf. Journal of Automated Reasoning 18(2), 199–204 (1997)
Voronkov, A.: The anatomy of Vampire. Journal of Automated Reasoning 15, 237–265 (1995)
Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topić, D.: System Description: Spass Version 1.0.0. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 378–382. Springer, Heidelberg (1999)
Löchner, B., Hillenbrand, T.: A Phytography of WALDMEISTER 1. AI Communications 15, 127–133 (2002)
Claessen, K., Sorensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: CADE-19 Workshop: Model Computation - Principles; Algorithms; and Applications (2003)
Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, pp. 56–68 (2003)
Andrews, P., Brown, C.: TPS: A Hybrid Automatic-Interactive System for Developing Proofs. Journal of Applied Logic 4(4), 367–395 (2006)
Benzmüller, C.E., Kohlhase, M.: System Description: Leo - A Higher-Order Theorem Prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 139–143. Springer, Heidelberg (1998)
Pelletier, F.J., Sutcliffe, G., Suttner, C.: The Development of CASC. AI Communications 15, 79–90 (2002)
Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)
Sutcliffe, G.: The CADE-22 Automated Theorem Proving System Competition -CASC-22. AI Communications 23, 47–60 (2010)
McCune, W.: OTTER 3.3 Reference Manual, Argonne National Laboratory, ANL/MSC-TM-263 (2003)
Korovin, K.: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)
Sutcliffe, G., Fuchs, M.: Homogeneous Sets of ATP Problems. In: 15th International Florida Artificial Intelligence Research Society Conference, pp. 57–61 (2000)
Denzinger, J., Fuchs, M.: High Performance ATP Systems by Combining Several AI Methods. In: 15th International Joint Conference on Artificial Intelligence, pp. 102–107 (1997)
Fuchs, M.: A Feature-Based Learning Method for Theorem Proving. In: 15th National Conference on Artificial Intelligence, pp. 457–462 (1998)
Kakkad, A.: Machine Learning for Automated Theorem Proving, unpublished Master’s Thesis for Master’s Degree, University of Miami (2009)
Schulz, S.: E- A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)
Wos, L., Robinson, G., Carson, D.: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. Journal of the ACM 12(4), 536–541 (1965)
Stenz, G., Wolf, A.: Strategy Selection by Genetic Programming. In: 12th International Florida Artificial Intelligence Research Society Conference, pp. 346–350 (1999)
Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: 12th International Florida Artificial Intelligence Research Society Conference, pp. 341–345 (1999)
Shearer, C.: The CRISP-DM model: The New Blueprint for Data Mining. J. Data Warehousing 5, 13–22 (2000)
Witten, H., Frank, E.: Data Mining: Practical Machine Learning Tools and Techniques, 2nd edn. Morgan Kaufmann (2005)
Newborn, M., Wang, Z.: Octopus: Combining Learning and Parallel Search. Journal of Automated Reasoning 33(2), 171–218 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Khalifa, M., Raafat, H., Almulla, M. (2012). Machine Learning Approach to Enhance the Design of Automated Theorem Provers. In: Huang, T., Zeng, Z., Li, C., Leung, C.S. (eds) Neural Information Processing. ICONIP 2012. Lecture Notes in Computer Science, vol 7664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34481-7_82
Download citation
DOI: https://doi.org/10.1007/978-3-642-34481-7_82
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34480-0
Online ISBN: 978-3-642-34481-7
eBook Packages: Computer ScienceComputer Science (R0)