Relevancy-based use of lemmas in connection tableau calculi (Diss., TU München, 1999) (Q2726303)

The main objective of automated deduction is, given a statement, to find its proof from the given theorems. In real (human) proofs, the success comes from a combination of the following two activities. The main emphasis is on the attempts to analyze the statement that we want to prove, so that eventually, we either come up with a proof of this statement, or with the proofs for auxiliary statements (``subgoals'') from which the desired statement follows. In mathematical texts, the statement that we are proving is placed at the top of the page, with the proof following it; as a result, this approach is called top-down. In some cases, this top-down approach works by itself, but often, what helps is an ongoing mathematical activity of looking at the axioms and seeing what we can deduce from them. Usually, when we prove a theorem, we do not reduce it all the way to the axioms; instead, we usually reduce it to some statements that have been proven before for a different purpose. In other words, the effectiveness of human theorem proving is enhanced by a fruitful combination of a top-down approach (from desired statement to axioms) and a ``bottom-up'' approach (from axioms to the desired statement). NEWLINENEWLINENEWLINEIt view of this effectiveness, researchers have been trying to incorporate a similar combination into automatic deduction algorithms. Until recently, however, these attempts have not been successful: although sometimes, the bottom-up approach does lead to helpful intermediate statement (``lemmas''), in general, most of thus generated statements are irrelevant, and, as a result, the overall computation time for the combined method increases instead of decreasing. NEWLINENEWLINENEWLINEThe author describes the first successful attempt to combine top-down and bottom-up approaches. To make this combination successful, the author does not simply let the bottom-up generator randomly prove different (mostly irrelevant) corollaries (``lemmas'') of given axioms. Instead, the author tunes up the probabilities of the corresponding lemma generator in such a way that these lemmas are most relevant -- i.e., most helpful -- in proving the desired statement. As a criterion of relevancy of the lemma generator, the author gauges how shorter the inference chains become for subgoals (generated during the top-down stage) if we use the resulting lemmas. To find the parameters of the lemma generator that optimizes this efficiency measure, the author uses genetic programming and evolutionary computation. The result is an efficient automatic deduction system that shows a great potential of the combination idea.