Represent regular classes of structures.
Basic Type Definition.
Sum of structures or specified classes with relation replacements.
(string * struct_sum list) list
Class of regular structures.
val struct_sum_str :
struct_sum -> string
Print a class definition (right hand side) as string.
val str :
structure_class -> string
Print a regular structure class as a string, using its definition.
Split with atom replacing.
val split :
Formula.formula -> struct_sum -> Formula.formula
Split of a sentence on a class definition is either true/false if the class
definition is a Struct s (depending on whether s |= phi or not), or a new
sentence psi such that, e.g. for the sum A:c + B:d, following is replaced:
- each exists x (phi) by (exists "A:c:x" phi) or (exists "B:d:x" phi)
- each exists X (phi) by exists "A:c:X" "B:d:X" (phi), x in X-> x in X1 or X2
- dually the forall quantifiers
- each resulting atom, say R(A:c:x, B:d:y), as given in WITH reldefs.
val split_simplify :
?get_ids:bool -> Formula.formula -> struct_sum -> Formula.formula
Split the formula as above and simplify by replacing trivially true
or false atoms such as L(x:R) ...
Decomposing a formula for a class definition.
val decompose :
Formula.formula -> struct_sum -> (string * Formula.formula) list list
Compute a decomposition of a formula on a given class definition.
WMSO model checking on inductive structures
val check :
string -> structure_class -> Formula.formula -> bool