Focusing and polarization in linear, intuitionistic, and classical logics

DOI10.1016/j.tcs.2009.07.041zbMath1187.68528MaRDI QIDQ1035706

Chuck Liang, Dale A. Miller

Publication date: 4 November 2009

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.07.041

zbMATH Keywords

sequent calculus; intuitionistic logic; classical logic; focused proof system

Mathematics Subject Classification ID

Uses Software

• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Polarized and focalized linear and classical proofs
• Linear logic
• Forum: A multiple-conclusion specification logic
• On the unity of logic
• A logical characterization of forward and backward chaining in the inverse method
• Logic programming in a fragment of intuitionistic linear logic
• On structuring proof search for first order linear logic
• Uniform proofs as a foundation for logic programming
• The duality of computation
• Jumbo λ-Calculus
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Focusing and Polarization in Intuitionistic Logic
• Incorporating Tables into Proofs
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• Contraction-free sequent calculi for intuitionistic logic
• A new deconstructive logic: linear logic
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Logical Approaches to Computational Barriers