- author = "Marc Fuchs",
- title = "Relevancy based Use of Lemmas in Connection Tableau Calculi",
- school = "Technical University Munich",
- year = "2000",
- address = "Germany",
- month = jan,
- keywords = "genetic algorithms, genetic programming, Artificial Intelligence, Computer and Communication Sciences, Computer Science",
- volume = "227",
- series = "Dissertations in Artificial Intelligence",
- publisher = "IOS",
- isbn13 = "978-3-89838-227-4",
- isbn13 = "978-1-58603-123-7",
- timestamp = "Thu, 30 Jan 2020 14:55:16 +0100",
-
biburl = "
https://dblp.org/rec/books/daglib/0001380.bib",
- bibsource = "dblp computer science bibliography, https://dblp.org",
-
URL = "https://www.iospress.nl/book/relevancy-based-use-of-lemmas-in-connection-tableau-calculi/",
-
URL = "http://d-nb.info/958746656",
- size = "255 pages",
-
abstract = "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 nondeterminism 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.",
- notes = "is this GP?",
