No Cover Image

Conference Paper/Proceeding/Abstract 27 views 6 downloads

A Dialectica-Like Interpretation of a Linear MSO on Infinite Words / Pierre Pradic, Colin Riba

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

Swansea University Author: Pierre Pradic

  • 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)

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!
first_indexed 2021-10-15T15:59:26Z
last_indexed 2021-10-19T03:23:09Z
id cronfa58114
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2021-10-18T13:22:01.0514049</datestamp><bib-version>v2</bib-version><id>58114</id><entry>2021-09-27</entry><title>A Dialectica-Like Interpretation of a Linear MSO on Infinite Words</title><swanseaauthors><author><sid>3b6e9ebd791c875dac266b3b0b358a58</sid><firstname>Pierre</firstname><surname>Pradic</surname><name>Pierre Pradic</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-27</date><deptcode>SCS</deptcode><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&#x2019;s synthesis, thanks to an automata-based realizability model. Invoking B&#xFC;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&#x2019;s synthesis for a given &#x2200;&#x2203; -formula by only looking for proofs of either that formula or its linear negation.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Lecture Notes in Computer Science</journal><volume>11425</volume><journalNumber/><paginationStart>470</paginationStart><paginationEnd>487</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>5</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2019</publishedYear><publishedDate>2019-04-05</publishedDate><doi>10.1007/978-3-030-17127-8_27</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2021-10-18T13:22:01.0514049</lastEdited><Created>2021-09-27T22:57:32.3261199</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Pierre</firstname><surname>Pradic</surname><order>1</order></author><author><firstname>Colin</firstname><surname>Riba</surname><order>2</order></author></authors><documents><document><filename>58114__21180__8f39ac667924487791b3552601ba7708.pdf</filename><originalFilename>58114.pdf</originalFilename><uploaded>2021-10-15T17:02:45.4826327</uploaded><type>Output</type><contentLength>1478625</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2021-10-18T13:22:01.0514049 v2 58114 2021-09-27 A Dialectica-Like Interpretation of a Linear MSO on Infinite Words 3b6e9ebd791c875dac266b3b0b358a58 Pierre Pradic Pierre Pradic true false 2021-09-27 SCS 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. Conference Paper/Proceeding/Abstract Lecture Notes in Computer Science 11425 470 487 Springer International Publishing Cham 0302-9743 1611-3349 5 4 2019 2019-04-05 10.1007/978-3-030-17127-8_27 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2021-10-18T13:22:01.0514049 2021-09-27T22:57:32.3261199 College of Science Computer Science Pierre Pradic 1 Colin Riba 2 58114__21180__8f39ac667924487791b3552601ba7708.pdf 58114.pdf 2021-10-15T17:02:45.4826327 Output 1478625 application/pdf Version of Record true © The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License true eng http://creativecommons.org/licenses/by/4.0/
title A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
spellingShingle A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
Pierre, Pradic
title_short A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
title_full A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
title_fullStr A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
title_full_unstemmed A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
title_sort A Dialectica-Like Interpretation of a Linear MSO on Infinite Words
author_id_str_mv 3b6e9ebd791c875dac266b3b0b358a58
author_id_fullname_str_mv 3b6e9ebd791c875dac266b3b0b358a58_***_Pierre, Pradic
author Pierre, Pradic
author2 Pierre Pradic
Colin Riba
format Conference Paper/Proceeding/Abstract
container_title Lecture Notes in Computer Science
container_volume 11425
container_start_page 470
publishDate 2019
institution Swansea University
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-030-17127-8_27
publisher Springer International Publishing
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2019-04-05T04:26:53Z
_version_ 1722265122795159552
score 10.851694