[logic-ml] Talk by Adam Prenosil (13 Oct 11:00-)

[Tetsuya Sato]

京都大学数理解析研究所の佐藤です。

10月13日11:00から、チェコ科学アカデミーのAdam Prenosil氏に
以下の講演をしていただくことになりましたので、
ご連絡いたします。どうぞお気軽にお越しください。

==========
Time:	11:00-12:00, 13 Oct, 2016
Place:	Rm 478, Research Building 2, Main Campus, Kyoto University
	京都大学 本部構内 総合研究2号館 4階478号室
	http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)
	http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)

Speaker: Adam Prenosil (Czech Academy of Sciences)

Title:	Classical proof theory, non-classically

Abstract:
We present an approach to cut elimination in classical logic
which appeals to elimination rules.rather than to induction
on cut rank and which works equally well for proofs from a
non-empty set of sequential premises. As an illustration of
the benefits of accepting elimination rules as an integral
part of the sequent calculus for classical logic, we use the
calculus with elimination rules to provide a particularly
simple syntactic proof of a recent non-classical refinement
of Craig's interpolation theorem due to Milne. This
approach, while non-standard, is in fact natural when we
view classical logic as part of the family of super-Belnap
logics, that is, extensions of the four-valued Belnap-Dunn
logic. We shall therefore start by introducing this family
proof-theoretically as the logics which retain the
structural and logical rules of classical logic, but relax
Identity and Cut (as opposed to substructural logics, which
retain Identity and Cut but relax the structural rules of
classical logic).