From 0632a399ae7aad808915602a4d686819f4c8900e Mon Sep 17 00:00:00 2001
From: raspbeguy <raspbeguy@hashtagueule.fr>
Date: Mon, 7 Mar 2016 19:42:13 +0100
Subject: [PATCH] initial

---
 README.md |  9 ++++++++
 demo.ml   | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 72 insertions(+)
 create mode 100644 README.md
 create mode 100644 demo.ml

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..1f8231a
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+#Démonstrateur automatique en Caml
+
+Implémenté avec amour en Caml.
+
+Je ne sais absolument plus l'utiliser (ça date de 2013) alors si quelqu'un sait, je l'autorise à s'acheter un Carambar.
+
+Utilise le [système de Gentzen de calcul de séquent] (http://www.pps.univ-paris-diderot.fr/~kesner/enseignement/licence/logique/Gentzen-predicats-4.pdf).
+
+Joie et bonheur sur vos familles.
diff --git a/demo.ml b/demo.ml
new file mode 100644
index 0000000..aa1d5ad
--- /dev/null
+++ b/demo.ml
@@ -0,0 +1,63 @@
+type formule = 
+  | Atome of string
+  | Et of formule * formule
+  | Ou of formule * formule
+  | Non of formule
+  | Fleche of formule * formule;;
+
+let rec appartient x l =
+  match l with
+    | [] -> false
+    | t::q -> (x = t) || appartient x q;;
+
+let rec commun l1 l2 = (*definition d'axiome*)
+  match l1 with
+    | [] -> false
+    | t::q -> (appartient t l2) || (commun q l2);;
+
+let rec addgauche f l =
+  match l with
+    | [] -> []
+    | t::q -> match t with (x,y) -> (f::x,y)::(addgauche f q);;
+
+let rec adddroite f l =
+  match l with
+    | [] -> []
+    | t::q -> match t with (x,y) -> (x,f::y)::(adddroite f q);;
+
+(* Les deux fonctions precedentes ne sont utilisees qu'une fois, et il faut juste
+ * savoir qu'elles permettent de considerer le cas "atomique" d'une formule*)
+
+let rec atomique f = (*teste si une liste de formule est inexpendable*)
+  match f with
+    | [] -> true
+    | t::q -> match t with
+        | Atome(a) -> atomique q
+        | _ -> false;;
+
+let rec developgauche f g = (*Application des regles gauches*)
+  match f with
+    | [] -> [(f,g)]
+    | t::q -> match t with
+        | Atome(a) -> addgauche t (developgauche q g)
+        | Et(a,b) -> [((a::b::q),g)]
+        | Ou(a,b) -> [((a::q),g);((b::q),g)]
+        | Non(a) -> [(q,(a::g))]
+        | Fleche(a,b) -> [(q,(a::g));((b::q),g)];;
+
+let rec developdroite f g = (*Application des regles droites*)
+  match g with
+    | [] -> [(f,g)]
+    | t::q -> match t with
+        | Atome(a) -> adddroite t (developdroite f q)
+        | Et(a,b) -> [(f,(a::q));(f,(b::q))]
+        | Ou(a,b) -> [(f,(a::b::q))]
+        | Non(a) -> [((a::f),q)]
+        | Fleche(a,b) -> [((a::f),(b::q))];;
+
+let rec calcul l =
+  match l with
+    | [] -> true
+    | (f,g)::q -> if atomique f then if atomique g then (commun f g) && (calcul q)
+      else (calcul (developdroite f g)) && (calcul q)
+      else (calcul (developgauche f g)) && (calcul q);;