On the Treatment of Equivalence Connectives in Automated Theorem Proving

Abstract

For automated theorem proving it is shown in [1] how formulas containing equivalence connectives can be treated so as to avoid excessive storage space explosion during runtime. The approach is logically based and is not an implementation technique. In [1] the approach is first restricted to the class of propositional formulas in which, apart from negation, only the equivalence and non-equivalence connectives appaer. For example take ((A ⇔ B) ⇎ C) ⇔ (D ⇎ E), where A,B,C,D,E are literals. Although computing time is not reduced the storage space required to prove this formula not valid is no more than the formula itself. First, in one pass, the literals are found and the proof can be carried out simply by placing negation connectives in front of the literals (i.e. the literals are ‘weighted’ with negations depending upon the number of ⇔’s and ⇎’s). Then the weighted literals are treated as a conjunction. If this conjunction does not contain a contradiction then the procedure stops. Otherwise the weighting and testing of the resulting conjunction for a contradiction is done 2^n-1 times, where n is the number of literals.If conjuncions are found each time then the negation of the given formula is valid. The main theorem in [1], based on combinatorial considerations, shows how the literals are to be weighted according to a simple formula. For formulas of the above class no recursion or splitting is needed and it can easily be shown that the space complexity is reduced from 0(2^n-1) to 0(n).