| RUS ENG |
| Полная версия |
|
|
|
| ВИДЕОТЕКА |
|
Симпозиум по логике и вычислимости «Logic and Computation Day»
|
|||
|
|
|||
|
Circular proofs for provability logic D. S. Shamkanov Steklov Mathematical Institute of the Russian Academy of Sciences |
|||
|
Аннотация: We present a circular proof system for the Gödel-Löb provability logic GL. In contrast to the ordinary proofs, a circular proof can be formed from an ordinary derivation tree by identifying each open assumption with an identical interior sequent. We prove that the circular proof-system is sound and complete with respect to the standard sequent-style formulation of GL, that it is contraction-free and cut-free, and that its logical rules are invertible. As an application, we give a syntactic proof of Lyndon interpolation for GL. Язык доклада: английский |
|||