# 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.