Algorithmic Model Theory
Introduction: Model Theory and Computation
Algorithmic model theory uses tools from mathematical logic to answer modeltheoretic questions that arise from algorithmic issues in discrete mathematical structures and in the modelling of data, information and computation.
As a branch of mathematical logic, model theory is generally concerned with the study of
 definability and the expressive power of logical formalisms for the specification of structural properties;
 analysis and classification of the models of given logical specifications.
Immediate algorithmic themes in this context are, for instance,
 decidability and complexity of the logical theories of given structures
(a classical issue relevant for model checking and verification methodologies);  connections between the logical and algorithmic complexities of given structural properties.
Modeltheoretic questions, which arise from the modelling of computations, specific models of computation or structural representations of data, include
 definability issues over special classes of structures;
 delineation of specialised formalisms designed to capture relevant properties at low levels of complexity;
 delineation of classes of structures with good modeltheoretic properties that are rich enough for the modelling of relevant phenomena.
All these issues typically display a sharp tradeoff between tractability and richness/expressiveness (of structures/logics).
Methodological Issues: Model Theory and Modelling
It is important to note that the basic logical notions of
 logical equivalence (of two specifications),
 satisfiability (of a specification),
 validity (of a deduction)
crucially depend on the underlying class of admissible structures.
Finite model theory, for instance, differs from classical model theory in admitting just finite structures; this restriction is essential for many applications, where infinite instances do not correspond to intended models and hence need to be excluded from all considerations for which the distinction matters. If, for instance, all counterexamples to the equivalence between two specifications or database queries are infinite, then they need to be recognised as equivalent in a setting in which only finite models occur.
Apart from the class of all finite structures, there are many other specific classes of structures that similarly deserve attention – either because they form natural levels with respect to our methods and tools, or because they arise as classes of intended models in some specific context. Similarly, the class of relevant properties may have to be restricted to capture the essence of some modelling scenario: aspects of the structural models that do not correspond to intended aspects of the underlying phenomenon must not make a difference. This imposes specific constraints on the level of granularity at which structural properties are discerned, which in modeltheoretic terms typically correspond to preservation properties.
In view of the tradeoff mentioned above, the real challenge, besides the technical analysis of interesting scenarios, may often consist in striking a balance between
 the richness of the class of admissible structures
 the expressiveness of the logical formalism or the constraints on structural properties under consideration,
taking into account fundamental limitations (like undecidability or lower bounds on complexities) and primarily technical limitations in terms of the available methods.
Research Questions and Projects
