Monadic second-order logic: Difference between revisions

Revision as of 21:31, 25 March 2017

Revision as of 22:03, 25 March 2017

Line 1:

In [[mathematical logic]], '''monadic second order logic (MSO)''' is the fragment of [[Higher-order logic|second-order logic]] where the second-order quantification is limited to quantification over [[Monadic predicate calculus|monadic first-order predicates]] (frequently treated as "sets").<ref>{{cite book|first1=Bruno|last1=Courcelle|author1-link=Bruno Courcelle|first2=Joost|last2=Engelfriet| title=Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach| publisher=Cambridge University Press|date=2012-01-01|isbn=978-0521898331|url=http://dl.acm.org/citation.cfm?id=2414243|accessdate=2016-09-15}}</ref> It is particularly important in the [[logic of graphs]], because of [[Courcelle's theorem]], which provides algorithms for evaluating monadic second-order formulas over certain types of graphs.

Existential monadic second-order logic (EMSO) is the [[Fragment (logic)|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, testing the [[Connectivity (graph theory)|connectivity of graphs]] belongs to monadic co-NP (the [[Complement (set theory)|complement]] of monadic NP) but not to monadic NP itself.<ref>{{citation