1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Pierre Weis, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 2001 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* only by permission. *)
(* *)
(***********************************************************************)
open List;;
type proposition =
| Vrai
| Faux
| Non of proposition
| Et of proposition * proposition
| Ou of proposition * proposition
| Implique of proposition * proposition
| quivalent of proposition * proposition
| Variable of string;;
exception Rfutation of (string * bool) list;;
let rec value_dans liaisons = function
| Vrai -> true
| Faux -> false
| Non p -> not (value_dans liaisons p)
| Et (p, q) -> (value_dans liaisons p) && (value_dans liaisons q)
| Ou (p, q) -> (value_dans liaisons p) || (value_dans liaisons q)
| Implique (p, q) ->
(not (value_dans liaisons p)) || (value_dans liaisons q)
| quivalent (p, q) ->
value_dans liaisons p = value_dans liaisons q
| Variable v -> assoc v liaisons;;
let rec vrifie_lignes proposition liaisons variables =
match variables with
| [] ->
if not (value_dans liaisons proposition)
then raise (Rfutation liaisons)
| var :: autres ->
vrifie_lignes proposition ((var, true) :: liaisons) autres;
vrifie_lignes proposition ((var, false) :: liaisons) autres;;
let vrifie_tautologie proposition variables =
vrifie_lignes proposition [] variables;;
let rec variables accu proposition =
match proposition with
| Variable v -> if mem v accu then accu else v::accu
| Non p -> variables accu p
| Et (p, q) -> variables (variables accu p) q
| Ou (p, q) -> variables (variables accu p) q
| Implique (p, q) -> variables (variables accu p) q
| quivalent (p, q) -> variables (variables accu p) q
| _ -> accu;;
let variables_libres proposition = variables [] proposition;;
|
