A Calculus Supporting Structured Proofs.
Bernd Ingo Dahn, Andreas M. Wolf · 1994
: Proofs in standard logical calculi have a simple structure (mostly a sequence, tree or set of related formulas). Therefore, formal proofs are hard to understand or to present in an intelligible way. The Block Calculus for first order logic introduced in this paper is a variant of natural deduction that has highly structured proofs. These proofs can be presented in many ways by hiding blocks of subproofs. Moreover it can be easily extended by other calculi. We characterize the semantics of incomplete proof structures in the Block Calculus and prove it's soundness and completeness. Contents 1. Introduction 1 2. Some Definitions 3 3. Rules 5 4. Examples 7 5. Completeness and Soundness 10 6. Conclusion 14 1. Introduction Verified proofs have to be written in a formalized logical calculus. This is tedious for a human user. For complex proof tasks automated theorem provers can be used perform a part of this work. However, proofs generated by these automated deductive systems are often ha...