Editing Model checking (section)

== First-order logic ==
Model checking is also studied in the field of [[computational complexity theory]]. Specifically, a [[First-order logic|first-order logical]] formula is fixed without [[free variable]]s and the following [[decision problem]] is considered: 

''Given a finite [[interpretation (logic)|interpretation]], for instance, one described as a [[relational database]], decide whether the interpretation is a model of the formula.''

This problem is in the [[circuit class]] '''[[AC0 (complexity)|AC<sup>0</sup>]]'''. It is [[Computational_complexity_theory#tractable_problem|tractable]] when imposing some restrictions on the input structure: for instance, requiring that it has [[treewidth]] bounded by a constant (which more generally implies the tractability of model checking for [[monadic second-order logic]]), bounding the [[degree (graph theory)|degree]] of every domain element, and more general conditions such as [[bounded expansion]], locally bounded expansion, and nowhere-dense structures.<ref>{{Cite journal|last1=Dawar|first1=A|last2=Kreutzer|first2=S|date=2009|title=Parameterized complexity of first-order logic|url=http://pdfs.semanticscholar.org/ac54/505a6c9b843259727dba98fad1a02af2a567.pdf|archive-url=https://web.archive.org/web/20190303105602/http://pdfs.semanticscholar.org/ac54/505a6c9b843259727dba98fad1a02af2a567.pdf|url-status=dead|archive-date=2019-03-03|journal=ECCC|s2cid=5856640}}</ref> These results have been extended to the task of [[enumeration algorithm|enumerating]] all solutions to a first-order formula with free variables.{{cn|date=May 2019}}