From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- contrib/dp/fol.mli | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 contrib/dp/fol.mli (limited to 'contrib/dp/fol.mli') diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli new file mode 100644 index 00000000..a85469cc --- /dev/null +++ b/contrib/dp/fol.mli @@ -0,0 +1,48 @@ + +(* Polymorphic First-Order Logic (that is Why's input logic) *) + +type typ = + | Tvar of string + | Tid of string * typ list + +type term = + | Cst of int + | Plus of term * term + | Moins of term * term + | Mult of term * term + | Div of term * term + | App of string * term list + +and atom = + | Eq of term * term + | Le of term * term + | Lt of term * term + | Ge of term * term + | Gt of term * term + | Pred of string * term list + +and form = + | Fatom of atom + | Imp of form * form + | Iff of form * form + | And of form * form + | Or of form * form + | Not of form + | Forall of string * typ * form + | Exists of string * typ * form + | True + | False + +(* the integer indicates the number of type variables *) +type decl = + | DeclType of string * int + | DeclFun of string * int * typ list * typ + | DeclPred of string * int * typ list + | Axiom of string * form + +type query = decl list * form + + +(* prover result *) + +type prover_answer = Valid | Invalid | DontKnow | Timeout -- cgit v1.2.3