History | View | Annotate | Download (289 Bytes)

(* transforms list of gml formulas (diamond?,number,formula)

to list of consequences (positive?,formula),

here positive? means that the formula must be true in order to make the

given conjunct of modalities true *)

val gml_rules : (bool*int*int) list -> (int*bool) list list list