Connection tableau calculi with disjunctive contraints (TU München) (Q2726292)

One of the main difficulties in automated theorem proving is that, to find a proof, we need to search over a very large search space. One of the possible ways to speed up this search is to try to make all intermediate results as general as possible. Specifically, in the process of theorem proving, we generate several auxiliary formulas (``subgoals'') and try to prove them one by one until we finally prove the original statement. Often, several of these formulas have a similar structure, so, we can describe a general formula that includes the desired ones as special cases. If we can prove this general formula instead of proving all its necessary particular cases one by one, we will save time and still get all the particular cases proven. This idea is used in automated theorem proving and it is indeed helpful. However, sometimes, a ``natural'' generalization is so general that it cannot be derived from the axioms; in this case, in the existing theorem provers, we go back to proving the original auxiliary formulas one by one. NEWLINENEWLINENEWLINEIt has been noticed that in many such situations, the general formula is ``almost'' deducible from the axioms, in the sense that we can deduce this general formula under certain constraints. A toy example: if we want to prove two formulas \(p(a,b)\) and \(p(a,c)\), then a natural generalization that covers both formulas is \(p(a,x)\) with a variable \(x\). If this general formula is false in some cases (and thus cannot be proven in all its generality), we may try to prove it under some constraint that includes both original formulas: e.g., under the constraint \((x=b)\vee (x=c)\). This idea has been known for some time, but it has never been successfully implemented in automatic deduction; the problem is that the relevant constraints are often disjunctions, and no efficient way of proving formulas under disjunctive constraints was previously known. The author has developed an efficient technique of proving formulas under disjunctive constraints, and has effectively applied this techniques to drastically speed up theorem proving algorithms.