A logic program for transforming sequent proofs to natural deduction proofs. (English) Zbl 1502.68063
Schroeder-Heister, Peter (ed.), Extensions of logic programming. International workshop, Tübingen, FRG, 8–10 December 1989. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 475, 157-178 (1991).
The paper presents a specification of sequent calculi and natural deduction proofs and a description of the transformation between them. The language expressing the above is a subset of higher-order hereditary Harrop formulas which correspond to \(\lambda\)Prolog. The specification itself presents both a declarative and an operational description of the correspondence between the sequent calculus and natural deduction for intuitionistic logic, which can actually be run as a program in \(\lambda\)Prolog.
For the entire collection see [Zbl 0770.68025].
For the entire collection see [Zbl 0770.68025].
Reviewer: Jiří Zlatuška (Brno)
MSC:
68N17 | Logic programming |
03B20 | Subsystems of classical logic (including intuitionistic logic) |
03B35 | Mechanization of proofs and logical operations |
03F07 | Structure of proofs |