Inference Rights for Controlling Search in Generating 
Theorem Provers

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

Abstract
We investigate the usage of so-called inference rights. We point 
out the problems arising from the inflexibility of 
existing approaches to heuristically
control the search of automated deduction systems, and we 
propose the application of inference rights that are 
well-suited for controlling the search more
flexibly. Moreover, inference rights allow for a mechanism of 
``partial forgetting'' of facts that is not realizable in the
most controlling aproaches.
We study theoretical foundations of inference rights as well as 
the integration of inference rights into already existing 
inference systems.
Furthermore, we present possibilities to control such modified 
inference systems in order to gain efficiency.
Finally, we report on experimental results obtained in the area 
of condensed detachment.

Keywords
condensed detachment, inference rights, partial forgetting
Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1996/
file: Fuchs.SR-96-12.ps.gz