Advertisement

Journal of Automated Reasoning

, Volume 33, Issue 1, pp 51–88 | Cite as

Constraint Solving for Proof Planning

  • Jürgen Zimmer
  • Erica Melis
Article

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.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. Baader, F. and Nipkow, T. (1998) Term Rewriting and All That, Cambridge University Press, Cambridge, UK. Google Scholar
  3. Bartle, R. and Sherbert, D. (1982) Introduction to Real Analysis, Wiley, New York. Google Scholar
  4. 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
  5. 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
  6. 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
  7. Bledsoe, W. W. (1990) Challenge problems in elementary calculus, J. Automated Reasoning 6, 341–359. Google Scholar
  8. Bledsoe, W. W., Boyer, R. and Henneman, W. (1972) Computer proofs of limit theorems, Artificial Intelligence 3(1), 27–60. Google Scholar
  9. Brelaz, D. (1979) New methods to colour the vertices of a graph, Comm. ACM 22(4), 251–256. Google Scholar
  10. 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
  11. 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
  12. Bürckert, H.-J. (1994) A resolution principle for constrained logics, Artificial Intelligence 66, 235–271. Google Scholar
  13. 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
  14. 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
  15. 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
  16. 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
  17. Gentzen, G. (1935) Untersuchungen über das logische Schließen I & II, Math. Zeitschrift 39, 176–210, 572–595. Google Scholar
  18. 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
  19. Giunchiglia, F. and Walsh, T. (1992) A theory of abstraction, Artificial Intelligence 57, 323–390. Google Scholar
  20. Haralick, R. and Elliot, G. (1980) Increasing tree search efficiency for constraint satisfaction problems, Artificial Intelligence 14, 263–313. Google Scholar
  21. 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
  22. Inc., I. (1999) ILOG solver user’s manual version 4.4, ILOG Inc., Mountain View, CA. Google Scholar
  23. Jaffar, J. and Lassez, J.-L. (1987) Constraint logic programming, in Proceedings 14th ACM Symposium on Principles of Programming Languages. Google Scholar
  24. 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
  25. Kambhampati, S. (1996) Refinement planning: Status and prospectus, in Proceedings of the AAAI-96, Morgan Kaufmann, pp. 1331–1336. Google Scholar
  26. Kautz, H. and Walser, J. (1999) State-space planning by integer optimization, The Knowledge Engineering Review 15(1), 526–533. Google Scholar
  27. 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
  28. Leron, U. (1985) Heuristic presentations: The role of structuring, For the Learning of Mathematics 5(3), 7–13. Google Scholar
  29. Mackworth, A. K. (1977) Consistency in networks of relations, Artificial Intelligence 8, 99–118. Google Scholar
  30. 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
  31. 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
  32. Melis, E. (1996) Island planning and refinement, in J. Hendler and J. Koehler (eds.), Control of Search in AI Planning. Google Scholar
  33. Melis, E. (1998a) AI-techniques in proof planning, in European Conference on Artificial Intelligence (ECAI-98) (Brighton), Kluwer, pp. 494–498. Google Scholar
  34. Melis, E. (1998b) Combining proof planning with constraint solving, in Proceedings of Calculemus and Types’98. Google Scholar
  35. 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
  36. 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
  37. Melis, E. and Siekmann, J. (1999) Knowledge-based proof-planning, Artificial Intelligence 115(1), 65–105. Google Scholar
  38. 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
  39. Mozart (2001) Mozart Consortium. The Mozart Programming System 1.2.0, Documentation and system available from http://www.mozart-oz.org.
  40. 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
  41. Muscettola, N. (1994) HSTS: Integrating planning and scheduling, in M. Zweben and M. Fox (eds.), Intelligent Scheduling, Morgan Kaufmann, pp. 169–212. Google Scholar
  42. 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
  43. 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
  44. Schulte, C. (2000) Programming constraint services, Doctoral dissertation, Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät I, Fachrichtung Informatik, Saarbrücken, Germany. Google Scholar
  45. 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
  46. Smith, D., Frank, J. and Jonsson, A. (2000) Bridging the gap between planning and scheduling, Knowledge Engineering Review 15(1), 61–94. Google Scholar
  47. 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
  48. 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
  49. Stickel, M. (1985) Automated deduction by theory resolution, in Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 1181–1186. Google Scholar
  50. 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
  51. 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
  52. Wolfman, S. and Weld, D. (1999) Combining linear programming and satisfiability solving for resource planning, The Knowledge Engineering Review 15(1). Google Scholar
  53. Wolfram, S. (1996) The Mathematica Book: Version 3.0, 3rd edn, Wolfram Media, Inc., Champaign, IL. Google Scholar
  54. 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
  55. Zimmer, J. (2000) Constraintlösen für Beweisplanung, Master’s thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany. In German. Google Scholar
  56. 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

Copyright information

© Kluwer Academic Publishers 2004

Authors and Affiliations

  1. 1.Arbeitsgruppe Siekmann (AGS), Fachbereich Informatik (FB 14)Universität des SaarlandesSaarbrückenGermany
  2. 2.Competence Centre for eLearningGerman Research Center for Artificial Intelligence (DFKI)SaarbrückenGermany

Personalised recommendations