Invited Talks
Title: A proof theory for model checking: an overview
Dale Miller (LIX, École Polytechnique, France)
Abstract:
While model checking has often been considered as a practical alternative to building formal proofs, we argue here that linear logic (actually MALL) extended with first-order term structures and with least and greatest fixed points provides an appealing foundation for model checking. Since the emphasis of model checking is on establishing the truth of a property in a model, we rely on the proof theoretic notion of additive inference rules, since it provides a natural way to allow provability to directly describe truth values. Unfortunately, using these rules alone potentially requires inference rules to have infinite sets of premises. We allow multiplicative rules but restrict their use to be limited to the construction of additive synthetic inference rules: such synthetic rules are derived from the proof theoretic notions of polarization and focused proof systems. This framework provides natural proof theoretic treatments of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.
This work is joint with Quentin Heath.
New Directions Talk
Title: On Gödel's Second Incompleteness Theorem for Arithmetic without Contraction
Daniyar Shamkanov (National Research University, Russia)
Abstract:
Exploring bounds of Godel's second incompleteness theorem leads to relaxing various assumptions involved in its proof. The standard proof of Godel's theorem applies the contraction rule. Moreover, one can find examples of modal systems enjoying Lob's derivability conditions without the contraction rule that invalidate Godel's argument. In this talk, we consider a system of arithmetic based on contraction-free logic and show that Godel's theorem is valid in this case.