Efficient Rule-Matching for Hyper-Tableaux

Over the past decades, a number of calculi for automated reasoning have been proposed that share some core features: 1. proofs are built in a tableau/sequent style as trees where nodes are labeled with literals, and 2. these proofs are expanded by interpreting the problem clause set as a set of rules, and requiring all negative literals in clauses to present on a branch for expansion. This applies to hyper-tableaux [2], MGTP [8], coherent logic [4, 5], and others. Existing implementations typically spend much of their time in the process of matching branch literals with the negative literals of the input clauses. We present an alternative to this matching process by applying a modified version of the Rete algorithm [7]. The Rete algorithm was developed in the 1970s for production systems in artificial intelligence. We exploit the similarities between the mentioned calculi and production systems in order to make the Rete algorithm solve the matching problem. We also investigate the effect of working on several independent branches present in tableau proof search but not in production systems. 9th International Workshop on the Implementation of Logics. Merida, 10.03.12 - 10.03.12