RESOLUTE – A Simple Proof Format for SMT-LIB
Although the SMT-LIB format defines a command for obtaining proofs, it does not prescribe the format for these proofs. The only requirement is that the result follows the grammar rule for s-expr. This document explains the proof format RESOLUTE, which is the lowlevel proof format returned by the SMT solver SMTInterpol.
SMTInterpol internally can switch between different proof levels. The
lowlevel proof format described in this document can be activated by
(set-option :proof-level lowlevel)
. The goal of the
lowlevel proof format is an easy to check format. There are also the
proof-levels clauses (which adds all input clauses as oracles) and full,
which uses the internal proof rules using oracle clauses.
We have a proof checker for these proofs.
Resolution proofs
The proof is given as a resolution proof. Each subproof proves the
validity of a clause where a clause is a list of literals and a literal
is a positive or negative atom. An atom is an SMT-LIB term of sort Bool,
in other words, an SMT-LIB formula. In particular input formulas are
seen as unit clauses with a single positive atom. We use
+ t
to denote the positive literal for the term
t
and - t
for the negative literal. As usual,
a positive literal represents the fact that the term is true, a negative
literal that the term is false, and a clause represents the fact that at
least one of its literals hold.
A proof is build from the resolution rule, axioms, and assumptions. A proof is valid, if the side conditions for every axiom is fulfilled and it proves the empty clause. The main rule is the resolution rule:
The concrete syntax for the resolution rule is
(res t proof1 proof2)
where t
is the pivot
atom (an SMT-LIB term), proof1
a proof for a clause
, and proof2
a proof for a clause
. The proof (res t proof1 proof2)
is then a proof for
a new clause containing all literals from
and
where
denotes the clause
with any occurrence of the literal
removed. A clause is seen as a set of literals and literals
appearing in both
and
appear only once in the conclusion.
Furthermore, there are several axioms for the different theories. In
particular, the core theory defines the axioms for the logical
operators. As an example the axiom (or+ 1 t0 t1 t2)
where
t0
, t1
, and t2
are arbitrary
terms is a proof for the valid clause
(+(or t0 t1 t2) - t1)
.
Facts from the SMT-LIB script can be introduced using the syntax
(assume term)
, which is a proof of the unit clause
(+ term)
provided the SMT-LIB script contains the assertion
(assert term)
. A proof of the unsatisfiability of an
SMT-LIB input script is a proof of the empty clause that only uses the
assumptions appearing in the SMT-LIB script.
Axioms for core theory
The meaning of logical operators is expressed by a set of core axioms
that are available in every SMT-LIB theory. The axioms explicitly
support associative SMT-LIB operators like and
,
or
, =>
with more than two arguments.
; axioms are written as name-of-axiom: (clause)
; logical operators
true+: (+ true) false-: (- false)
not+: (+ (not p0) + p0) not-: (- (not p0 ) - p0)
and+: (+ (and p0 … pn) - p0 … - pn) and-: (- (and p0 … pn) + pi)
or+: (+ (or p0 … pn) - pi ) or-: (- (or p0 … pn) + p0 … + pn)
=>+: (+ (=> p0 … pn) +/- pi ) =>-: (- (=> p0 … pn) - p0 … + pn)
=+1: (+ (= p0 p1) + p0 + p1) =-1: (- (= p0 p1) + p0 - p1)
=+2: (+ (= p0 p1) - p0 - p1) =-2: (- (= p0 p1) - p0 + p1)
xor+: (+(xor l1) +(xor l2) -(xor l3)) xor-: (-(xor l1) -(xor l2) -xor(l3))
where each term in l1,l2,l3 occurs an even number of times.
; quantifiers
forall+: (+ (forall x (F x)) - (F (choose x (F x))))
forall-: (- (forall x (F x)) + (F t))
exists+: (+ (exists x (F x)) - (F t))
exists-: (- (exists x (F x)) + (F (choose x (F x))))
; equality axioms
refl: (+ (= t t)) symm: (+(= t0 t1) -(= t1 t0))
trans: (+(= t0 tn) -(= t0 t1) … -(= tn-1 tn))
cong: (+(= (f t0 … tn) (f t0' … tn')) -(= t0 t0') … -(= tn tn'))
=+: (+ (= t0 … tn) -(= t0 t1) … -(= tn-1 tn))
=-: (- (= t0 … tn) +(= ti tj))
distinct+: (+ (distinct t0 … tn) +(= t0 t1) … +(= t0 tn) … +(= tn-1 tn))
distinct-: (- (distinct t0 … tn) -(= ti tj)) where i != j
; ite, define-fun, annotations
ite1: (+(= (ite t0 t1 t2) t1) - t0) ite2: (+(= (ite t0 t1 t2) t2) + t0)
del!: (+(= (! t :annotation…) t))
expand: (+(= (f t0 … tn) (let ((x0 t0)…(xn tn)) d)))
where f is defined by (define-fun f ((x0 τ0)…(xn τn)) τ d)
A detailed explanation of the axioms will be given in the section Core Axioms below.
Syntactic extensions
Conceptually a resolution proof is just a big proof term applying the
resolution rule res
to axioms and assumptions. However,
there are a few important extensions to concisely express large
proof.
let-terms
A large proof may use the same large term multiple times. These large
terms can be shared between different clauses in the proof. To express
proofs in a concise manner, we support the let
syntax from
SMT-LIB to bind terms to variables. Such let
terms are seen
as syntactic sugar and are equal to their expanded form, i.e., no proof
rule is required to expand a let
. In particular, the
resolution rule will also remove the pivot literal from the proved
sub-clause if they are only identical after let expansion.
To bind a proof to a variable, the let-proof
keyword is
used with the same syntax as let
. This can be used to avoid
repeating the same subproof multiple times. This proof variable may then
be used whereever a proof is expected, e.g., as arguments of the
resolution rule.
The let-proof
syntax is also useful for expressing the
proofs in a linear form. A solver may choose to print its proof on the
fly by printing each learned clause and binding it to a variable until
it derives the empty clause:
(let-proof ((C1 (assume …)))
(let-proof ((C2 (res … C1 …)))
…
C100 ; empty clause
)…)
Function definitions
The proof format also supports custom defined functions that are only
used inside the proof. This can be usefule for auxiliary functions that
are created by Skolemization or by CNF conversion of quantified
formulas. The syntax for this is
((define-fun f ((x0 τ0)…(xn τn)) d) subproof)
where
subproof may use the function symbol f
and the
cong
and expand
axioms for this function
symbol.
Extended resolution
The proof calculus trivially supports extended resolution, where a
new literal p
is introduced that represents
(and p1 p2)
and the three clauses
(- p1 - p2 + p)
, (- p + p1)
, and
(- p + p2)
are added. This is facilitated by the
let
syntax and the axioms for logical operators as
follows:
(let ((p (and p1 p2)))
(let-proof ((C1 (and+ (and p1 p2)))
(C2 (and- 0 (and p1 p2)))
(C3 (and- 1 (and p1 p2))))
…))
Resolution proofs are usually only refutation complete, i.e., they
can prove the empty clause if the conjunction of the input clauses are
unsatisfiable. However, the addition of the core axioms makes the
calculus complete in the sense that for every valid SMT-LIB formula
t
there is a proof that proves the unit clause
(+ t)
.
The proof calculus does not support RUP proofs directly. They need to
be converted to applications of res
by explicitly listing
the clauses and pivot term used in the unit propagation subproof. More
importantly DRAT proofs are not supported and there is no syntax for
deleting clauses. Instead they need to be converted to extended
resolution (which blows up the proof quadratically). On the other hand,
this simplifies the proof checker, which would otherwise need to
rediscover the necessary clauses and subproofs.
Example Proof: eq-diamond2
We give an example proof for the following simple benchmark from the SMT-LIB benchmark set.
(set-option :produce-proofs true)
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x0 () U)
(declare-fun y0 () U)
(declare-fun z0 () U)
(declare-fun x1 () U)
(declare-fun y1 () U)
(declare-fun z1 () U)
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (not (= x0 x1))))
(check-sat)
(get-proof)
A valid output for this benchmark would be the following.
unsat
(let ((t1 (= x0 y0))
(t2 (= y0 x1))
(t3 (= x0 z0))
(t4 (= z0 x1))
(t5 (= x0 x1)))
(let ((t6 (and t1 t2))
(t7 (and t3 t4))
(t8 (not t5)))
(let ((t9 (or t6 t7)))
(let ((t10 (and t9 t8)))
(let-proof ((C0 (assume t10)))
(let-proof ((C1 (res t9 (res t10 C0 (and- 0 t10)) (or- t9))))
(let-proof ((C2 (res t8 (res t10 C0 (and- 1 t10)) (not- t8))))
(let-proof ((C3 (and- 0 t6)))
(let-proof ((C4 (and- 1 t6)))
(let-proof ((C5 (and- 0 t7)))
(let-proof ((C6 (and- 1 t7)))
(let-proof ((C7 (res t5 (res t1 C3 (res t2 C4 (trans x0 y0 x1))) C2)))
(res t5 (res t6 (res t7 C1 (res t4 C6 (res t3 C5 (trans x0 z0 x1)))) C7) C2)
))))))))))))
As mentioned earlier, the proof follows mostly the syntax of SMT-LIB
terms. In particular it uses let
and let-proof
to bind expression and sub-proofs to variables.
Introducing names for subterms
The first ten lines define names for the sub-terms of the formula
from bottom to top. Note that t10
is the asserted formula
in the input file (after variable expansion of letted variables). It is
not required to introduce an identifier for every subterm, but it is
recommended to keep the proof size small.
CNF conversion
Then C0
is defined, which is an input clause. Using the
assume
rule an input clause can be proved as a unit clause.
As usual a clause is a list of literals, which are atoms with positive
or negative polarity. In our proof calculus the atoms are SMT-LIB terms
of type Boolean. So the input formula is represented by a unit clause
containing one positive atom that is the asserted term.
Every proof rule produces a proof for a clause. The
assume
rule produces the proof that the unit clause
( + t10 )
holds. Clauses are written by listing the
literals in parenthesis and the +
indicates that the
literal has positive polarity. This proof is then assigned to the
variable C0
so it can be referenced in later proofs.
The next step is to convert the input formula into CNF. We use
C1
–C7
for the clauses resulting from the
conversion (or more precise, they are the proofs for the clauses of the
CNF). So lets look how this is done here. The input formula
t10
is
(and (or t6 t7) (not t5))
Thus, we want to split it into C1: (+ t6, + t7)
and
C2: (- t5)
. To split the and
-formula, we use
the and-elimination rule. In this example the axiom
(and- 0 t10)
is used to proof t9
from
t10
. Note that t10
is just an abbreviation for
(and t9 t8)
and that t9
is the 0th argument.
So the axiom (and- 0 t10)
proves the tautology clause
(- t10 + t9)
, which states that t9
is implied
by t10
. By resolving this clause with the input formula
t10
, we get a proof for t9
. The resolution is
written as (res t10 C0 (and- 0 t10))
, where
t10
is the pivot literal, C0 the proof of a clause
containing it positively, and (and- 0 t10)
a proof
containing it negatively. The result is a proof for
( + t9 )
.
The next step is to eliminate (or t6 t7)
, that is
t9
, using the or-elimination rule. The axiom
(or- t9)
proves the tautology clause
( -t9 + t6 + t7) )
and resolving it with the previous proof
on the pivot t9
we finally obtain C1
which is
a proof for (+ t6 + t7)
.
(let-proof ((C1 (res t9 (res t10 C0 (and- 0 t10)) (or- t9))))
Similarly we use the other and-elimination rule
(and- 1 t10)
and the not-elimination rule
(not- t8)
to obtain from C0
the clause
C2
that proves (- t5)
.
(let-proof ((C2 (res t8 (res t10 C0 (and- 1 t10)) (not- t8))))
Furthermore, we add the clauses of the Plaisted–Greenbaum-encoding
C3
–C6
. These clauses are just the
and-elimination clauses, but this time for (and t1 t2)
and
(and t3 t4)
. This gives us the full CNF of the input:
C1: (+ t6 + t7)
C2: (- t5)
C3: (- t6 + t1)
C4: (- t6 + t2)
C5: (- t7 + t3)
C6: (- t7 + t4)
SMT solving
The only unit clause C2
propagates -t5
. We
assume, the DPLL-engine now decides the literal +t6
and
propagates +t1
and +t2
by unit-propagation.
Then the theory solver finds the conflict involving transitivity:
(trans x0 y0 x1): (- t1 - t2 + t5)
By definition t1
is (= x0 y0)
,
t2
is (= y0 x1)
and t5
is
(= x0 x1)
, so the transitivity axiom for
x0 = y0 = x1
has exactly this form.
CDCL now explains the conflict to obtain C7: (- t6)
(let-proof ((C7 (res t5 (res t2 C4 (res t1 C3 (trans x0 y0 x1))) C2)))
Now unit resolution propagates -t6
, +t7
,
+t3
, and +t4
and again a theory conflict is
found:
(trans x0 z0 x1): (- t3 - t4 + t5)
The explanation yields the empty clause.
(res t5 (res t6 (res t7 C1 (res t4 C6 (res t3 C5 (trans x0 z0 x1)))) C7) C2)
This concludes the proof.
Grammar
The grammar for proofs uses the grammar for ⟨numeral⟩, ⟨term⟩, ⟨sort⟩, ⟨symbol⟩, ⟨sorted_var⟩, ⟨attribute⟩ from the SMT-LIB standard, version 2.6. It is given below:
⟨term_or_proof⟩ ::= ⟨term⟩ | ⟨proof⟩
⟨polarity⟩ ::= + | -
⟨literal⟩ ::= ⟨polarity⟩ ⟨term⟩
⟨clause⟩ ::= ( ⟨literal⟩ ⃰ )
⟨proof⟩ ::= (assume ⟨term⟩)
| (res ⟨term⟩ ⟨proof⟩ ⟨proof⟩)
| (let ((⟨symbol⟩ ⟨term⟩)⁺) ⟨proof⟩)
| (let-proof ((⟨symbol⟩ ⟨proof⟩)⁺) ⟨proof⟩)
| ⟨symbol⟩
| ((define-fun ⟨symbol⟩ (⟨sorted_var⟩⁺) ⟨term⟩) ⟨proof⟩)
| ((declare-fun ⟨symbol⟩ (⟨sort⟩⁺) ⟨sort⟩) ⟨proof⟩)
| (oracle ⟨clause⟩ ⟨attributes⟩ ⃰)
| false- | true+
| (not+ ⟨term⟩)
| (not- ⟨term⟩)
| (and+ ⟨term⟩)
| (and- ⟨numeral⟩ ⟨term⟩)
| (or+ ⟨numeral⟩ ⟨term⟩)
| (or- ⟨term⟩)
| (=>+ ⟨numeral⟩ ⟨term⟩)
| (=>- ⟨term⟩)
| (=+1 ⟨term⟩)
| (=+2 ⟨term⟩)
| (=-1 ⟨term⟩)
| (=-2 ⟨term⟩)
| (xor+ (⟨term⟩⁺) (⟨term⟩⁺) (⟨term⟩⁺))
| (xor- (⟨term⟩⁺) (⟨term⟩⁺) (⟨term⟩⁺))
| (forall+ ⟨term⟩)
| (forall- (⟨term⟩⁺) ⟨term⟩)
| (exists+ (⟨term⟩⁺) ⟨term⟩)
| (exists- ⟨term⟩)
| (refl ⟨term⟩)
| (symm ⟨term⟩ ⟨term⟩)
| (trans ⟨term⟩⁺)
| (cong ⟨term⟩ ⟨term⟩)
| (ite1 ⟨term⟩)
| (ite2 ⟨term⟩)
| (=+ ⟨term⟩)
| (=- ⟨numeral⟩ ⟨numeral⟩ ⟨term⟩)
| (distinct+ ⟨term⟩)
| (distinct- ⟨numeral⟩ ⟨numeral⟩ ⟨term⟩)
| (del! ⟨term⟩ ⟨attributes⟩ ⃰)
| (expand ⟨term⟩)
In our settings, an atom is an SMT-LIB term. A literal is a term with a polarity + or -. A clause is a set of literal, written as a sequence with a pair of parenthesis around it.
Every proof proves a clause. The whole proof given by an SMT-solver as the solution, should prove the empty clause. A proof may be produced from subproofs and for this purpose a subproof may be bound to a variable symbol, so it can be efficiently used multiple times.
The first rule, (assume t)
where t
is a
term, proves the unit clause (+ t)
. Its side condition
(checked by the proof checker) is that it was asserted in the input
problem by an SMT-LIB assert
command.
The rule (res t p1 p2)
is the resolution rule, the main
work-horse of this proof format. Here p1
is a proof that
proves some clause
and p2
a proof that proves
. The side-condition is that + t
occurs in
and - t
in
(the order of the arguments p1
and p2
is important). The resulting proof term proves the clause
.
The let binder let ((x t)) p
binds the value of
t
to a symbol x
. Here t
can be an
arbitrary term. The symbol x
can then be used in terms as
free variable. Similarly, the let binder
let-proof ((x p1)) p
binds a proof p1
to the
variable x
and x
can be referenced in
p
using the ⟨symbol⟩ rule. The scope of x
is
the proof p
and the resulting proof proves the same clause
as p
.
The oracle rule can be used to introduce clauses that cannot be easily explained. It should be used as a last resort, if a full low-level proof is too tedious, or if the axioms for the theory are missing. The proof-checker allows any oracle clause but will warn about these clauses.
The remaining rules are the low-level axioms of the proof format. Each of them creates a tautological clause. They are given in the next section.
Core Axioms
The core axioms are ⟨proof⟩ objects that prove a tautological clauses. Their inputs are usually ⟨term⟩s. We distinguish the following categories.
Logical axioms – elimination and introduction
For every logical operator we have the usual elimination and
introduction rules. In our calculus they take the form of a clause where
the premises have negative polarity and the conclusion has positive
polarity. They are also identical to the clauses that Tseitin-encoding
gives. The following list the axioms and the corresponding clause proved
by this axiom. In this list t, t0,…
denote terms,
n,i,j
denote numerals. The elimination rules are indicated
by -
and the introduction rules are indicated by
+
.
(false-): ( - false )
(true+): ( + true )
(not+ (not t)): ( +(not t) + t )
(not- (not t)): ( -(not t) - t )
(and+ (and t0 … tn)): ( +(and t0 … tn) - t0 … - tn)
(and- i (and t0 … tn)): ( -(and t0 … tn) + ti)
(or+ i (or t0 … tn)): ( +(or t0 … tn) - ti)
(or- (or t0 … tn)): ( -(or t0 … tn) + t0 … + tn)
(=>+ (=> i t0 … tn)): ( +(=> t0 … tn) + ti) (for i < n)
(=>+ n (=> t0 … tn)): ( +(=> t0 … tn) - tn)
(=>- (=> t0 … tn)): ( -(=> t0 … tn) - t0 … - tn-1 + tn)
(=+1 (= t0 t1)): ( +(= t0 t1) + t0 + t1) (only for Boolean t0/t1)
(=+2 (= t0 t1)): ( +(= t0 t1) - t0 - t1) (only for Boolean t0/t1)
(=-1 (= t0 t1)): ( -(= t0 t1) + t0 - t1) (only for Boolean t0/t1)
(=-2 (= t0 t1)): ( -(= t0 t1) - t0 + t1) (only for Boolean t0/t1)
All rules containing i
have the implicit constraint
0 <= i <= n
.
Equality rules
We support the usual axioms of reflexivity, symmetry, transitivity (with arbitrarily long chains), and congruence:
(refl t): ( +(= t t) )
(symm t0 t2): ( +(= t0 t1) -(= t1 t0) )
(trans t0 … tn): ( +(= t0 tn) -(= t0 t1) … -(= tn-1 tn) ) (for n >= 2)
(cong (f t0 … tn) (f t'0 … t'n)):
( +(= (f t0 … tn) (f t'0 … t'n))
-(= t0 t'0) … -(= tn t'n))
Additionally we have elimination and introduction rules for equality chains and for distinct:
(=+ (= t0 … tn)): ( +(= t0 … tn) -(= t0 t1) … -(= tn-1 tn))
(=- i j (= t0 … tn)): ( -(= t0 … tn) +(= ti tj))
(distinct+ (distinct t0 … tn)): ( +(distinct t0 … tn)
+(= t0 t1) … +(= t0 tn)
+(= t1 t2) … +(= t2 tn)…
+(= tn-1 tn))
(distinct- i j (distinct t0 … tn)): ( -(distinct t0 … tn) -(= ti tj)) (for i != j)
The rules containing i,j
have the implicit constraint
0 <= i <= n
, 0 <= j <= n
. For
=
we have n >= 2. for distinct
we have
n >= 1
.
ite rules
To support ite terms, we have two simple axioms:
(ite1 (ite c t e)): ( + (= (ite c t e) t) - c)
(ite2 (ite c t e)): ( + (= (ite c t e) e) + c)
xor rules
For efficient xor
reasoning we allow arbitrary split and
reordering of the xor arguments between three xor terms. The rules
are
(xor+ (t̅0) (t̅1) (t̅2): ( +(xor t̅0) +(xor t̅1) -(xor t̅2) )
(xor- (t̅0) (t̅1) (t̅2): ( -(xor t̅0) -(xor t̅1) -(xor t̅2) )
where t̅0,t̅1,t̅2
are three non-empty sequences of terms
that in total contains every term an even number of times. Furthermore,
if one of the sequences t̅i
consists of only a single term
ti
then the clause contains the atom ti
instead of the corresponding xor-term. For example:
(xor+ (t0 t1 t2) (t1) (t2 t0)): ( + (xor t0 t1 t2) + t1 -(xor t2 t0) )
(xor- (t t) (t t) (t t)): ( - (xor t t) )
Note that the last rule uses the fact that a clause is a set of literals, so multiple occurrences of literals are implicitly removed.
Quantifier instantiation and Skolemization
The rules for quantifier introduction and elimination bind the quantified variables either by an arbitrary term or use the choose operator (the Hilbert epsilon operator).
(forall+ (forall ((x0 X0) … (xn Xn)) F))
( +(forall ((x0 X0) … (xn Xn)) F)
-(let ((x0 (choose (x0 X0) (not (forall ((x1… xn Xn)) F)))))
(let ((x1 (choose (x1 X1) (not (forall ((x2… xn Xn)) F)))))
…
(let ((xn (choose (xn X)) (not F))) F)..)) )
(forall- (t0 … tn) (forall ((x0 X0) … (xn Xn)) F)):
( -(forall ((x0 X0) … (xn Xn)) F) +(let ((x0 t0) … (xn tn)) F) )
(exists+ (t0 … tn) (exists ((x0 X0) … (xn Xn)) F)):
( +(exists ((x0 X0) … (xn Xn)) F) -(let ((x0 t0) … (xn tn)) F) )
(exists- (exists ((x0 X0) … (xn Xn)) F))
( -(exists ((x0 X0) … (xn Xn)) F)
+(let ((x0 (choose (x0 X0) (exists ((x1… xn Xn)) F))))
(let ((x1 (choose (x1 X1) (exists ((x2… xn Xn)) F))))
…
(let ((xn (choose (xn X)) F)) F)..)) )
In forall- and exists+, Xi
is the type of
ti
.
Miscellaneous rules
For every symbol defined by define-fun
we have a rule
that expands the function definition. Assume f
is defined
as
(define-fun f ((x0 X0) … (xn Xn)) t)
then the expand rule for f
is
(expand (f t0 … tn)): ( + (= (f t0 … tn)
(let ((x0 t0) … (xn tn)) t)))
Note that the :named
attribute is implicitly expanded to
define-fun according to the standard and therefore the expand rule can
also be used for named terms.
For some internal functions, the expand rule is also applicable. For every function with the LEFTASSOC, RIGHTASSOC, CHAINABLE, or PAIRWISE attribute and more than two arguments expand will apply the transformation given by the SMT-LIB standard, e.g.:
(expand (or t0 … tn)): ( + (= (or t0 … tn)
(or … (or t0 t1) … tn)))
(expand (=> t0 … tn)): ( + (= (=> t0 … tn)
(or t0 … (or tn-1 tn) … )))
(expand (< t0 … tn)): ( + (= (< t0 … tn)
(and (< t0 t1) … (tn-1 tn))))
Moreover, for every internal binary function in LIRA that takes two reals, the functions for automatically casting the to real are defined. This is also supported by the expand function, even if the function is not used with more than two arguments.
(expand (+ i0 r1 i2 r3)): ( + (= (+ i0 r1 i2 r3)
(+ (to_real i0) r1 (to_real i2) r3)))
We also have a simple rule to delete attributes from input terms
(del! t :attributes…): ( + (= (! t :attributes…) t) )
Equality between terms
A proof calculus needs to define which terms are intrinsically equal. This equality relation needs to be decidable, but it should also simple for efficient implementation of proof checkers. To get a consensus when a proof is correct we need to formally define this intrinsic equality.
Equality is used by the proof checker in two places. The first is for
the side-condition of the assume
rule that states that the
assumed term must be equal to a formula asserted in the input problem.
The second is for the set operations in the resolution rule that require
that the pivot literal is contained in the clause, is removed from the
clause, and for the union operation that will remove duplicated elements
in the resolvent.
In type theory equality is usally defined by α,β,δ,…-reduction. Here we define our own reduction rules in form of a rewrite system. Two terms are equal, if they are rewritten to the same canonical term.
The rules are
x → t where x in the current context is bound to t by a let
(let (...) t) → t where t has no variable bound by let
|symbol| → symbol where symbol is a valid SMT-LIB symbol
Discussion
The above rules are minimal to keep the canonicalization of terms simple. The let rules are necessary for efficient proof representation. The |symbol| rule should help solvers whose internal representation may not differentiate between quoted and unquoted terms.
Note that any change to these rules can make existing proofs invalid. If new rules are added this may cause resolution steps to be superfluous and cause an error message that the pivot literal was not found in the antecedent clause. This could be solved by making the resolution rule more lenient, but such a change would make debugging faulty proofs much harder as then only the final emptiness check for the proved clause fails.
Clashing variable names
For the rewrite system above variable names can clash. As an example consider the following term.
(exists ((x Int)) (let ((y x)) (exists (x Int) (not (= x y)))))
When rewriting the above term using the let rules and replacing
y
by its definition x
, the proof validator
needs to remember that it binds to the outer quantifier and not to the
inner one. In particular the above term is not equal (not even
equivalent) to the term
(exists ((x Int)) (exists (x Int) (not (= x x))))
Extensions for other theories
When adding more theories, we need to add more axioms to support these theories. Here we will look into some of them.
Array Theory
We add the McCarthy axioms and an axiom for extensionality. We choose
the axiom with an explicit @diff
operator that returns some
index where two arrays differ, if they differ.
(selectstore1 a i v): ( + (= (select (store a i v) i) v) )
(selectstore2 a i j v): ( + (= (select (store a i v) j) (select a j)) + (= i j))
(extdiff a b): ( + (= a b) - (= (select a (@diff a b)) (select b (@diff a b))))
For supporting const arrays one additional axiom is needed:
(const v i): ( + (= (select (@const v) i) v) )
Linear Arithmetic
For arithmetic we need to manipulate polynomials. Polynomials are represented by an SMT-LIB term of the following form.
(+ (* c1 t11 ...t1m) ... (* cn tn1 ... tnm))
Here c1, .., cn are constants (NUMERALS, DECIMALS, or integer/real
numbers in canonical form). All (ti1…tim) are different multi-sets, the
head symbol of tij is not +
or *
. All ci,tij
have the same type (Real or Int). The constant ci can be omitted, if it
is 1 (except if there is no ti1…tin), */+ is omitted if it has only one
argument. The zero polynomial is represented by 0.
When multiplying polynomials or adding them together the usual rules of distributivity, commutativity and associativity are applied to bring them into the above normal form again.
We have four rules that manipulate these polynomial. The first two are doing polynom addition and multiplication:
(poly+ a1 .. an a): ( +(= (+ a1 ... an) a) )
where a1+...+an = a
(poly* a1 .. an a): ( +(= (* a1 ... an) a) )
where a1*...*an = a
Here a1
, …, an
, a
are
polynomials. The side-condition a1+...+an=a
states that the
polynomial resulting from adding a1
to an
together yields a polynomial equal to a
, i.e. has the same
monomials with the same coefficients, but can differ in the order of the
terms. Similarly for a1*...*an=a
.
Then we have one rule for to_real
:
(to_real a): ( +(= (to_real a) a') )
where a
is a polynomial
(+ ... (* ci ...tij...))
with integer terms and
a'
is the polynomial
(+ ... (* ci' ...(to_real tij)...))
where ci'
is the real representation of the integer ci
, i.e., an
integer NUM
is replaced with NUM.0
and
(- NUM)
is replaced with (- NUM.0)
. Every
other term t is replaced by (to_real t).
The heart of the proof system is the following rule proving the inconsistency between multiple inequalities by using Farkas’ Lemma. (Note that this is only complete for linear arithmetic).
(farkas c1 (<=? a1 b1) ... cn (<=? an bn)): ( -(<=? a1 b1) ... -(<=? an bn) )
where ci
are positive integers, <=?
stands for <
, <=
, or =
,
ai
,bi
are polynomials. The weighted sum of
these polynomials, c1*(a1-b1) + ... + cn*(an-bn)
is a
(rational or integer) constant c
where
c >= 0
. If c = 0
, then at least one
inequality must be strict. If some inequalities are Int and some are
Real, all inequalites are implicitly converted to Real by converting all
coefficients in ai/bi to real and replacing all terms t in ai/bi with
(to_real t).
The other axioms work with arbitrary terms and do not require adding or multiplying polynomials:
(trichotomy a b): ( +(< a b) +(= a b) +(< b a) )
(total a b): ( +(<= a b), (< b a) )
(>def a b): ( +(= (> a b) (< b a)) )
(>=def a b): ( +(= (>= a b) (<= b a)) )
(/def a b1 ... bn): ( +(= a (* b1 ... bn (/ a b1 ... bn))) +(= b1 0) ... +(= bn 0) )
(-def a): ( +(= (- a) (* (- 1) a)))
(-def a b1 ... bn): ( +(= (- a b1 ... bn) (+ a (* (- 1) b1)) ... (* (- 1) bn)) )
(abs-def x): ( +(= (abs x) (ite (< x 0) (- x) x)) )
The only side condition is that the terms in the clause type check.
For integer reasoning we use the following axiom that states that there
is no number between c
and c+1
:
(total-int a c): ( +(<= a c) +(<= (c+1) a) )
where c
is an integer constant (NUMERAL or negated
NUMERAL) and (c+1)
is the SMT-LIB representation of that
constant plus one. The term a
is an arbitrary term of sort
Int
. Remark: an alternative would be to restrict the axiom
to c=0: (total-int a): ( +(<= a 0) +(<= 1 a) )
Also we need the following axioms for integer and mixed integer/real reasoning:
(to_int-low x): ( +(<= (to_real (to_int x)) x) )
(to_int-high x): ( +(< x (+ (to_real (to_int x)) 1.0)) )
(div-low x d): ( +(<= (* d (div x d)) x) +(= d 0) )
(div-high x d): ( +(< x (+ (* d (div x d)) (abs d))) +(= d 0) )
(mod-def x d): ( +(= (mod x d) (- x (* d (div x d)))) +(= d 0) )
(divisible-def c x): ( +(= ((_ divisible c) x) (= x (* c (div x c)))) )
(expand (is_int x)): ( +(= (is_int x) (= x (to_real (to_int x)))) )
Note that in (divisible-def c x)
the constant
c
must be a positive numeral larger than zero, to make the
term ((_ divisible c) x)
syntactically correct.
Note that the axiom farkas
is the only axiom with
negated literals. It can be used in a resolution proof to rewrite a
positive literals into the corresponding negative literal. On the other
hand, the axiom total
and total-int
can be
used to rewrite a negative literal into the corresponding positive
literal.
Most proof rules do not use the symbols -
,
/
, >=
, >
. A solver should
first rewrite them using the definition rules and then only work with
<=
, <
, *
,
+
.
Data Types
For reasoning about data types, the following rules are used
(dt_project seli a1 ... an): (= (seli (cons a1 ... an)) ai)
(dt_cons cons x): ~((_ is cons) x), (= (cons (sel1 x) ... (seln x)) x)
(dt_test cons (cons a1 ... an)): ((_ is cons) (cons a1 ... an))
(dt_test cons' (cons a1 ... an)): ~((_ is cons') (cons a1 ... an))
(dt_exhaust x): ((_ is cons1) x), ..., ((_ is consn) x)
(dt_acyclic (cons ... x ...)): ~(= (cons ... x ...) x)
where (cons ... x ...) is a term dag containing term x and on the path
from the root to x only constructor functions appear.
(dt_match (match ..)): (= (match t ((p1 x1) c1) ...)
(ite ((_ is p1) t) (let (x1 (sel1 t)) c1)
...))