Towards Full Automation of Deduction: A Case Study

Matthias Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 67653 Kaiserslautern
Germany
E-mail: fuchs@informatik.uni-kl.de

Abstract
We present first steps towards fully automated deduction that
merely requires the user to submit proof problems and pick up
results. Essentially, this necessitates the automation of the
crucial step in the use of a deduction system, namely choosing
and configuring an appropriate search-guiding heuristic.
Furthermore, we motivate why learning capabilities are pivotal
for satisfactory performance. The infrastructure for automating
both the selection of a heuristic and integration of learning
are provided in form of an environment embedding the "core"
deduction system.

We have conducted a case study in connection with a deduction
system based on condensed detachment. Our experiments with a
fully automated deduction system `AUTOCODE' have produced
remarkable results. We substantiate AUTOCODE's encouraging
achievements with a comparison with the renowned theorem prover
OTTER. AUTOCODE outperforms OTTER even when assuming very
favorable conditions for OTTER

Keywords
condensed detachment, fully automated deduction,
learning search heuristics

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1996/
file: Fuchs.SR-96-07.ps.gz