Conference Paper/Proceeding/Abstract 645 views 75 downloads
A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
Lecture Notes in Computer Science, Volume: 11425, Pages: 470 - 487
Swansea University Author:
Cécilia Pradic
-
PDF | Version of Record
© The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License
Download (1.41MB)
DOI (Published version): 10.1007/978-3-030-17127-8_27
Abstract
We devise a variant of Dialectica interpretation of intuitionistic linear logic for Open image in new window, a linear logic-based version MSO over infinite words. Open image in new window was known to be correct and complete w.r.t. Church’s synthesis, thanks to an automata-based realizability model...
Published in: | Lecture Notes in Computer Science |
---|---|
ISSN: | 0302-9743 1611-3349 |
Published: |
Cham
Springer International Publishing
2019
|
Online Access: |
Check full text
|
URI: | https://cronfa.swan.ac.uk/Record/cronfa58114 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Abstract: |
We devise a variant of Dialectica interpretation of intuitionistic linear logic for Open image in new window, a linear logic-based version MSO over infinite words. Open image in new window was known to be correct and complete w.r.t. Church’s synthesis, thanks to an automata-based realizability model. Invoking Büchi-Landweber Theorem and building on a complete axiomatization of MSO on infinite words, our interpretation provides us with a syntactic approach, without any further construction of automata on infinite words. Via Dialectica, as linear negation directly corresponds to switching players in games, we furthermore obtain a complete logic: either a closed formula or its linear negation is provable. This completely axiomatizes the theory of the realizability model of Open image in new window. Besides, this shows that in principle, one can solve Church’s synthesis for a given ∀∃ -formula by only looking for proofs of either that formula or its linear negation. |
---|---|
College: |
Faculty of Science and Engineering |
Start Page: |
470 |
End Page: |
487 |