FC: A finite-model theory of concatenation

Sam Thompson ( King's College London )

The theory of concatenation is a first-order logic over the free monoid (Σ*,·). While this logic is highly expressive, it is also very expensive, with satisfiability being undecidable. Furthermore, there is no meaningful distinction between satisfiability and model checking.

FC is a logic that merges the theory of concatenation with finite-model theory by restricting the universe to factors of an input word. This results in an expressive logic over words with many desirable properties of more classical forms of FO over finite structures. For example, model checking is not only decidable but becomes tractable by bounding "the usual" parameters (such as width). FC is strongly coupled with information extraction (querying text documents), and thus can be viewed as a logic for querying unstructured textual data. More generally, FC can be used as a logical framework to obtain algorithms for various string-related problems, like pattern matching with variables.