KE+: Beyond Refutation
Guido Governatori · 1995
The system KE +, a tableau-like proof system based on D’Agostino-Mondadori KE [DM94], is presented in this paper. This system avoids some of the drawbacks of other proof methods. In fact it is completly analytical, it is able to detect whether a formula is either a tautology or a contradiction or only a satisfiable one; in the course of a proof it can detect whether a subformula is a tautology and it uses this fact in the proof of the main formula. In what follows we shall use the Smullyan uniform notation [Smu68]; if X is a signed formula, X C denotes the conjugate of X. The method KE + follows consists in verifying whether the truth of the conjugate of an immediate subformula of a β formula implies the truth of the other immediate subformula; if it is implied then we have enough information to affirm that the whole formula is provable. This result is obtained through the fact that in a given branch, the branch beginning with the conjugate, a formula which leads to the branch closure does not exist (i.e. there are not two formulas T A, F A) but this is done by proving that the conjugate of the formula occurs in the branch, i.e. we have to see that in a branch a signed formula appears twice, and that the two occurrences are derived from appropriate formulas. KE and KE + share the same inference rules and differ only with respect to the proof procedure they use. The main feature of KE is that it is a method which uses elimination rules and an analytic form of cut (P B). Its rules are stated as follows: