Proof planning with multiple strategies. (English) Zbl 1182.68259
Summary: Proof planning is a technique for theorem proving which replaces the ultra-efficient but blind search of classical theorem proving systems by an informed knowledge-based planning process that employs mathematical knowledge at a human-oriented level of abstraction. Standard proof planning uses methods as operators and control rules to find an abstract proof plan which can be expanded (using tactics) down to the level of the underlying logic calculus.In this paper, we propose more flexible refinements and a modification of the proof planner with an additional strategic level of control above the previous proof planning control. This strategic control guides the cooperation of the problem solving strategies by meta-reasoning.We present a general framework for proof planning with multiple strategies and describe its implementation in the Multi system. The benefits are illustrated by several large case studies, which significantly push the limits of what can be achieved by a machine today.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Software:
HR; TRAMP; Lambda-Clam; Waldmeister; Bliksem; Multi; SicoTHEO; OTTER; IsaPlanner; Prodigy; SPASS; GAPReferences:
| [1] | S. Autexier, Hierarchical contextual reasoning, Computer Science Department, Saarland University, Saarbrücken, Germany, PhD thesis, 2003; S. Autexier, Hierarchical contextual reasoning, Computer Science Department, Saarland University, Saarbrücken, Germany, PhD thesis, 2003 |
| [2] | Gandalf, O., CASC-14 (1997) |
| [3] | (Baader, F., Proceedings of the 19th International Conference on Automated Deduction (CADE-19). Proceedings of the 19th International Conference on Automated Deduction (CADE-19), Miami Beach, FL. Proceedings of the 19th International Conference on Automated Deduction (CADE-19). Proceedings of the 19th International Conference on Automated Deduction (CADE-19), Miami Beach, FL, LNAI, vol. 2741 (2003), Springer-Verlag: Springer-Verlag Germany) · Zbl 1026.00022 |
| [4] | Bartle, R.; Sherbert, D., Introduction to Real Analysis (1982), John Wiley & Sons: John Wiley & Sons New York · Zbl 0494.26002 |
| [5] | Bledsoe, W., Challenge problems in elementary analysis, Journal of Automated Reasoning, 6, 341-359 (1990) · Zbl 0702.68092 |
| [6] | Bledsoe, W., I had a dream: AAAI presidential address, AI Magazine, August, 57-61 (1985) |
| [7] | Bundy, A., The use of explicit plans to guide inductive proofs, (Lusk, E.; Overbeek, R., Proceedings of the 9th International Conference on Automated Deduction (CADE-9). Proceedings of the 9th International Conference on Automated Deduction (CADE-9), Argonne, IL. Proceedings of the 9th International Conference on Automated Deduction (CADE-9). Proceedings of the 9th International Conference on Automated Deduction (CADE-9), Argonne, IL, LNCS, vol. 310 (1988), Springer Verlag: Springer Verlag Germany), 111-120 · Zbl 0656.68106 |
| [8] | A. Bundy, A critique of proof planning, in: Festschrift in Honour of Robert Kowalski, 2002; A. Bundy, A critique of proof planning, in: Festschrift in Honour of Robert Kowalski, 2002 |
| [9] | Bundy, A.; van Harmelen, F.; Hesketh, J.; Smaill, A., Experiments with proof plans for induction, Journal of Automated Reasoning, 7, 303-324 (1991) · Zbl 0733.68069 |
| [10] | Church, A., A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 56-68 (1940) · JFM 66.1192.06 |
| [11] | A. Cohen, S. Murray, M. Pollet, V. Sorge, Certifying solutions to permutation group problems, in: [3]; A. Cohen, S. Murray, M. Pollet, V. Sorge, Certifying solutions to permutation group problems, in: [3] · Zbl 1278.68254 |
| [12] | Colton, S., Automated Theory Formation in Pure Mathematics (2002), Springer-Verlag: Springer-Verlag London · Zbl 1219.68141 |
| [13] | Corkill, D.; Lesser, V.; Hudlicka, Unifying data-directed and goal-directed control, (Waltz, D., Proceedings of the Second National Conference on Artificial Intelligence (AAAI-82). Proceedings of the Second National Conference on Artificial Intelligence (AAAI-82), Carnegie-Mellon University/University of Pittsburgh, Pittsburgh, PA (1982), AAAI Press: AAAI Press Menlo Park, CA), 143-147 |
| [14] | De Nivelle, H., Bliksem User Manual (1998), Delft University of Technology |
| [15] | Denzinger, J.; Fuchs, D., Cooperation of heterogeneous provers, (Dean, T., Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI). Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI), Stockholm, Sweden (1999), Morgan Kaufmann: Morgan Kaufmann San Mateo, CA), 10-15 |
| [16] | L. Dixon, J. Fleuriot, IsaPlanner: A prototype proof planner in Isabelle, in: [3]; L. Dixon, J. Fleuriot, IsaPlanner: A prototype proof planner in Isabelle, in: [3] |
| [17] | Durfee, E.; Lesser, V., Incremental planning to control a blackboard-based problem solver, (Kehler, T.; Rosenschein, S., Proceedings of the Fifth National Conference on Artificial Intelligence (AAAI-86). Proceedings of the Fifth National Conference on Artificial Intelligence (AAAI-86), Philadelphia, PA (1986), AAAI Press: AAAI Press Menlo Park, CA), 58-64 |
| [18] | (Engelmore, R.; Morgan, T., Blackboard Systems (1988), Addison-Wesley) |
| [19] | Erman, L.; London, P.; Fickas, S., The design and an example use of HEARSAY-III, (Buchanan, B., Proceedings of the 6th International Joint Conference on Artificial Intelligence (ICJAI) (1979), Morgan Kaufmann: Morgan Kaufmann Tokyo, Japan), 409-415 |
| [20] | E. Fink, How to solve it automatically: Selection among problem-solving methods, in: [50]; E. Fink, How to solve it automatically: Selection among problem-solving methods, in: [50] |
| [21] | GAP, GAP—Groups, Algorithms, and Programming, Version 4, The GAP Group, 1998; GAP, GAP—Groups, Algorithms, and Programming, Version 4, The GAP Group, 1998 |
| [22] | (Gomes, C.; Selman, B.; Kautz, H.; Mostow, J., Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI-98) and Tenth Conference on Innovative Application of Artificial Intelligence (IAAI-98). Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI-98) and Tenth Conference on Innovative Application of Artificial Intelligence (IAAI-98), Madison, WI (1998), AAAI Press: AAAI Press Menlo Park, CA), 431-437 |
| [23] | P. Hayes, D.B. Anderson, An arraignment of theorem-proving; or, the logician’s folly, Memo 54, Dept. Computational Logic, Edinburgh University, 1972; P. Hayes, D.B. Anderson, An arraignment of theorem-proving; or, the logician’s folly, Memo 54, Dept. Computational Logic, Edinburgh University, 1972 |
| [24] | Hayes-Roth, B.; Hayes, P., A blackboard architecture for control, Artificial Intelligence, 25, 251-321 (1985) |
| [25] | Hillenbrand, T.; Jaeger, A.; Löchner, B., System description: Waldmeister, improvements in performance and ease of use, (Ganzinger, H., Proceedings of the 16th International Conference on Automated Deduction (CADE-16). Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy. Proceedings of the 16th International Conference on Automated Deduction (CADE-16). Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy, LNAI, vol. 1632 (1999), Springer-Verlag: Springer-Verlag Germany), 232-236 |
| [26] | Howe, A.; Dahlman, E.; Hansen, C.; Scheetz, M.; von Mayrhauser, A., Exploiting competitive planner performance, (Biundo, S.; Fox, M., Recent Advances in AI Planning, Proceedings of the 5th European Conference on Planning (ECP’99). Recent Advances in AI Planning, Proceedings of the 5th European Conference on Planning (ECP’99), Durham, UK. Recent Advances in AI Planning, Proceedings of the 5th European Conference on Planning (ECP’99). Recent Advances in AI Planning, Proceedings of the 5th European Conference on Planning (ECP’99), Durham, UK, LNCS, vol. 1809 (1999), Springer Verlag: Springer Verlag Germany), 62-72 |
| [27] | Ireland, A., The use of planning critics in mechanizing inductive proofs, (Voronkov, A., Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning (LPAR’92). Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning (LPAR’92), St. Petersburg, Russia. Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning (LPAR’92). Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning (LPAR’92), St. Petersburg, Russia, LNAI, vol. 624 (1992), Springer-Verlag: Springer-Verlag Germany), 178-189 |
| [28] | Ireland, A.; Bundy, A., Productive use of failure in inductive proof, Journal of Automated Reasoning, 16, 1-2, 79-111 (1996) · Zbl 0847.68103 |
| [29] | W.W. McCune, Otter 2.0 users guide, Argonne National Laboratory, ANL-90/9, 1990; W.W. McCune, Otter 2.0 users guide, Argonne National Laboratory, ANL-90/9, 1990 |
| [30] | A. Meier, Randomization and heavy-tailed behavior in proof planning, Seki Report SR-00-03, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, 2000; A. Meier, Randomization and heavy-tailed behavior in proof planning, Seki Report SR-00-03, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, 2000 |
| [31] | Meier, A., TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level, (McAllester, D., Proceedings of the 17th Conference on Automated Deduction (CADE-17). Proceedings of the 17th Conference on Automated Deduction (CADE-17), LNAI, vol. 1831 (2000), Springer-Verlag: Springer-Verlag Germany), 460-464 · Zbl 0963.68537 |
| [32] | A. Meier, Proof planning with multiple strategies, Ph.D. thesis, University of Saarland, FB Informatik, Saarbrücken, Germany, 2004; A. Meier, Proof planning with multiple strategies, Ph.D. thesis, University of Saarland, FB Informatik, Saarbrücken, Germany, 2004 · Zbl 0983.68531 |
| [33] | Meier, A.; Gomes, C.; Melis, E., Randomization and restarts in proof planning, (Cesta, A.; Borrajo, D., 6th European Conference on Planning (ECP-01). 6th European Conference on Planning (ECP-01), LNCS (2001), Springer) |
| [34] | Meier, A.; Melis, E., Impasse-driven reasoning in proof planning, (Kohlhase, M., Proceedings of Fourth International Conference on Mathematical Knowledge Management (MKM2005). Proceedings of Fourth International Conference on Mathematical Knowledge Management (MKM2005), LNAI, vol. 3863 (2005), Springer-Verlag), 143-158 · Zbl 1151.68636 |
| [35] | Meier, A.; Melis, E., MULTI: A multi-strategy proof planner, (Nieuwenhuis, R., Automated Deduction: 20th International Conference on Automated Deduction (CADE-20). Automated Deduction: 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia. Automated Deduction: 20th International Conference on Automated Deduction (CADE-20). Automated Deduction: 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, LNAI, vol. 3632 (2005), Springer-Verlag), 250-254 · Zbl 1135.68557 |
| [36] | Meier, A.; Melis, E.; Pollet, M., Adaptable mixed-initiative proof planning for educational interaction, Electronic Notes in Theoretical Computer Science, 103, C, 105-120 (2004) |
| [37] | Meier, A.; Sorge, V.; Colton, S., Employing theory formation to guide proof planning, (Calmet, J.; Benhamou, B.; Caprotti, O.; Henocque, L.; Sorge, V., Proceedings of Joint International Conferences, AISC 2002 and Calculemus 2002. Proceedings of Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France (2002), Springer-Verlag: Springer-Verlag Germany), 275-289 · Zbl 1072.68582 |
| [38] | E. Melis, Island planning and refinement, Seki Report SR-96-10, Universität des Saarlandes, FB Informatik, 1996; E. Melis, Island planning and refinement, Seki Report SR-96-10, Universität des Saarlandes, FB Informatik, 1996 |
| [39] | Melis, E., AI-techniques in proof planning, (Prade, H., Proceedings of the 13th European Conference on Artificial Intelligence (1998), John Wiley & Sons: John Wiley & Sons Brighton, UK), 494-498 |
| [40] | Melis, E.; Leron, U., A proof presentation suitable for teaching proofs, (Lajoie, S. P.; Vivet, M., 9th International Conference on Artificial Intelligence in Education (1999), IOS Press), 483-490 |
| [41] | Melis, E.; Siekmann, J., Knowledge-based proof planning, Artificial Intelligence, 115, 1, 65-105 (1999) · Zbl 0939.68822 |
| [42] | M. Pollet, E. Melis, A. Meier, User interface for adaptive suggestions for interactive proof, in: Proceedings of the International Workshop on User Interfaces for Theorem Provers (UITP 2003), Rome, Italy, 2003; M. Pollet, E. Melis, A. Meier, User interface for adaptive suggestions for interactive proof, in: Proceedings of the International Workshop on User Interfaces for Theorem Provers (UITP 2003), Rome, Italy, 2003 |
| [43] | J. Richardson, A. Smaill, Continuations of proof strategies, in: R. Gore, A. Leitsch, T. Nipkov (Eds.), Short Papers of International Joint Conference on Automated Reasoning, 2001; J. Richardson, A. Smaill, Continuations of proof strategies, in: R. Gore, A. Leitsch, T. Nipkov (Eds.), Short Papers of International Joint Conference on Automated Reasoning, 2001 |
| [44] | Richardson, J.; Smaill, A.; Green, I., System description: Proof planning in higher-order logic with λClam, (Kirchner, C.; Kirchner, H., Proceedings of the 15th International Conference on Automated Deduction (CADE-15). Proceedings of the 15th International Conference on Automated Deduction (CADE-15), Lindau, Germany. Proceedings of the 15th International Conference on Automated Deduction (CADE-15). Proceedings of the 15th International Conference on Automated Deduction (CADE-15), Lindau, Germany, LNAI, vol. 1421 (1998), Springer-Verlag: Springer-Verlag Germany), 129-133 · Zbl 0892.00047 |
| [45] | Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. 1 (2001), Elsevier · Zbl 0964.00020 |
| [46] | Schoenfeld, A., Mathematical Problem Solving (1985), Academic Press: Academic Press New York · Zbl 0655.00020 |
| [47] | J. Schumann, SiCoTHEO—simple competitive parallel theorem provers based on SETHEO, in: Proceedings of PPAI’95, Montreal, Canada, 1995; J. Schumann, SiCoTHEO—simple competitive parallel theorem provers based on SETHEO, in: Proceedings of PPAI’95, Montreal, Canada, 1995 |
| [48] | Siekmann, J.; Benzmüller, C.; Autexier, S., Computer supported mathematics with ΩMEGA, Journal of Applied Logic (2006) · Zbl 1107.68101 |
| [49] | Siekmann, J.; Benzmüller, C.; Fiedler, A.; Meier, A.; Normann, I.; Pollet, M., Proof development in OMEGA: The irrationality of square root of 2, (Kamareddine, F., Thirty Five Years of Automating Mathematics. Thirty Five Years of Automating Mathematics, Kluwer Applied Logic series (2003), Kluwer Academic Publishers) · Zbl 1023.68660 |
| [50] | (Simmons, R.; Veloso, M.; Smith, S., Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems (AIPS-98). Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems (AIPS-98), Pittsburgh, PEN (1998), AAAI Press: AAAI Press Menlo Park, CA) |
| [51] | G. Sutcliffe, D. Seyfang, Smart selective competition parallelism ATP, in: A. Kumar, I. Russell (Eds.), Proceedings of the 12th International Florida Artificial Intelligence Research Symposium (FLAIRS-99), Orlando, Florida, USA, 1999, pp. 341-345; G. Sutcliffe, D. Seyfang, Smart selective competition parallelism ATP, in: A. Kumar, I. Russell (Eds.), Proceedings of the 12th International Florida Artificial Intelligence Research Symposium (FLAIRS-99), Orlando, Florida, USA, 1999, pp. 341-345 |
| [52] | Veloso, M.; Carbonell, J.; Perez, M.; Borrajo, D.; Fink, E.; Blythe, J., Integrating planning and learning: The prodigy architecture, Journal of Experimental and Theoretical Artificial Intelligence, 7, 1, 81-120 (1995) · Zbl 0939.68830 |
| [53] | Weidenbach, Ch., SPASS: Version 0.49, Special Issue on the CADE-13 Automated Theorem Proving System Competition. Special Issue on the CADE-13 Automated Theorem Proving System Competition, Journal of Automated Reasoning, 18, 2, 247-252 (1997) |
| [54] | (Weiss, G., Multiagent Systems: A Modern Approach to Distributed Artificial Intelligence (1999), MIT Press: MIT Press Cambridge, MA) |
| [55] | Weld, D., An introduction to least commitment planning, AI Magazine, 15, 4, 27-61 (1994) |
| [56] | Wilkins, D.; desJardins, M., A call for knowledge-based planning, Artificial Intelligence, 22 (2001) |
| [57] | D. Wilkins, K. Myers, A multiagent planning architecture, in: [50]; D. Wilkins, K. Myers, A multiagent planning architecture, in: [50] |
| [58] | D. Wilkins, K. Myers, M. desJardins, P. Berry, Multiagent planning architecture, Tech. rep., Stanford Research Institute (SRI), 1997; D. Wilkins, K. Myers, M. desJardins, P. Berry, Multiagent planning architecture, Tech. rep., Stanford Research Institute (SRI), 1997 |
| [59] | Wolf, A., Strategy selection for automated theorem proving, (Giunchiglia, F., Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the 8th International Conference (AIMSA’98). Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the 8th International Conference (AIMSA’98), Sozopol, Bulgaria. Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the 8th International Conference (AIMSA’98). Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the 8th International Conference (AIMSA’98), Sozopol, Bulgaria, LNAI, vol. 1480 (1998), Springer-Verlag: Springer-Verlag Germany), 452-465 · Zbl 0903.00073 |
| [60] | Zhang, J.; Zhang, H., SEM: A system for enumerating models, (Mellish, C., Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI). Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI), Montreal, Canada (1995), Morgan Kaufmann: Morgan Kaufmann San Mateo, CA), 298-303 |
| [61] | J. Zimmer, S. Autexier, The mathserve system for semantic reasoning with web services, in: IJCAR, 2006; J. Zimmer, S. Autexier, The mathserve system for semantic reasoning with web services, in: IJCAR, 2006 |
| [62] | Zimmer, J.; Melis, E., Constraint solving for proof planning, Journal of Automated Reasoning, 33, 1, 51-88 (2004) · Zbl 1071.68093 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
