Učitavanje video playera...
00:52:24
Sebastijan Horvat: PSPACE-potpunost GL₁
Sažetak: Félix Bou i Joost J. Joosten 2011. godine dokazuju da je zatvoreni fragment logike IL (u oznaci IL_0) PSPACE-težak. U članku The closed fragment of IL is PSPACE hard pokazuju da se problem ispunjivosti za GL_1 može u polinomnom vremenu svesti na problem ispunjivosti za IL_0. Stoga ćemo se na seminaru usredotočiti na dokaz PSPACE-težine GL_1, koji se može naći u članku Vitezslava Švejdara, The Decision Problem of Provability Logic with Only One Atom. Problem ispunjivosti TQBF svest ćemo u polinomnom prostoru na problem ispunjivosti GL_1. Preciznije, za danu zatvorenu QBF-formulu A konstruirat ćemo (koristeći polinomni prostor) neku GL_1-formulu F tako da vrijedi: formula A je istinita ako i samo ako je formula F GL-ispunjiva. Kratko ćemo komentirati i dokaz PSPACE-potpunosti GL_1.
