Proof Search Optimizations for Non-clausal Connection Calculi
Author: Jens Otten
Paper Information
| Title: | Proof Search Optimizations for Non-clausal Connection Calculi |
| Authors: | Jens Otten |
| Proceedings: | PAAR papers |
| Editors: | Boris Konev, Josef Urban and Philipp Ruemmer |
| Keywords: | non-clausal theorem proving, optimization techniques, nanoCoP |
| Abstract: | ABSTRACT. The paper presents several proof search optimization techniques for non-clausal connection calculi. These techniques are implemented and integrated into the non-clausal connection prover nanoCoP. Their effectiveness is evaluated on the problems in the TPTP library. Together with a fixed strategy scheduling, these techniques are the basis of the new version 1.1 of nanoCoP. |
| Pages: | 9 |
| Talk: | Jul 19 11:30 (Session 132D: Automated Reasoning I) |
| Paper: |  |