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, in elementary parts of set theory and in formalized metamathematics.
Gentzen proposed natural deduction calculi as logical tools that capture quite directly how humans reason through a proof. They allow, most distinctively, 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.