We provide a theoretical framework that allows the direct search for natural deduction proofs in some non-classical logics, namely, intuitionistic sentential and predicate logic, but also in the modal logic S4. The framework uses so-called intercalation calculi to build up broad search spaces from which normal proofs can be extracted, if a proof exists at all. This claim is supported by completeness proofs establishing in a purely semantic way normal form theorems for the above logics. Logical restrictions on the search spaces are briefly discussed in the last section together with some heuristics for structuring a more efficient search. Our paper is a companion piece to [15], where classical logic was treated. © Springer-Ver lag Berlin Heidelberg 2005.
CITATION STYLE
Sieg, W., & Cittadini, S. (2005). Normal natural deduction proofs (in non-classical logics). Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2605 LNAI, 169–191. https://doi.org/10.1007/978-3-540-32254-2_11
Mendeley helps you to discover research relevant for your work.