blob: ab690eb51878fc5204f29a3c41541138145114c5 (
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
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
; --------------------------------------------------------------------------------
; input :
; ( a = b )
; ( b = f(c) )
; ( a != f(c) V a != b )
; theory lemma (by transitivity) :
; ( a != b V b != f(c) V a = f(c) )
; With the theory lemma, the input is unsatisfiable.
; --------------------------------------------------------------------------------
(check
(% s sort
(% a (term s)
(% b (term s)
(% c (term s)
(% f (term (arrow s s))
; -------------------- declaration of input formula -----------------------------------
(% A1 (th_holds (= s a b))
(% A2 (th_holds (= s b (apply _ _ f c)))
(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))
; ------------------- specify that the following is a proof of the empty clause -----------------
(: (holds cln)
; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
(decl_atom (= s a b) (\ v1 (\ a1
(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3
; --------------------------- proof of theory lemma ---------------------------------------------
(satlem _ _
(ast _ _ _ a1 (\ l1
(ast _ _ _ a2 (\ l2
(asf _ _ _ a3 (\ l3
(clausify_false
; this should be a proof of l1 ^ l2 ^ ~l3 => false
; this is done by theory proof rules (currently just use "trust")
trust
))))))) (\ CT
; CT is the clause ( ~v1 V ~v2 V v3 )
; -------------------- clausification of input formulas -----------------------------------------
(satlem _ _
(asf _ _ _ a1 (\ l1
(clausify_false
; input formula A1 is ( ~l1 )
; the following should be a proof of l1 ^ ( ~l1 ) => false
; this is done by natural deduction rules
(contra _ A1 l1)
))) (\ C1
; C1 is the clause ( v1 )
(satlem _ _
(asf _ _ _ a2 (\ l2
(clausify_false
; input formula A2 is ( ~l2 )
; the following should be a proof of l2 ^ ( ~l2 ) => false
; this is done by natural deduction rules
(contra _ A2 l2)
))) (\ C2
; C2 is the clause ( v2 )
(satlem _ _
(ast _ _ _ a3 (\ l3
(ast _ _ _ a1 (\ l1
(clausify_false
; input formula A3 is ( ~a3 V ~a1 )
; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
; this is done by natural deduction rules
(contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))
))))) (\ C3
; C3 is the clause ( ~v3 V ~v1 )
; -------------------- resolution proof ------------------------------------------------------------
(satlem_simplify _ _ _
(R _ _ C1
(R _ _ C2
(R _ _ CT C3 v3) v2) v1)
(\ x x))
))))))))))))))))))))))))))
)
|
