A logic program for transforming sequent proofs to natural deduction proofs

DOI10.1007/BFB0038694zbMATH Open1502.68063MaRDI QIDQ5053007FDOQ5053007

Authors: Amy P. Felty 

Publication date: 26 November 2022

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

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

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)

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
• Title not available (Why is that?)
• Presentation of proofs in modal natural deduction
• Interpolation theorems for intuitionistic predicate logic
• Title not available (Why is that?)
• Title not available (Why is that?)

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)