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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
; Depends on sat.plf
; This file exists to support the **definition introduction** (or **extension**)
; rule in the paper:
; "Extended Resolution Simulates DRAT"
; which can be found at http://www.cs.utexas.edu/~marijn/publications/ijcar18.pdf
;
; The core idea of extended resolution is that given **any** formula f
; involving the variables from some SAT problem, one can introduce the
; constraint
;
; new <=> f
;
; without changing satisfiability, where "new" is a fresh variable.
;
; This signature does not provide axioms for facilitating full use of this
; idea. Instead, this signature facilitates use of one specific kind of
; extension, that of the form:
;
; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
;
; which translates into the clauses:
;
; new v l_1 v l_2 v ... v l_n
; new v ~old
; for each i <= n: l_i v ~new v old
;
; This kind of extension is (a) sufficient to simulate DRAT proofs and (b) easy
; to convert to clauses, which is why we use it.
; A definition witness value for:
; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n)
; It witnesses the fact that new was fresh when it was defined by the above.
;
; Thus it witnesses that the above, when added to the formula consisting of the
; conjunction all the already-proven clauses, produces an equisatisfiable
; formula.
(declare definition (! new var (! old lit (! others clause type))))
; Given `old` and `others`, this takes a continuation which expects
; 1. a fresh variable `new`
; 2. a definition witness value for:
; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n)
;
; Aside:
; In programming a **continuation** of some computation is a function that
; takes the results of that computation as arguments to produce a final
; result.
;
; In proof-construction a **continuation** of some reasoning is a function
; that takes the results of that reasoning as arguments to proof a final
; result.
;
; That definition witness value can be clausified using the rule below.
;
; There need to be two different rules because the side-condition for
; clausification needs access to the new variable, which doesn't exist except
; inside the continuation, which is out-of-scope for any side-condition
; associated with this rule.
(declare decl_definition
(! old lit
(! others clause ; List of vars
(! pf_continuation (! new var (! def (definition new old others)
(holds cln)))
(holds cln)))))
; Represents multiple conjoined clauses.
; There is a list, `heads` of literals, each of which is suffixed by the
; same `tail`.
(declare common_tail_cnf_t type)
(declare common_tail_cnf
(! heads clause
(! tail clause common_tail_cnf_t)))
; A member of this type is a proof of a common_tail_cnf.
(declare common_tail_cnf_holds
(! cnf common_tail_cnf_t type))
; This translates a definition witness value for the def:
;
; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
;
; into the clauses:
;
; new v l_1 v l_2 v ... v l_n
; new v ~old
; for each i <= n: l_i v ~new v old (encoded as (cnf_holds ...))
(declare clausify_definition
(! new var
(! old lit
(! others clause
; Given a definition { new <-> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) }
(! def (definition new old others)
(! negOld lit
(! mkNegOld (^ (lit_flip old) negOld)
; If you can prove bottom from its clausal representation
(! pf_continuation
; new v l_1 v l_2 v ... v l_n
(! pf_c1 (holds (clc (pos new) others))
; new v ~old
(! pf_c2 (holds (clc (pos new) (clc negOld cln)))
; for each i <= n: l_i v ~new v old
(! pf_cs (common_tail_cnf_holds
(common_tail_cnf
others
(clc (neg new) (clc old cln))))
(holds cln))))
; Then you've proven bottom
(holds cln)))))))))
; These axioms are useful for converting a proof of some CNF formula represented
; using the `common_tail_cnf` type (a value of type `common_tail_cnf_holds`),
; into proofs of its constituent clauses (many values of type `holds`).
; Given
; 1. a proof of some `common_tail_cnf`
; Then
; 1. the first axiom gives you a proof of the first `clause` therein and
; 2. the second gives you a proof of the rest of the `common_tail_cnf`.
(declare common_tail_cnf_prove_head
(! first lit
(! rest clause
(! tail clause
(! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail))
(holds (clc first tail)))))))
(declare common_tail_cnf_prove_tail
(! first lit
(! rest clause
(! tail clause
(! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail))
(common_tail_cnf_holds (common_tail_cnf rest tail)))))))
|
