Connection Tableau Calculi with Disjunctive Constraints |
| |
Authors: | Ibens Ortrun |
| |
Affiliation: | (1) Institut für Informatik Technische, Universität München, Germany |
| |
Abstract: | Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo. |
| |
Keywords: | Automated theorem proving tableau calculi connection tableau calculi first-order constraint solvin |
本文献已被 SpringerLink 等数据库收录! |