Overview   AProS   L & P   Proof Lab   Tutor   Truth Lab   Participants

automated proof search

IntroductionProof Display

Introduction

AProS uses the intercalation method to search for normal natural deduction proofs in classical sentential and predicate logic; the method has been adapted to search also in intuitionistic and minimal logic. Extensions to elementary parts of set theory and formalized metamathematics have been developed. Currently, these extensions are being refined further. Gentzen's natural deduction calculi are logical tools that capture directly, how humans reason through a proof. They allow reasoning with assumptions and introduction as well as elimination rules for the logical connectives. The intercalation method exploits systematically the underlying idea that elimination rules allow the decomposition of complex formulas and that introduction rules permit building up complex ones.

The most distinctive feature of the search procedure implemented in AProS is that the proof construction can be separated strategically into three distinct modules: extraction or goal-directed forward use of elimination rules, inversion or backward use of introduction rules, and finally the use of indirect argumentation.

The pleasure of seeing AProS at work can be experienced through connecting to the Proof Display.