Number of the records: 1
Parity games and propositional proofs
- 1.
SYSNO ASEP 0422131 Document Type C - Proceedings Paper (int. conf.) R&D Document Type Conference Paper Title Parity games and propositional proofs Author(s) Beckmann, A. (GB)
Pudlák, Pavel (MU-W) RID, SAI
Thapen, Neil (MU-W) RID, SAISource Title Mathematical Foundations of Computer Science 2013. - Berlin : Springer, 2013 / Chatterjee K. ; Sgall J. - ISBN 978-3-642-40312-5 Pages s. 111-122 Number of pages 12 s. Publication form Print - P Action International Symposium on Mathematical Foundations of Computer Science 2013 /38./ Event date 26.08.2013-30.08.2013 VEvent location Klosterneuburg Country AT - Austria Event type WRD Language eng - English Country DE - Germany Keywords resolution proof systems ; parity games ; game equivalent to resolution Subject RIV BA - General Mathematics R&D Projects IAA100190902 GA AV ČR - Academy of Sciences of the Czech Republic (AV ČR) Institutional support MU-W - RVO:67985840 UT WOS 000342994500012 EID SCOPUS 84885230768 DOI 10.1007/978-3-642-40313-2_12 Annotation 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 also define a 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. Workplace Mathematical Institute Contact Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Year of Publishing 2014
Number of the records: 1