Automatic Structures

点击翻译按钮获取中文摘要

This project adresses questions from the field of algorithmic model theory. The overall goals include a better understanding of the model-theoretic and algorithmic properties of finitely presentable infinite structures, the development of new methods for the algorithmic treatment of infinite structures, towards applications in several areas of computer science, and the solution of some fundamental theoretic problems in this area.More specifically, this project is concerned with automatic structures. A structure is automatic if its elements can be represented by words of a regular language in such a way that all relations and functions of the structure can be recognized by synchronous finite automata. Since automatic structures admit the effective (in fact even automatic) evaluation of arbitrary first-order formulae, and certain stronger formalisms, and since theyare closed under many fundamental operations, they provide a natural and relevant framework for the research programme of algorithmic model theory.In particular we will address the current challenge to advance, beyond the relatively well-understood case of word-automatic structures, the theory and algorithmic methods for omega-automatic and omega-tree-automatic structures. In addition we aim at a general and comprehensive framework for automatic structures that should permit to solve certain fundamental questions independent of a specific variant of automatic presentations. Although relevant achievements have recently been obtained on omega-automatic structures and on injective versus non-injective presentations, the current methodology needs to be enriched and refined for making significant progress for omega-tree-automatic structures.Beyond the study of the established classes of automatic presentations we aim at a systematic generalization of the approach to handle infinite structures algorithmically on the basis of such finite presentations.A further motivation for this approach comes from the, at present still informal, question of whether every (natural) structure with a decidable theory can be decided by means of a finite (or even in some sense automatic) presentation. In a differern form this question has already been raised in Rabin's classical paper from 1969 on the monadic theory of the infinite binary tree. In this way, we also hope to provide a better understanding of the algorithmic complexity of decidable theories.