-
Notifications
You must be signed in to change notification settings - Fork 1
/
minlog-examples.scm
78 lines (69 loc) · 1.24 KB
/
minlog-examples.scm
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
73
74
75
76
77
78
(add-pvar-name "A" (make-arity))
(set-goal (pf "A -> A & A"))
(assume "u")
(split)
(use "u")
(use "u")
(cdp)
(add-pvar-name "B" (make-arity))
; K
(set-goal (pf "A -> B -> A"))
(assume "u")
(assume "v")
(use "u")
(cdp)
; S
(add-pvar-name "C" (make-arity))
(set-goal (pf "(A -> B -> C) -> (A -> B) -> A -> C"))
(assume "u" "v" "w")
(use "u")
(use "w")
(use "v")
(use "w")
(cdp)
; слаба дизюнкция към силна дизюнкция
(set-goal (pf "A ord B -> (A -> bot) -> (B -> bot) -> bot"))
(assume "u" "v" "w")
(elim "u")
(use "v")
(use "w")
(cdp)
; закон на de Morgan
(set-goal (pf "((A ord B) -> bot) -> ((A -> bot) & (B -> bot))"))
(assume "u")
(split)
(assume "v")
(use "u")
(intro 0)
(use "v")
; done
(assume "v")
(use "u")
(intro 1)
(use "v")
; done
; done
(cdp)
; закон на Peirce
(set-goal (pf "((A -> B) -> A) -> A"))
(assume "u")
(use "StabLog")
(assume "v")
(use "v")
(use "u")
(assume "w")
(use "EfqLog")
(use "v")
(use "w")
(cdp)
(add-var-name "x" (py "alpha"))
(add-pvar-name "D" (make-arity (py "alpha")))
; закон на de Morgan за ∀ и ∃
(set-goal (pf "(exd x (D x) -> bot) -> all x ((D x) -> bot)"))
(assume "u")
(assume "x")
(assume "v")
(use "u")
(intro 0 (pt "x"))
(use "v")
(cdp)