Intercalation calculi for classical logic

Abstract: "Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use I describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? This informal question motivated the formulation of intercalation calculi. Ic- calculi are the technical underpinnings for (1) and (2), and the paper focuses on their detailed presentation and meta-mathematical investigation -- in the case of classical predicate logic."