infix 5 -- ==> <=>;
infix 3 >>;
infix 0 || @@;
infix 4 &&;

signature PROPOSITIONSIG = 
    sig 
	eqtype Name

datatype Term = ^^ of Name
  | ?  of Name

and Predicate = % of Name
  | ==
 
datatype Type = Type of Name | Either of Type list | Object

datatype 'a TypedList = TypedList of ('a list * Type) list
val forgetTypes : 'a TypedList -> 'a list
val @@ : 'a TypedList * 'a TypedList -> 'a TypedList
val printType : Type -> string
val printTypedList : Term TypedList -> (Term -> Term) -> string

	(* a substitution maps variables to constants (Term -> Term)
	 substitutions types constants parameters 
	 is a list of all well-typed substitutions instantiating the parameters *)
val substitutions :
     Name TypedList ->
     Term TypedList -> Term TypedList -> (Term -> Term) list 

datatype Lit = !! of Predicate * Term list

val mkLit : Predicate * Term list -> Lit

datatype
    Formula =   
        (* Conjunction *)
        && of Formula * Formula
      | &&& of Formula list
      | ==> of Formula * Formula
      | <=> of Formula * Formula
      | A of Lit                     (* Atom  *)
      | F                            (* False *)
      | T                            (* True  *)
      | || of Formula * Formula
      | ||| of Formula list
      | ~ of Formula
      | ALL of Term TypedList * Formula
      | EXS of Term TypedList * Formula
      | LT  of (int *  Term TypedList) * Formula 
      | GT  of (int *  Term TypedList) * Formula
      | EQ  of (int *  Term TypedList) * Formula
      | GE  of (int *  Term TypedList) * Formula
      | LE  of (int *  Term TypedList) * Formula

val tr : (Term -> Term)  -> Lit -> Lit 
val predicatesInFormula : Formula -> Predicate list
val uniquePredicates :  Predicate list list ->  Predicate list
val lit2string : Lit -> string
val form2string : Formula -> string

val simp : Formula -> Formula

end