blob: 27c61de1f7c2658d4ccf68f2b371fb7247a45ff8 (
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
|
; Depends on er.plf
; Type for representing success when testing a side-condition
(declare TestSuccess type)
; Test for clause_add_suffix_all
(declare test_clause_add_suffix_all
(! list clause
(! suffix clause
(! result cnf
(! (^ (clause_add_suffix_all list suffix) result)
TestSuccess)))))
(check
(% a lit
(% b lit
(% c lit
(test_clause_add_suffix_all
(clc a (clc b cln))
(clc c cln)
(cnfc (clc a (clc c cln))
(cnfc (clc b (clc c cln))
cnfn))
)
)))
)
; This is a circuitous proof that uses the definition introduction and
; unrolling rules
(check
(% v1 var
(% v2 var
(% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln)))
(% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln)))
(% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln)))
(% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln)))
(: (holds cln)
(decl_definition
(neg v1)
(clc (neg v2) cln)
(\ v3
(\ def3
(clausify_definition _ _ _ def3 _ _
(\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
(\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
(\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn))
(cnfc_unroll_towards_bottom _ _ pf_cnf3
(\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln)))
(\ pf_cnfn
; Clauses
(satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2
(satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3
(satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1
(satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1
(satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2
(satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty
pf_c13
))
))
))
))
))
))
)))
)))
)
))
)
)
))))
))
)
; This is a test of ER proof produced by drat2er on Example 1 from:
; https://www.cs.utexas.edu/~marijn/drat-trim/
(check
(% v1 var
(% v2 var
(% v3 var
(% v4 var
(% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
(% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
(% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
(% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
(% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
(% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
(% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
(% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
(: (holds cln)
(decl_definition
(neg v1)
cln
(\ v5
(\ def1
(clausify_definition _ _ _ def1 _ _
(\ pf_c9 ; type: (holds (clc (pos def1v) cln))
(\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
(\ idc0 ; type: (cnf_holds cnfn)
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
(satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14
(satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15
(satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16
(satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17
(satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18
pf_c18
))))))))))))))))
)))
)
))
)
)
))))))))
))))
)
|
