Towards Full Automation of Deduction : A Case Study

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.