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)

Full work available at URL https://doi.org/10.1007/BFB0038694

Mathematics Subject Classification ID

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

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

(12)

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

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)