No Cover Image

Conference Paper/Proceeding/Abstract 555 views 71 downloads

A Dialectica-Like Interpretation of a Linear MSO on Infinite Words

Cécilia Pradic Orcid Logo, Colin Riba

Lecture Notes in Computer Science, Volume: 11425, Pages: 470 - 487

Swansea University Author: Cécilia Pradic Orcid Logo

  • 58114.pdf

    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)

Check full text

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...

Full description

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

Similar Items