Simultaneous Search in Connection Tableau Calculi by Means of Disjunctive Constraints

Automatedtheorem proving with connection tableau calculi imposessearch problemsin tremendoussearch spaces. In this paper, wepresent a newapproachto search space reduction in connection tableau calculi. In our approachstructurally similar parts of the search space are compressedby meansof disjunctive constraints. Wedescribe the necessary changesof the calculus, and wedevelopelaborate techniques for an efficient constraint processing. Moreover,wepresent an experimental evaluation of our approach.

• Type: Conference
• Year: 2000
• Where: FLAIRS
• Authors: Ortrun Ibens
• Keywords: Artificial Intelligence, Calculi Imposessearch Problemsin, Connection Tableau Calculi, FLAIRS 2000, Search Space