Abstract
An adaptative theorem prover is a system able to modify its current set of inference rules in order to improve its performance on a specific domain. We address here the issue of the generation of inference rules, without considering the selection and deletion issues. We especially develop the treatment of repeating events within a proof. We specify a general representation for objects to be learned in this framework, that is macro-connectives and macro-inference-rules and show how they may be generated from the primitive set of inference rules. Our main contribution consists to show that a form of analytical, static learning, is possible in this domain.
Chapter PDF
References
Belleannée C. "Improving deduction in a sequent calculus". Proc of the 8th biennal conference of the CSCSI", pp 220–226, Ottawa, may 1990.
Belleannée C. "Vers un démonstrateur adaptatif". Thèse de l'Université de RennesI, Jan 1991.
Cheng P. & Carbonell J. "The FERMI system: Inducing Iterative Macro-operators from Experience". Proc. of AAAI, 1986.
Cohen W. "A Technique for Generalizing Number in Explanation Based Learning". ML TR 19, Rutgers University, Sept 1987.
Cohen W. "Generalising Number and Learning from Multiple Examples in Explanation Based Learning". Proc. of 5th ICML, pp256–269, Morgan Kaufmann, Los Altos, Calif. 1988.
Fikes R., Hart P. & Nilsson N. "Learning and Executing Generalized Robot Plans". A.I. 3, pp 251–288, 1972.
Gallier J.H. "Logic for Computer Science: Foundations of Automatic Theorem Proving". Harper & Rown, New York, 1986.
Greenwood R.E. & Gleason A.M. "Combinatorial relations and chromatic graphs" Combinatorial Journal 7, 1955
Iba G. "A Heuristic Approach to the Discovery of Macro-operators". Machine Learning 3, pp 285–317, 1989.
Korf R. "Learning to Solve Problems by searching for macro-operators". PhD Thesis Carnegie Mellon University, 1983.
Korf R. "Macro-operators: A Weak Method for Learning". A I 26, pp35–77, 1985.
Minton S. "Learning Effective Search Control Knowledge: an Explanation Based Approach". PhD Thesis Carnegie Mellon University, 1988.
O'Rorke P. "LT revisited: Experimental results of applying explanation-based learning to the logic of principia mathematica". 4th IWML Irvine, 1987.
Pastre. D "Muscadet: An Automatic Theorem Proving System Using Knowledge and Meta-knowledge in Mathematics". Artificial Intelligence, vol 38, 1989 pp 257–318.
Porter.B "Learning Problem Solving". PhD Thesis University of California, Irvine 1984.
Prieditis A. "Discovery of Algorithms from Weak Methods". Proc. of International Meeting on Advances in Learning, Les Arcs France, 1986.
Schur I. "Über die kongruenz xm+ym=zm mod p" Jber Deutsch Verein 25, pp114–116. 1916
Shavlik J. & Dejong G. "An Explanation-Based Approach to Generalising Number". Proc. of IJCAI-87, Milan, Italy, pp236–238, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Belleannee, C., Nicolas, J. (1991). Static learning for an adaptative theorem prover. In: Kodratoff, Y. (eds) Machine Learning — EWSL-91. EWSL 1991. Lecture Notes in Computer Science, vol 482. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017022
Download citation
DOI: https://doi.org/10.1007/BFb0017022
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53816-5
Online ISBN: 978-3-540-46308-5
eBook Packages: Springer Book Archive