aboutsummaryrefslogtreecommitdiff
path: root/semestr-3/pf/lista5/proof/logic.mli
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