Theory.md

 # Typed Constraint Graph
 
 In the heart of the NDL language lies a specific representation of Constraint Programming Problems. Instead of using a common Constraint (Hyper-) Graph formalization, we introduce a Typed Constraint Graph, that enriches the Constraint Graphs with types, representing the higher level structure of the problem.
+
+Typed Constraint Graph is a Labeled Directed Multigraph with no self-loops. Formally, it's an 8-tuple $`G = \left \langle V, A, s, t, \Sigma, \Theta, l, \theta \right \rangle`$, where:
+*  $`V`$ is a set of vertices
+*  $`A`$ is a set of edges
+*  $`s`$ and $`t`$ are both maps $`A \rightarrow V`$ pointing at the *source* and *target* vertices of an arc  
+* $`\Sigma`$ is a set of the arc labels
+* $`\Theta`$ is a set of the vertex labels 
+* $`l: A \rightarrow \Sigma`$ maps arcs to their labels
+* $`\theta: V \rightarrow \Theta`$ maps vertices to their labels
+
+