## Abstract

Proof planning is an application of AI planning to theorem proving that employs plan operators that encapsulate mathematical proof techniques. Many proofs require the instantiation of variables; that is, mathematical objects with certain properties have to be constructed. This is particularly difficult for automated theorem provers if the instantiations have to satisfy requirements specific for a mathematical theory, for example, for finite sets or for real numbers, because in this case unification is insufficient for finding a proper instantiation. Often, constraint solving can be employed for this task. We describe a framework for the integration of constraint solving into proof planning that combines proof planners and stand-alone constraint solvers. Proof planning has some peculiar requirements that are not met by any off-the-shelf constraint-solving system. Therefore, we extended an existing propagation-based constraint solver in a generic way. This approach generalizes previous work on tackling the problem. It provides a more principled way and employs existing AI technology.

## Keywords

automated reasoning proof plans constraint satisfaction## Preview

Unable to display preview. Download preview PDF.

## References

- Autexier, S. and Hutter, D. (1997) Equational proof-planning by dynamic abstraction, in M. Bonacina and U. Furbach (eds.),
*Proceedings of the First Workshop on First-Order Theorem Proving (FTP97)*, RISC-Linz Report Series No. 97-50, Linz, Austria. Google Scholar - Baader, F. and Nipkow, T. (1998)
*Term Rewriting and All That*, Cambridge University Press, Cambridge, UK. Google Scholar - Bartle, R. and Sherbert, D. (1982)
*Introduction to Real Analysis*, Wiley, New York. Google Scholar - Baumgartner, P. and Stolzenburg, F. (1995) Constraint model elimination and a PPT-implementation, in P. Baumgartner, R. Haehnle and J. Posegga (eds.),
*Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods*, Springer-Verlag, pp. 201–216. Google Scholar - Beeson, M. (1989) Logic and computation in Mathpert: An expert system for learning mathematics, in E. Kaltofen and S. Watt (eds.),
*Computers and Mathematics ‘89*, Springer, pp. 202–214. Google Scholar - Beeson, M. (1998) Automatic generation of epsilon-delta proofs of continuity, in J. Calment and J. Plaza (eds.),
*Artificial Intelligence and Symbolic Computation*, Springer-Verlag, pp. 67–83. Google Scholar - Bledsoe, W. W. (1990) Challenge problems in elementary calculus,
*J. Automated Reasoning***6**, 341–359. Google Scholar - Bledsoe, W. W., Boyer, R. and Henneman, W. (1972) Computer proofs of limit theorems,
*Artificial Intelligence***3**(1), 27–60. Google Scholar - Brelaz, D. (1979) New methods to colour the vertices of a graph,
*Comm. ACM***22**(4), 251–256. Google Scholar - Bundy, A. (1988) The use of explicit plans to guide inductive proofs, in E. Lusk and R. Overbeek (eds.),
*Proceedings of the 9th International Conference on Automated Deduction (CADE-9)*(Argonne), Lecture Notes in Comput. Sci. 310, Springer, pp. 111–120. Google Scholar - Bundy, A., Stevens, A., van Harmelen, F., Ireland, A. and Smaill, A. (1993) Rippling: A heuristic for guiding inductive proofs,
*Artificial Intelligence***62**, 185–253. Also available from Edinburgh as DAI Research Paper No. 567. Google Scholar - Bürckert, H.-J. (1994) A resolution principle for constrained logics,
*Artificial Intelligence***66**, 235–271. Google Scholar - Collins, G. (1975) Quantifier elimination for real closed fields by cylindrin algebraic decomposition, in
*Second GI Conference on Automata Theory and Formal Languages*, Lecture Notes in Comput. Sci. 33, Springer-Verlag, pp. 134–183. Google Scholar - Dechter, R. and Dechter, A. (1988) Belief maintenance in dynamic constraint networks, in
*Proceedings of the Seventh Annual Conference of the American Association of Artificial Intelligence*, pp. 37–42. Google Scholar - Dupre, D. (2000) Automated theorem proving by integrating proving, solving and computing, Ph.D. thesis, Forschungsinstitut für symbolisches Rechnen, Technisch-Naturwissenschaftche Fakultät, Johannes Kepler Universität Linz. Google Scholar
- Fikes, R. and Nilsson, N. (1971) STRIPS: A new approach to the application of theorem proving to problem solving,
*Logic and Comput. Sci.***2**, 189–208. Google Scholar - Gentzen, G. (1935) Untersuchungen über das logische Schließen I & II,
*Math. Zeitschrift***39**, 176–210, 572–595. Google Scholar - Ghallab, M. and Laruelle, H. (1994) Representation and control in IxTeT, a temporal planner, in
*Proceedings of the Second International Conference on Artificial Intelligence Planning (AIPS)*. Google Scholar - Giunchiglia, F. and Walsh, T. (1992) A theory of abstraction,
*Artificial Intelligence***57**, 323–390. Google Scholar - Haralick, R. and Elliot, G. (1980) Increasing tree search efficiency for constraint satisfaction problems,
*Artificial Intelligence***14**, 263–313. Google Scholar - Haslum, P. and Geffner, H. (2001) Heuristic planning with time and resources, in A. Cesta and D. Borrajo (eds.),
*Proceedings of the 6th European Conference on Planning*, pp. 121–132. Google Scholar - Inc., I. (1999) ILOG solver user’s manual version 4.4, ILOG Inc., Mountain View, CA. Google Scholar
- Jaffar, J. and Lassez, J.-L. (1987) Constraint logic programming, in
*Proceedings 14th ACM Symposium on Principles of Programming Languages*. Google Scholar - Jonsson, A., Morris, P., Muscettola, N. and Rajan, K. (2000) Planning in interplanetary space: Theory and practice, in S. Chien, S. Kambhampati and C. Knoblock (eds.),
*Proceedings of the Second International Conference on Artificial Intelligence Planning (AIPS) 2000*, AAAI, pp. 177–186. Google Scholar - Kambhampati, S. (1996) Refinement planning: Status and prospectus, in
*Proceedings of the AAAI-96*, Morgan Kaufmann, pp. 1331–1336. Google Scholar - Kautz, H. and Walser, J. (1999) State-space planning by integer optimization,
*The Knowledge Engineering Review***15**(1), 526–533. Google Scholar - Laborie, P. (2001) Algorithms for propagating resource constraints in AI planning and scheduling: Existing approaches and new results, in A. Cesta and D. Borrajo (eds.),
*Proceedings of the Sixth European Conference on Planning, ECP-01*, pp. 205–216. Google Scholar - Leron, U. (1985) Heuristic presentations: The role of structuring,
*For the Learning of Mathematics***5**(3), 7–13. Google Scholar - Mackworth, A. K. (1977) Consistency in networks of relations,
*Artificial Intelligence***8**, 99–118. Google Scholar - McCune, W. (1990) Otter 2.0, in M. E. Stickel (ed.),
*Proceedings of the 10th International Conference on Automated Deduction (CADE–10)*(Kaiserslautern, Deutschland), Lecture Notes in Artif. Intell. 449, Springer-Verlag, Berlin, pp. 663–664. Google Scholar - Meier, A., Pollet, M. and Sorge, V. (2002) Comparing approaches to the exploration of the domain of residue classes,
*J. Symbolic Comput., Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems***34**(4), 287–306. S. Linton and R. Sebastiani, eds. Google Scholar - Melis, E. (1996) Island planning and refinement, in J. Hendler and J. Koehler (eds.),
*Control of Search in AI Planning*. Google Scholar - Melis, E. (1998a) AI-techniques in proof planning, in
*European Conference on Artificial Intelligence (ECAI-98)*(Brighton), Kluwer, pp. 494–498. Google Scholar - Melis, E. (1998b) Combining proof planning with constraint solving, in
*Proceedings of Calculemus and Types’98*. Google Scholar - Melis, E. (1998c) The “Limit” domain, in R. Simmons, M. Veloso and S. Smith (eds.),
*Proceedings of the Fourth International Conference on Artificial Intelligence in Planning Systems (AIPS-98)*. Google Scholar - Melis, E. and Meier, A. (2000) Proof planning with multiple strategies, in J. Loyd, V. Dahl, U. Furbach, M. Kerber, K. Lau, C. Palamidessi, L. Pereira and Y. S. P. Stuckey (eds.),
*First International Conference on Computational Logic*, Lecture Notes in Artif. Intell. 1861, Springer-Verlag, pp. 644–659. Google Scholar - Melis, E. and Siekmann, J. (1999) Knowledge-based proof-planning,
*Artificial Intelligence***115**(1), 65–105. Google Scholar - Monfroy, E. and Ringeissen, C. (1998) SoleX: A domain-independent scheme for constraint solver extension, in J. Calmet and J. Plaza (eds.),
*Artificial Intelligence and Symbolic Computation AISC’98*, Springer, pp. 222–233. Google Scholar - Mozart (2001)
*Mozart Consortium. The Mozart Programming System 1.2.0*, Documentation and system available from http://www.mozart-oz.org. - Müller, T. (2000) Promoting constraints to first-class status, in
*Proceedings of the First International Conference on Computational Logic – CL2000*(London), Springer-Verlag. Google Scholar - Muscettola, N. (1994) HSTS: Integrating planning and scheduling, in M. Zweben and M. Fox (eds.),
*Intelligent Scheduling*, Morgan Kaufmann, pp. 169–212. Google Scholar - Myers, K., Smith, S., Hildrum, D., Jarvis, P. and de Lacaze, R. (2001) Integrating planning and scheduling through adaptation of resource intensity estimates, in
*Proceedings of the 6th European Conference on Planning*, pp. 133–144. Google Scholar - Penberthy, J. and Weld, D. (1994) Temporal planning with continuous change, in
*Proceedings of the 12th National Conference on AI*, pp. 1010–1015. Google Scholar - Schulte, C. (2000) Programming constraint services, Doctoral dissertation, Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät I, Fachrichtung Informatik, Saarbrücken, Germany. Google Scholar
- Siekmann, J., Benzmüller, C., Brezhnev, V., Cheikhrouhou, L., Fiedler, A., Franke, A., Horacek, H., Kohlhase, M., Meier, A., Melis, E., Moschner, M., Normann, I., Pollet, M., Sorge, V., Ullrich, C., Wirth, C. and Zimmer, J. (2002) Proof development with ΩMEGA, in A. Voronkov (ed.),
*Proceedings of the 18th Conference on Automated Deduction (CADE-18)*(Copenhagen, Denmark), Lecture Notes in Artif. Intell. 2392, Springer-Verlag, Berlin, pp. 144–149. Google Scholar - Smith, D., Frank, J. and Jonsson, A. (2000) Bridging the gap between planning and scheduling,
*Knowledge Engineering Review***15**(1), 61–94. Google Scholar - Smolka, G. (1995) The Oz programming model, in J. van Leeuwen (ed.),
*Current Trends in Computer Science*, Lecture Notes in Comput. Sci. 1000, Springer, Berlin, pp. 324–343. Google Scholar - Sorge, V. (2000) Non-trivial computations in proof planning, in H. Kirchner and C. Ringeissen (eds.),
*Frontiers of Combining Systems: Third International Workshop, FroCoS 2000*(Nancy, France), Lecture Notes in Comput. Sci. 1794, Springer-Verlag, Berlin, pp. 121–135. Google Scholar - Stickel, M. (1985) Automated deduction by theory resolution, in
*Proceedings of the 9th International Joint Conference on Artificial Intelligence*, pp. 1181–1186. Google Scholar - Sutcliffe, G., Suttner, C. and Yemenis, T. (1994) The TPTP problem library, in A. Bundy (ed.),
*Proceedings of the 12th Conference on Automated Deduction*(Nancy, France), Springer-Verlag. Google Scholar - Tate, A. (1996) Representing plans as a set of constraints – the I-N-OVA model, in
*Proceedings of the Third International Conference on Artificial Intelligence Planning Systems (AIPS-96)*. Google Scholar - Wolfman, S. and Weld, D. (1999) Combining linear programming and satisfiability solving for resource planning,
*The Knowledge Engineering Review***15**(1). Google Scholar - Wolfram, S. (1996)
*The Mathematica Book: Version 3.0*, 3rd edn, Wolfram Media, Inc., Champaign, IL. Google Scholar - Yoshida, T., Bundy, A., Green, I., Walsh, T. and Basin, D. (1994) Coloured rippling: An extension of a theorem proving heuristic, in
*Proceedings of the 11th ECAI*(Amsterdam, The Netherlands), pp. 85–89. Google Scholar - Zimmer, J. (2000) Constraintlösen für Beweisplanung, Master’s thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany. In German. Google Scholar
- Zimmer, J. and Kohlhase, M. (2002) System description: The MathWeb software bus for distributed mathematical reasoning, in A. Voronkov (ed.),
*Proceedings of the 18th International Conference on Automated Deduction*, Springer-Verlag, pp. 139–143. Google Scholar