Просмотр кода страницы Logic for expressing graph properties

'''Logic for expressing graph properties''' --- логика для выражения
свойств графа. 

Any labelled graph may be defined as a logical structure

<math>(V_{G}, E_{G}, (lab_{a,G})_{a \in C_{V}}, (edg_{b,G})_{b \in C_{E}})</math>

where <math>V_{G}</math> is the set of vertices,  <math>E_{G}</math> is the  set  of  edges,
<math>C_{V}</math> is a set of vertex labels and <math>C_{E}</math> is a set of edge labels,
moreover, the meaning of the predicates is the following:

(1) <math>lab_{a,G}(v)</math> is true iff the vertex <math>v</math> has <math>a</math>-label in <math>G</math>,

(2) <math>edg_{b,G}(e,v,v')</math> is true iff <math>e</math> is an edge <math>(v,v')</math> in <math>G</math> and has
a <math>b</math>-label in <math>G</math>.

To define the sets of graphs, one considers formulas built by using
individual variables (vertex variables or edge variables), set
variables (sets of vertices or sets of edges) and binary relation
variables (subsets of <math>V_{G} \times V_{G}</math> or <math>V_{G} \times E_{G}</math> or
<math>E_{G} \times E_{G}</math>).

'''Atomic formulas''' are the following:

(1) <math>x = x'</math>, where <math>x,x'</math> are two vertices or two edges;

(2) <math>lab_{a}(v)</math>, where <math>v</math> is a vertex;

(3) <math>edg_{b}(e,v,v')</math>, where <math>e</math> is an edge and <math>v, v'</math> are two
vertices;

(4) <math>x \in X</math>, where <math>X</math> is a set of vertices or a set of edges;

(5) <math>(x,y) \in R</math>, where <math>R</math> is a binary relation included in a
cartesian product <math>X \times Y</math> with <math>X</math> which is a set of vertices or
a set of edges, the same for <math>Y</math>.


A '''First Order formula''' is a formula formed with the above
atomic formulas numbered from (1) to (3) together with boolean
connectives ''' OR, AND, NOT''', the individual quantifications
<math>\forall x, \exists x</math> (where <math>x</math> is a vertex or an  edge).

A '''Monadic Second Order formula''' is a formula formed with the above
atomic
formulas numbered from (1) to (4) together with boolean
connectives ''' OR, AND, NOT''', the individual quantifications
<math>\forall x, \exists x</math> (where <math>x</math> is a vertex or an edge) and the set
quantifications <math>\forall X, \exists X</math> (where <math>X</math> is a set of vertices
or a set of edges).

A '''Second Order formula''' is a formula formed with the above
atomic formulas numbered from (1) to (5) together with boolean
con\-nec\-tives '''OR, AND, NOT''', the individual quantifications
<math>\forall x, \exists x</math> (where <math>x</math> is a vertex or an edge), the set
quantifications <math>\forall X, \exists X</math> (where <math>X</math> is a set of vertices
or a set of edges) and the binary relations quantifications <math>\forall
R, \exists R</math> (where <math>R</math> is a binary relation).