Logic and Games on Automatic Structures: Playing with Quantifiers and Decompositions

ارزیابی یک فرمول منطقی را می‌توان به‌عنوان بازی دو حریف در نظر گرفت، یکی در تلاش برای نشان دادن درستی فرمول و دیگری برای اثبات نادرست بودن آن. این مکاتبات برای مدت بسیار طولانی شناخته شده است و الهام بخش جهت های تحقیقاتی متعددی بوده است. در این کتاب، نویسنده این ارتباط بین منطق و بازی‌ها را به کلاس ساختارهای خودکار تعمیم می‌دهد، جایی که روابط توسط خودکارهای متناهی سنکرون شناسایی می‌شوند.

در بازی‌های بررسی مدل برای ساختارهای خودکار، دو ائتلاف در برابر هر کدام بازی می‌کنند. دیگر با نوع خاصی از اطلاعات ناقص سلسله مراتبی. بررسی چنین بازی‌هایی منجر به معرفی یک کمیت بازی بر روی ساختارهای خودکار می‌شود که اتوماتای ​​متناوب را با مفهوم کلاسیک مدل-نظری یک کمی‌تفایر بازی مرتبط می‌کند. این مطالعه سپس گسترش می‌یابد و از یک سو حافظه مورد نیاز برای استراتژی‌ها در بازی‌های بی‌نهایت را تعیین می‌کند و از سوی دیگر کمیت‌کننده‌های لیندستروم حفظ نظم را مشخص می‌کند. کمی‌سازهای شمارش عمیقاً بررسی می‌شوند: نشان داده شده است که تمام ساختارهای امگا-اتوماتیک قابل شمارش در واقع خودکار کلمات محدود هستند و کمیت‌کننده‌های مجموعه بی‌نهایت و غیرقابل شمارش در MSO بر روی نظم‌های خطی قابل شمارش و روی درخت‌های باینری برچسب‌گذاری‌شده قابل تعریف هستند.

این کتاب بر اساس پایان نامه دکترای لوکاس قیصر است که جایزه E.W. Beth را برای پایان نامه های برجسته در زمینه های منطق، زبان و اطلاعات در سال 2009 دریافت کرد. این کار یک مطالعه نوآورانه در زمینه الگوریتمی است. نظریه مدل، نشان دهنده تعامل عمیق بین منطق و محاسبات در ساختارهای خودکار است. کیفیت و اصالت فنی و ارائه بسیار بالایی را نشان می دهد، زمینه تئوری مدل الگوریتمی را به طور قابل توجهی پیشرفت می دهد و سؤالات جدید جالبی را مطرح می کند، بنابراین به عنوان منبعی پربار و الهام بخش برای تحقیقات آینده ظهور می کند.

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.