No Cover Image

Journal article 1126 views

Parity Games and Propositional Proofs

Arnold Beckmann Orcid Logo, Pavel Pudlák, Neil Thapen

ACM Transactions on Computational Logic, Volume: 15, Issue: 2, Pages: 17:1 - 17:30

Swansea University Author: Arnold Beckmann Orcid Logo

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1145/2579822

Abstract

A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then...

Full description

Published in: ACM Transactions on Computational Logic
Published: 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa17523
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2014-03-25T02:30:08Z
last_indexed 2023-01-31T03:22:53Z
id cronfa17523
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2023-01-30T14:41:36.5078724</datestamp><bib-version>v2</bib-version><id>17523</id><entry>2014-03-24</entry><title>Parity Games and Propositional Proofs</title><swanseaauthors><author><sid>1439ebd690110a50a797b7ec78cca600</sid><ORCID>0000-0001-7958-5790</ORCID><firstname>Arnold</firstname><surname>Beckmann</surname><name>Arnold Beckmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2014-03-24</date><deptcode>SCS</deptcode><abstract>A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.</abstract><type>Journal Article</type><journal>ACM Transactions on Computational Logic</journal><volume>15</volume><journalNumber>2</journalNumber><paginationStart>17:1</paginationStart><paginationEnd>17:30</paginationEnd><publisher/><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>Bounded arithmetic, mean payoff games, parity games, resolution, simple stochastic sames, weak automatizability</keywords><publishedDay>30</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-04-30</publishedDate><doi>10.1145/2579822</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2023-01-30T14:41:36.5078724</lastEdited><Created>2014-03-24T08:39:00.7134692</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Arnold</firstname><surname>Beckmann</surname><orcid>0000-0001-7958-5790</orcid><order>1</order></author><author><firstname>Pavel</firstname><surname>Pudl&#xE1;k</surname><order>2</order></author><author><firstname>Neil</firstname><surname>Thapen</surname><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2023-01-30T14:41:36.5078724 v2 17523 2014-03-24 Parity Games and Propositional Proofs 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2014-03-24 SCS A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form. Journal Article ACM Transactions on Computational Logic 15 2 17:1 17:30 Bounded arithmetic, mean payoff games, parity games, resolution, simple stochastic sames, weak automatizability 30 4 2014 2014-04-30 10.1145/2579822 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2023-01-30T14:41:36.5078724 2014-03-24T08:39:00.7134692 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Arnold Beckmann 0000-0001-7958-5790 1 Pavel Pudlák 2 Neil Thapen 3
title Parity Games and Propositional Proofs
spellingShingle Parity Games and Propositional Proofs
Arnold Beckmann
title_short Parity Games and Propositional Proofs
title_full Parity Games and Propositional Proofs
title_fullStr Parity Games and Propositional Proofs
title_full_unstemmed Parity Games and Propositional Proofs
title_sort Parity Games and Propositional Proofs
author_id_str_mv 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 Arnold Beckmann
Pavel Pudlák
Neil Thapen
format Journal article
container_title ACM Transactions on Computational Logic
container_volume 15
container_issue 2
container_start_page 17:1
publishDate 2014
institution Swansea University
doi_str_mv 10.1145/2579822
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.
published_date 2014-04-30T03:20:14Z
_version_ 1763750565547868160
score 10.998116

Similar Items