| RUS ENG |
| Full version |
|
|
|
| VIDEO LIBRARY |
|
Symposium on logic and computability "Logic and Computation Day"
|
|||
|
|
|||
|
Circular proofs for provability logic D. S. Shamkanov Steklov Mathematical Institute of the Russian Academy of Sciences |
|||
|
Abstract: 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. Language: English |
|||