blob: afbdc7d4f3e88b4ece390843b644ada224e1c8f7 (
plain)
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
|
(** reprezentacja formuł *)
type formula = False | Var of string | Imp of formula * formula
val pp_print_formula : Format.formatter -> formula -> unit
(** reprezentacja twierdzeń *)
type theorem
(** założenia twierdzenia *)
val assumptions : theorem -> formula list
(** teza twierdzeni *)
val consequence : theorem -> formula
val pp_print_theorem : Format.formatter -> theorem -> unit
(** by_assumption f konstuuje następujący dowód
-------(Ax)
{f} ⊢ f *)
val by_assumption : formula -> theorem
(** imp_i f thm konstuuje następujący dowód
thm
Γ ⊢ φ
---------------(→I)
Γ \ {f} ⊢ f → φ *)
val imp_i : formula -> theorem -> theorem
(** imp_e thm1 thm2 konstuuje następujący dowód
thm1 thm2
Γ ⊢ φ → ψ Δ ⊢ φ
------------------(→E)
Γ ∪ Δ ⊢ ψ *)
val imp_e : theorem -> theorem -> theorem
(** bot_e f thm konstruuje następujący dowód
thm
Γ ⊢ ⊥
-----(⊥E)
Γ ⊢ f *)
val bot_e : formula -> theorem -> theorem
|
