Content deleted Content added
more specific about treewidth |
structuring, add more about computational complexity of evaluation, enumeration, and counting |
||
Line 2:
Second-order logic allows quantification over [[Predicate (mathematical logic)|predicates]]. However, MSO is the [[Fragment (logic)|fragment]] in which second-order quantification is limited to monadic predicates (predicates having a single argument). This is often described as quantification over "sets" because monadic predicates are equivalent in expressive power to sets (the set of elements for which the predicate is true).
== Computational complexity of evaluation ==
Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must be [[existential quantifier]]s, outside of any other part of the formula. The first-order quantifiers are not restricted. By analogy to [[Fagin's theorem]], according to which existential (non-monadic) second-order logic captures precisely the [[descriptive complexity]] of the complexity class [[NP (complexity)|NP]], the class of problems that may be expressed in existential monadic second-order logic has been called monadic NP. The restriction to monadic logic makes it possible to prove separations in this logic that remain unproven for non-monadic second-order logic. For instance, in the [[logic of graphs]], testing whether a graph is [[Connectivity (graph theory)|disconnected]] belongs to monadic NP, as the test can be represented by a formula that describes the existence of a proper subset of vertices with no edges connecting them to the rest of the graph; however, the complementary problem, testing whether a graph is connected, does not belong to monadic NP.<ref>{{citation
Line 19 ⟶ 21:
| title = Proceedings of the Eighth Annual Structure in Complexity Theory Conference
| year = 1993}}.</ref> The existence of an analogous pair of complementary problems, only one of which has an existential second-order formula (without the restriction to monadic formulas) is equivalent to the inequality of NP and [[coNP]], an open question in computational complexity.
By contrast, when we wish to check whether a Boolean MSO formula is satisfied by an input finite [[tree (data structure)|tree]], this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to a [[tree automaton]]<ref>{{Cite journal|last=Thatcher|first=J. W.|last2=Wright|first2=J. B.|date=1968-03-01|title=Generalized finite automata theory with an application to a decision problem of second-order logic|url=https://doi.org/10.1007/BF01691346|journal=Mathematical systems theory|language=en|volume=2|issue=1|pages=57–81|doi=10.1007/BF01691346|issn=1433-0490}}</ref> and evaluating the automaton on the tree. In terms of the query, however, the complexity of this process is generally [[nonelementary problem|nonelementary]].<ref>{{Cite journal|last=Meyer|first=Albert R.|date=1975|editor-last=Parikh|editor-first=Rohit|title=Weak monadic second order theory of succesor is not elementary-recursive|url=https://link.springer.com/chapter/10.1007%2FBFb0064872|journal=Logic Colloquium|series=Lecture Notes in Mathematics|language=en|publisher=Springer Berlin Heidelberg|pages=132–154|doi=10.1007/bfb0064872.pdf|isbn=9783540374831}}</ref> Thanks to [[Courcelle's theorem]], we can also evaluate a Boolean MSO formula in linear time on an input graph if the [[treewidth]] of the graph is bounded by a constant.
For MSO formulas that have [[free variable]]s, when the input data is a tree or has bounded treewidth, there are efficient [[enumeration algorithm]]s to produce the set of all solutions<ref>{{Cite journal|last=Bagan|first=Guillaume|date=2006|editor-last=Ésik|editor-first=Zoltán|title=MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay|url=https://link.springer.com/chapter/10.1007/11874683_11|journal=Computer Science Logic|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=167–181|doi=10.1007/11874683_11|isbn=9783540454595}}</ref>, ensuring that the input data is preprocessed in linear time and that each solution is then produced in a delay linear in the size of each solution, i.e., constant-delay in the common case where all free variables of the query are first-order variables (i.e., they do not represent sets). There are also efficient algorithms for counting the number of solutions of the MSO formula.<ref>{{Cite journal|last=Arnborg|first=Stefan|last2=Lagergren|first2=Jens|last3=Seese|first3=Detlef|date=1991-06-01|title=Easy problems for tree-decomposable graphs|url=http://www.sciencedirect.com/science/article/pii/019667749190006K|journal=Journal of Algorithms|volume=12|issue=2|pages=308–340|doi=10.1016/0196-6774(91)90006-K|issn=0196-6774}}</ref>
== Satisfiability ==
The monadic second order theory of the infinite complete [[binary tree]], called S2S, is [[decidability (logic)|decidable]]. As a consequence of this result, the following theories are decidable:
| |||