Formelspel

Ett formelspel är ett konstgjort spel som representeras av en helt kvantifierad boolesk formel . Spelarnas turer växlar och utrymmet för möjliga drag betecknas med bundna variabler . Om en variabel är universellt kvantifierad , har formeln som följer den samma sanningsvärde som formeln som börjar med den universella kvantifieraren oavsett draget. Om en variabel är existentiellt kvantifierad har formeln som följer den samma sanningsvärde som formeln som börjar med den existentiella kvantifieraren för minst ett drag som är tillgängligt vid tur. Omgångarna växlar, och en spelare förlorar om han inte kan röra sig vid sin tur. I beräkningskomplexitetsteori definieras språket FORMULA-SPEL som alla formler $\Phi$ så att spelare 1 har en vinnande strategi i spelet representerad av $\Phi$ . FORMULA-SPEL är PSPACE-komplett .

• Sipser, Michael. (2006). Introduktion till teorin om beräkning . Boston: Thomson Course Technology.