EAFormula.mli

(* This module implements formulas with global box and global diamond (A, E) *)

type formula =
  | TRUE
  | FALSE
  | AP of string (*named atom*)
  | NOT of formula
  | OR of formula * formula
  | AND of formula * formula
  | EQU of formula * formula
  | IMP of formula * formula
  | EX of string * formula (* exists, diamond of K *)
  | AX of string * formula (* forall, box of K *)
  | CONST of string (* constant functor with value string *)
  | CONSTN of string (* constant functor with value other than string *)
  | ID of formula (* modality of the identity functor *)
  | NORM of formula * formula (* default implication *)
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
  | E of formula (* global diamond *)
  | A of formula (* global box *)

val exportFormula : formula -> string

        
(* vim: set et sw=2 sts=2 ts=8 : *)