Previous: TR 92-15 Next: TR 92-18

Intellektik: Technical report 92-17

Induktion in der Konnektionsmethode

Stefan Brüning

We present an approach to integrate induction into calculi based on Bibel's connection method by introducing several new inference steps. As a result, we obtain a homogeneous proof procedure that combines the advantages of the connection calculi and the possibility of finding proofs by induction. This work generalizes previous techniques \cite{breu} which are restricted to the case of inductive sentences consisting of a single literal. Namely, in order to handle arbitrary inductive sentences we introduce a way to split the proof of a formula into several subproofs which include inductive proofs with inductive sentences consisting of one literal only. On the one hand, this avoids the need of a general proof procedure for formulas in non-normal form as required for an obvious alternative approach. On the other hand, for performing a proof by induction we do not need to know the inductive sentence as a whole.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry