Logic and Games on Automatic Structures Playing with Quantifiers and Decompositions

The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it is false. This correspondence has been known for a very long time and has inspired numerous research directions. In this book, the author...

Full description

Bibliographic Details
Main Author: Kaiser, Lukasz
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2011, 2011
Edition:1st ed. 2011
Series:Lecture Notes in Artificial Intelligence
Subjects:
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
LEADER 03449nmm a2200349 u 4500
001 EB000387435
003 EBX01000000000000000240487
005 00000000000000.0
007 cr|||||||||||||||||||||
008 130626 ||| eng
020 |a 9783642228070 
100 1 |a Kaiser, Lukasz 
245 0 0 |a Logic and Games on Automatic Structures  |h Elektronische Ressource  |b Playing with Quantifiers and Decompositions  |c by Lukasz Kaiser 
250 |a 1st ed. 2011 
260 |a Berlin, Heidelberg  |b Springer Berlin Heidelberg  |c 2011, 2011 
300 |a XII, 118 p  |b online resource 
505 0 |a 1 Logics, Structures and Presentations -- 2 Game Quantifiers on Automatic Presentations -- 3 Games for Model Checking on Automatic Structures -- 4 Memory Structures for Infinitary Games -- 5 Counting Quantifiers on Automatic Structures -- 6 Cardinality Quantifiers in MSO on Linear Orders -- 7 Cardinality Quantifiers in MSO on Trees -- 8 Outlook 
653 |a Computer science—Mathematics 
653 |a Symbolic and Algebraic Manipulation 
653 |a Mathematical logic 
653 |a Artificial Intelligence 
653 |a Formal Languages and Automata Theory 
653 |a Machine theory 
653 |a Artificial intelligence 
653 |a Mathematical Logic and Foundations 
041 0 7 |a eng  |2 ISO 639-2 
989 |b Springer  |a Springer eBooks 2005- 
490 0 |a Lecture Notes in Artificial Intelligence 
028 5 0 |a 10.1007/978-3-642-22807-0 
856 4 0 |u https://doi.org/10.1007/978-3-642-22807-0?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 006.3 
520 |a The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it is false. This correspondence has been known for a very long time and has inspired numerous research directions. In this book, the author extends this connection between logic and games to the class of automatic structures, where relations are recognized by synchronous finite automata. In model-checking games for automatic structures, two coalitions play against each other with a particular kind of hierarchical imperfect information. The investigation of such games leads to the introduction of a game quantifier on automatic structures, which connects alternating automata with the classical model-theoretic notion of a game quantifier. This study is then extended, determining the memory needed for strategies in infinitary games on the one hand, and characterizing regularity-preserving Lindström quantifiers on the other. Counting quantifiers are investigated in depth: it is shown that all countable omega-automatic structures are in fact finite-word automatic and that the infinity and uncountability set quantifiers are definable in MSO over countable linear orders and over labeled binary trees. This book is based on the PhD thesis of Lukasz Kaiser, which was awarded with the E.W. Beth award for outstanding dissertations in the fields of logic, language, and information in 2009. The work constitutes an innovative study in the area of algorithmic model theory, demonstrating the deep interplay between logic and computability in automatic structures. It displays very high technical and presentational quality and originality, advances significantly the field of algorithmic model theory and raises interesting new questions, thus emerging as a fruitful and inspiring source for future research