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
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(* Sequent Calculus *)
open Types
open To_string
type seq = Seq of proposition list * proposition list;; (* sequent *)
type stree = (* tree of sequents *)
| Taut (* tautology of the form A, Gamma => A, Delta *)
| Br of stree * stree
let string_of_seq (Seq (p1, p2)) =
let rec string_of_prop_list = function
| [] -> ""
| p :: ps -> (string_of_prop p) ^ ", " ^ (string_of_prop_list ps)
in
(string_of_prop_list p1) ^ "⇒" ^ (string_of_prop_list p2);;
(* let rec reduce_seq s =
let rec not_lhs (Seq(p1s, p2s)) =
match p1s with
| [] -> Seq(p1s, p2s), None, false
| p::ps ->
(match p with
| Not(p') -> Seq(ps, p'::p2s), None, true
| _ -> let Seq(ps', p2s), _, found = not_lhs (Seq(ps, p2s)) in Seq(p::ps', p2s), None, found)
in
let rec not_rhs (Seq(p1s, p2s)) =
match p2s with
| [] -> Seq(p1s, p2s), None, false
| p::ps ->
(match p with
| Not(p') -> Seq(p'::p1s, ps), None, true
| _ -> let Seq(p1s, ps'), _, found = not_rhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
in
let rec and_lhs (Seq(p1s, p2s)) =
match p1s with
| [] -> Seq(p1s, p2s), None, false
| p::ps ->
(match p with
| And(p1, p2) -> Seq(p1::p2::ps, p2s), None, true
| _ -> let Seq(p1s, ps'), _, found = and_lhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
in
let rec and_rhs (Seq(p1s, p2s)) =
match p2s with
| [] -> Seq(p1s, p2s), None, false
| p::ps ->
(match p with
| And(p1, p2) -> Seq(p1s, p1::ps), Some (Seq(p1s, p2::ps)), true
| _ ->
(match and_rhs (Seq(p1s, ps)) with
| Seq(p1s, ps'), None, found -> Seq(p1s, p2s), None, false
| Seq(p1s, ps'), Some (Seq(p1s', ps'')), found -> Seq(p1s, p::ps'), Some (Seq(p1s', p::ps'')), true))
in
match s with
| Seq *)
(*
Steps (repeat in this order):
- reduce AND on LHS
- reduce OR on RHS
- reduce NOT on LHS
- reduce NOT on RHS
- reduce -> (RHS)
- reduce <-> (both)
- reduce OR (LHS)
- reduce AND (RHS)
- reduce -> (LHS)
*)
|
