Backward reasoning in systems with cut
In backward reasoning, a proof of a theorem is constructed by trying to obtain a set of axioms from the theorem by backward application of inference rules. Backward reasoning can be automatized if, for each instance of a rule, the premises are uniquely determined by the conclusion. The cut rule does not have this property. On the contrary, for every formula which is the conclusion of an instance of the cut rule, there are infinitely many pairs of premises. Hence, the known efficient techniques of automated backward reasoning cannot be used in systems with cut.
In this paper, an approach to the problem is presented using formula schemes rather than formulas. A formula scheme is like a formula except it can contain metavariables instead of some subformulas or subterms. For example, backward application of modus ponens to a formula F yields the two formula schemes Φ and Φ → F where Φ is a metavariable for a formula. Rules just consist of a number of formula schemes (premises and conclusion) and of a number of conditions under which the rule is applicable. Two or more rules can be composed into a new rule. This allows an arbitrary mixture of forward and backward reasoning. The composite rule is computed by a sort of unification on the set of formulas. Since a unifiable pair of formulas in general does not have a single most general unifier, unification is only done partially (pseudounification) leaving an equation between formulas as a new condition of the resulting rule. Since these equations are always solvable, it is guaranteed that an inference step on the level of formula schemes fails whenever there is no corresponding inference on the level of formulas. So, considering formula schemes rather than formulas really reduces the search tree.
KeywordsSearch Tree Term Variable Constant Variable Formula Variable Variable Variable
Unable to display preview. Download preview PDF.
- W. Bibel, M. Davis, E. Eder, N. Eisinger, M. Fitting, W. Hodges, D. J. Israel, H.J. Ohlbach, and D.A. Plaisted. Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1. Clarendon Press, Oxford, 1993. (Dov M. Gabbay, C.J. Hogger, and J.A. Robinson, editors).Google Scholar
- Wolfgang Bibel. Automated Theorem Proving. Artificial Intelligence. Vieweg, Braunschweig/Wiesbaden, second edition, 1987.Google Scholar
- Elmar Eder. An implementation of a theorem prover based on the connection method. In W. Bibel and B. Petkoff, editors, Artificial Intelligence, Methodology, Systems, Applications (AIMSA '84), Varna, Bulgaria (Sept. 1984), pages 121–128, Amsterdam, New York, Oxford, 1985. European Coordinating Committee for Artificial Intelligence, North-Holland.Google Scholar
- Elmar Eder. Relative Complexities of First Order Calculi. Artificial Intelligence. Vieweg, Wiesbaden, 1992. (Wolfgang Bibel and Walther von Hahn, editors).Google Scholar
- R. Statman. Lower bounds on herbrand's theorem. Proc. AMS, 75, 1979.Google Scholar
- M. E. Szabo. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1969.Google Scholar