A logic program for transforming sequent proofs to natural deduction proofs

DOI10.1007/BFB0038694MaRDI QIDQ5053007zbMATH OpenFDO

Authors Amy P. Felty

Publication date 26 November 2022

Published in Extensions of Logic Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Recommendations

• Proofs, upside down. A functional correspondence between natural deduction and the sequent calculus
• scientific article; zbMATH DE number 785043
• scientific article; zbMATH DE number 1555192
• scientific article; zbMATH DE number 1390270
• A proof procedure for the logic of hereditary Harrop formulas

Cited in

(11)

• Proofs, upside down. A functional correspondence between natural deduction and the sequent calculus
• Representing scope in intuitionistic deductions
• A Compressing Translation from Propositional Resolution to Natural Deduction
• Extended Natural Deduction Images of Conversions from the System of Sequents
• From input/output logics to conditional logics via sequents -- with provers
• A negationless interpretation of intuitionistic theories. I
• scientific article; zbMATH DE number 1543302 (Why is no real title available?)
• Presentation of proofs in modal natural deduction
• Interpolation theorems for intuitionistic predicate logic
• scientific article; zbMATH DE number 1555192 (Why is no real title available?)
• scientific article; zbMATH DE number 1389648 (Why is no real title available?)

This page was built for publication: A logic program for transforming sequent proofs to natural deduction proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5053007)