Abstract
In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver \({\mathcal C}o{\cal SIE}\).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aiba, A., Hasegawa, R.: Constraint Logic Programming System - CAL, GDCC and Their Constraint Solvers. In: Proc. of the Conference on Fifth Generation Computer Systems, ICOT, pp. 113–131 (1992)
Bartle, R.G., Sherbert, D.R.: Introduction to Real Analysis. John Wiley& Sons, New York (1982)
Benzmueller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J., Sorge, V.: OMEGA: Towards a Mathematical Assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249. Springer, Heidelberg (1997)
Boyer, R.S., Moore, J.S.: Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence (Logic and the Acquisition of Knowledge) 11 (1988)
Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310. Springer, Heidelberg (1988)
Bürckert, H.-J.: A Resolution Principle for Constrained Logics. Artifcial Intelligence 66(2) (1994)
Frühwirth, T.: Constraint Handling Rules. In: Podelski, A. (ed.) Constraint Programming: Basics and Trends. LNCS, vol. 910. Springer, Heidelberg (1995)
Jaffar, J., Lassez, J.-L.: Constraint Logic Programming. In: Proc. 14th ACM Symposium on Principles of Programming Languages (1987)
Mackworth, A.K.: Consistency in Networks of Relations. Artificial Intelligence 8, 99–118 (1977)
Melis, E.: AI-Techniques in Proof Planning. In: European Conference on Artificial Intelligence. Kluwer Academic, Dordrecht (1998)
Melis, E.: Combining Proof Planning with Constraint Solving. In: Proceedings of Calculemus and Types 1998. Electronic Proceedings (1998), http://www.win.tue.nl/math/dw/pp/calc/proceedings.html
Melis, E., Siekmann, J.H.: Knowledge-based Proof Planning. Artificial Intelligence 115(1), 65–105 (1999)
Melis, E., Sorge, V.: Employing External Reasoners in Proof Planning. In: Armando, A., Jebelean, T. (eds.) Calculemus 1999 (1999)
Mittal, S., Falkenhainer, B.: Dynamic Constraint Satisfaction Problems. In: Proceedings of the 10th National Conference on Arti ficial Intelligence, AAAI 1990, Boston, MA, pp. 25–32 (1990)
Monfroy, E., Ringeissen, C.: SoleX: a Domain-Independent Scheme for Constraint Solver Extension. In: Calmet, J., Plaza, J. (eds.) AISC 1998. LNCS (LNAI), vol. 1476, p. 222. Springer, Heidelberg (1998)
The Mozart Consortium. The Mozart Programming System, http://www.mozart-oz.org/
Prawitz, D.: Natural Deduction - A Proof Theoretical Study. Almquist and Wiksell, Stockholm (1965)
Smolka, G.: The Oz programming model. In: van Leeuwen, J. (ed.) Current Trends in Computer Science. Springer, Hidleberg (1995)
Stickel, M.K.: Automated Deduction by Theory Resolution. In: Proc. of the 9th International Joint Conference on Artificial Intelligence (1985)
Stolzenburg, F.: Membership Constraints and Complexity in Logic Programming with Sets. In: Baader, F., Schulz, U. (eds.) Frontiers in Combining Systems. Kluwer Academic, Dordrecht (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melis, E., Zimmer, J., Müller, T. (2000). Integrating Constraint Solving into Proof Planning. In: Kirchner, H., Ringeissen, C. (eds) Frontiers of Combining Systems. FroCoS 2000. Lecture Notes in Computer Science(), vol 1794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720084_3
Download citation
DOI: https://doi.org/10.1007/10720084_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67281-4
Online ISBN: 978-3-540-46421-1
eBook Packages: Springer Book Archive