Focusing and polarization: a journey from proof search to term representation
- 講者吳睿軒 先生 (法國巴黎綜合理工學院)
邀請人：陳亮廷 - 時間2024-11-05 (Tue.) 10:30 ~ 11:30
- 地點資訊所新館101演講廳
摘要
In this talk, I will discuss the concepts of focusing and polarization in structural proof theory. Focusing was first introduced by Jean-Marc Andreoli as a technique to improve proof search in linear logic by distinguishing between invertible and non-invertible inference rules in the sequent calculus. This distinction leads naturally to the notion of polarity in linear logic: a connective is classified as negative if its right-introduction rule is invertible, and positive if it is non-invertible.
While polarities of connectives are well-defined in linear logic, they are ambiguous in intuitionistic and classical logics. In these settings, an arbitrary polarity can be assigned to each connective and even atomic formula when one wants to express focusing in these settings. Though these assignments do not affect the provability of a given formula, they can have a significant impact on the form of resulting proofs. By annotating proofs with terms, this feature allows us to explore different styles of term representation.
This talk aims to provide a high-level overview of existing work related to these two notions, from their impact on proof search to their role in studying term representation.
While polarities of connectives are well-defined in linear logic, they are ambiguous in intuitionistic and classical logics. In these settings, an arbitrary polarity can be assigned to each connective and even atomic formula when one wants to express focusing in these settings. Though these assignments do not affect the provability of a given formula, they can have a significant impact on the form of resulting proofs. By annotating proofs with terms, this feature allows us to explore different styles of term representation.
This talk aims to provide a high-level overview of existing work related to these two notions, from their impact on proof search to their role in studying term representation.