Elements of finite model theory

Více o knize

Finite model theory, rooted in mathematical logic and computer science, explores applications in database theory, computational complexity, and formal languages, with recent connections to formal methods, verification, and artificial intelligence. Its origins trace back to Trakhtenbrot's 1950 result, which established that validity over finite models is not recursively enumerable, highlighting a failure of completeness. This proof technique, which encodes Turing machine computations as finite structures, was later employed by Fagin to demonstrate the equivalence between the class NP and existential second-order logic, offering a machine-independent view of a key complexity class. In 1982, Immerman and Vardi expanded this field by showing that a fixed point extension of first-order logic captures the complexity class PTIME, leading to logical characterizations of other significant complexity classes, a pursuit known as descriptive complexity. Additionally, finite model theory has influenced the evolution of relational databases; by the late 1970s, the relational model emerged as the dominant framework, with basic query languages primarily based on first-order predicate calculus or its minor extensions.