Using Term Space Maps to Capture Search Control Knowledge in Equational Theorem Proving
Stephan Schultz, Felix Brandt · The Florida AI Research Society · 1999
We describe a learning inference control heuristic for an equationM theorem prover. Tile heuristic scl~’ts a number of problems similar to a new problem from a knowledge base and compiles information about good search decisions for the~ selected problems into a term space map, which is used to evaluate the searcJl alternatives ~tt an importmit choice point in the theerent prover. Experimems on the TPTP problem library show the improvements possible with this new approach. Introduction Automated theorem provers (ATP systems) are programs tilat try to prove tile validity of a given statement under the assumption of a ~t of axioms. They are currently beginning to make inroads into industrial anti scientific fields outside tile core deduction community. Systems likc DISCOUNT (Denzinger, Kronenburg, & Schulz 1997) and SETHEO (Letz ctal. 1992) are being used for the verification of protocols (Schumann 1997), the retrieval of software components (Fischer & Schumann 1997) and inathenmtical theorems (Dahn & Wernhard 1997) from libraries. Recent successes of theorem provers, most visibly tim proof of the Robbins algebra problem by EQP (McCune 1997), demonstrate the power of current theorem proving technology.. Itowever, despite the fact that ATP systems arc able to perform basic operations at an enormous rate and can solve nlost silnl)le problems nlucil faster than an,) hulnan expert, they still fail on lnauy tasks routinely solved by mathematicians. We believe that tills is dllr~ to tim differences in how humans and coml)uters search for proofs. Human beings usually develop botil conscious and intuitive knowledge about which operations to apply in a given situation to reach a given target. Most theorem proving programs, on tile other hand. use ve.ry little of this kiud of search, control knowledge and rely on a set of fixed: preprogrmnumd search control heuristics. Optimization of the theorem prover for a given set of problems consists in the selection of an existing heuristic (with suitable panuneters), or even in the manual coding of a new tleuristic based on tim experience of a user witll the domain. Botll tasks are tedious, and expensive in terms of time and manpower. Our aim is Copyright (~)1999, American Association for Artificial Intelligence (www.,-mai.org). All rights reserved. to adapt a th(x~rem prover to a domain or a problem by learning from examples of successfifl proof seaxehes. For this purpose, we store inforination about good sear(~l decisions for problems in a given domain, l%r each new problem, we select a couple of previous exampies with similar features aal(1 t.ompile tim associated infornmtion into a term space map, whietl in turn defines a searctl guiding tmuristic for the new problenl. This work solves some problems encountered with a similar approach without example selection (Denzinger & Schulz 1996a). In tills paper, we first give a very short introduction into equational theorem proving and the associated search problem. We then describe how we generate ~ul(t store examples of good search decisions. The next section describes how we select training exanlples for a given new problem and how we use these cxanlpies to create a suitable heuristic evaluation function. Finally, we preseut experimcmal r~ull,s with the theorem prover DISCOUNT 2.1/TSM aud (:(mclude. Equational Theorem Proving The aim of equational t hc~)rcm proving is to show timt two terms s and t can be transformed into each otlmr by the application of equations from a set. of axioms E, i.e. riley try to show that s = t is a logical eonse.quence of E. This problem is only semi-deeidat)le, thereibre all proof pr, Jcedures have to search for a proof in an infinite search space. Most successful tll~)retll provers (e.g. DISCOUNT or Waldmeister (Hillenbrand, Buch, & Fettig 1996)) for thi,s kind of deduction are based on unfailin.q completion (Bachmair, Ders(’howitz, PIMstcd 1989). We assume that the re~gler is familiar with most basic teruls and ,)nly give a very short introduction to the necessary concepts. So0. (Baader Nipkow 1998) for a lnore comprehensive introduction. The set Term(F.. V) of terms ,)v(,r a tinite set of flmction symbols F (with a,usociated arities) and an cnumcrable set of variables V is defined as usually. An equation s = t is a pair of terms. ,~,r consider equatiolm to be symmetrical. A rule l ---~ r is all oriented equation such that all variables in r also occur is l. A ground reduction o~zle.rin9 > is a Noetimrimt partial ordering that is stable with respect to tim term structure and substitutions and total on ground terms. A 244 SCHULZ From: Proceedings of the Twelfth International FLAIRS Conference. Copyright © 1999, AAAI (www.aaai.org). All rights reserved. rule l -~ r is said to be compatible with > if I > r. Rules and equations can be applied to terms by matching one side onto a subterm and replacing this subterm with the instantiated other side. We usually only allow simplifications, i.e. applications f rules and equations that replace larger terms by smaller terms. Our prover, DISCOUNT, takes a set of equations E, a goal s -t and a ground reduction ordering > as input. It tries to decide the equality of s and ~ modulo E by incrementally generating a ground confluent and terminating set of rules and equations equivalent to K If certain fairness criteria are ensured, it. can be guaranteed that any valid equation s = t can be proven after a finite number of inferences by simplifying s and t as far as possible (i.e. to compute their normal forms) with each successive system of rules and equations. The proof procedure of DISCOUNT is based on two basic inference rules: Ordered unit paramodulation (the building of critical pairs) and rewriting. Ordered unit paramodulation generates new equation by overlapping a maximal side of one rule or equation into a maximal side of another rule or equation. Rewriting, on the other hand, is a contracting inference. It does not create new equations, but allows the simplification of an existing rule or equation if certain conditions are fulfilled. We use three sets of term pairs to represent the current state of a completion process: A set E of processed, but unorientable equations, a set R of rules (processed and oriented equations) and a set CP of unprocessed equations. The completion algorithm will start out with empty sets R and E, and the initial axioms in CP. It will examine each equation in CP in turn, reduce it to normal form with respect to E and R, use it to build new critical pairs (to be added to CP) and to eliminate redundancies from R and E by simplification. It will then be added to either R (if it can be oriented according to >) or E. The order in which equations from CP are processed is one of the most crucial points for the performance of the prover. This order is determined by an heuristic evaluation function, which assigns a weight to each fact. The prover always selects the fact with the lowest weight for processing. Experimentai results show that all proofs found by DISCOUNT at all can be reproduced in sub-second times if a good evaluation function is used. However, using standard search heuristics (weighting equations according to the number of symbol in the terms) the prover typically spends more than 99% of the processing time on inferences not contributing to the proof (see (Denzinger & Schulz 1996b) more detailed results). Our aim is to improve the overall performance of the prover by controlling this choice point with a learning evaluation function. Knowledge Acquisition and