Relevancy based Use of Lemmas in Connection Tableau Calculi

Share
Author
Fuchs, M.
Pub. date
January 2000
Pages
255
Binding
softcover
Volume
227 of Dissertations in Artificial Intelligence
ISBN print
978-1-58603-123-7
Subject
Artificial Intelligence, Computer & Communication Sciences, Computer Science

Automated deduction is a fundamental research area in the field of artificial intelligence. The aim of an automated deduction system is to find a formal proof for a given goal based on given axioms. Essentially automated deduction can be viewed as a search problem which spans huge search spaces. One main thrust of research in automated deduction is the development of techniques for achieving a reduction of the search space.


A particularly promising approach for search space reduction relies on the integration of top-down and bottom-up reasoning. A possible approach employs bottom-up generated lemmas in top-down systems. Lemma use offers the possibility to shorten proofs and to overcome weaknesses of top-down systems like poor redundancy control. In spite of the possible advantages of lemma use, however, naive approaches for lemma integration even tend to slow down top-down systems. The main problem is the increased indeterminism in the search process. In this thesis important contributions for a successful application of lemmas in top-down deduction systems based on connection tableau calculi are made. New methods for lemma generation and for the estimation of the relevancy of lemmas are developed. As a practical contribution, the implementation of the new techniques leads to a powerful system for automated deduction which demonstrates the high potential of the new techniques.