Toward an efficient equality computation in connection tableaux: A modification method without symmetry transformation: A preliminary report
Koji Iwanuma, Hidetomo Nabeshima, Katsumi Inoue · 2009
In this paper, we study an efficient equality computation in connection tableaux, and give a new variant of Brand, Bachmair-Ganzinger-Voronkov and Paskevich’s modification methods, where the symmetry elimination rule is never applied. As is well known, effective equality computing is very difficult in a top-down theorem proving framework such as connection tableaux, due to a strict restriction to re-writable terms. The modification method with ordering constraints is a wellknown remedy for top-down equality computation, and Paskevich adapted the method to connection tableaux. However the improved modification method still causes essentially redundant computation which originates in a symmetry elimination rule for equational clauses. The symmetry elimination may produce an exponential number of clauses from a given single clause, which inevitably causes a huge amount of redundant backtracking in connection tableaux. In this paper, we study a simple but effective remedy, that is, we abandon such symmetry elimination for clauses and instead introduce new equality inference rules into connection tableaux. These new inference rules have a possibility of achieving efficient equality computation, without losing the symmetry property of equality, which never cause redundant backtracking nor redundant contrapositive computation. We implemented the proposed methods in a sophisticated prover SOLAR which is originally designed to finding logical consequences, and show a preliminary experimental results for TPTP benchmark problems. This research is now in progress, thus the experimental results provided in this paper are tentative ones. 1