We present a simple resolution-based proof format targeted for SMT. The proof format uses a syntax similar to SMT-LIB terms. The resolution rule is its only proof rule with premises; all other rules are axioms proving tautological clauses. The format aims to be solver-independent by only including a minimal complete set of axioms while still being able to express proofs succinctly. Most of its axioms are purely syntactic; only for arithmetic reasoning, some axioms with side conditions are used for succinct reasoning with linear (in)equalities. The format can be extended with solver-specific rules, which can then either be treated as trusted axioms, or, better, replaced by their low-level proof. The format has been implemented in the solver SMTInterpol and the solver produces proofs for all benchmarks it can solve in the combinations of the theories of equality, linear arithmetic, arrays and datatypes. There is also a stand-alone proof checker for this format.
SMT solvers have become an integral part of many modern verification techniques. They are used to prove the absence of errors in complex systems that cannot be verified by hand. This begs the question whether the solvers themselves are correct.
Many SMT solvers can support their answer on the satisfiability problem of a formula by
providing either a model for a satisfiable formula, or a proof for an unsatisfiable formula. The
SMT-LIB standard [
In this paper we present a very simple but expressive proof format that we propose as a candidate for such a standard. Our proof format uses the resolution rule known from SAT proofs and combines it with axioms for SMT theories. We propose to use a minimal complete set of axioms, and the idea is that a solver needs to explain its theory lemmas using only these axioms. An important idea is that even the meaning of the built-in logical symbols like not and or is given by axioms that correspond to the Tseitin transformation. Thus, even the conversion into conjunctive normal form (CNF) can be explained in this format. By implementing the proof format in SMTInterpol, we have shown that despite the minimality of the axiom set, the overhead of generating proofs is manageable (it is linear in the run-time of the solver).
We claim that our proof format solves the following goals: (1) it is easy and fast to verify, (2) it avoids solver-specific rules, (3) it supports several reasoning techniques, from equality rewriting to symmetry breaking, (4) it enables short proofs that are linear in the number of reasoning steps the solver took.
We use the SMT-LIB [
We use typewriter font for literal SMT-LIB terms, stands for an SMT-LIB term and for an SMT-LIB formula (term of type Bool). We use the symbol f for an (uninterpreted or theory) function symbol, the symbol for variables, and for SMT-LIB sorts. We use prf for proof terms. In linear arithmetic, we use for a polynomial.
Our proof format is a resolution proof that shows unsatisfiability by deriving the empty clause. The leaves of the proof are input formulas and axioms. The only proof rule is the resolution rule that proves from two given clauses a resolvent.
{} ∪ 1 {¬} ∪ 2 1 ∪ 2 (res) A clause is a set of literals, which is interpreted as the disjunction of these literals. A literal is a positive or negated atomic formula. The core idea of our proof format is that atomic formulas are exactly the SMT-LIB formulas, i.e., SMT-LIB terms of type Bool.
As far as the proof format is concerned, the atomic formulas are opaque and even the built-in SMT-LIB functions and, or, not have no predefined meaning. Instead the meaning is given by axioms that can be seen as a set of theory lemmas for the core theory. For each SMT-LIB formula , there are the axioms (not+ ) : {(not ), }2 and (not- ) : {¬(not ), ¬}. Similarly, the axioms (or- 0 1) : {¬(or 0 1), 0, 1}, (or+ 0 0 1) : {(or 0 1), ¬0}, and (or+ 1 0 1) : {(or 0 1), ¬1} define the meaning of (or 0 1).
The syntax of proof terms is similar to the syntax of SMT-LIB terms. The simplest proof term is an axiom, e.g., (not+ ). Moreover, for each assertion (assert ) in the SMT-LIB 2We write prf : to denote that prf is an axiom stating the validity of the clause . (set-option :produce-proofs true) (set-logic QF_UF) (declare-fun q1 () Bool) (declare-fun q2 () Bool) (assert (or (not q1) q2)) (assert q1) (assert (not q2)) (check-sat) (get-proof) unsat (res q1 (assume q1) (res q2 (res (not q1) (res (or (not q1) q2) (assume (or (not q1) q2)) (or- (not q1) q2)) (not- q1)) (res (not q2) (assume (not q2))
(not- q2)))) assume {(or (not q1) q2)}
(or- (not q1) q2) {¬(or (not q1) q2), (not q1), q2}
(not- q1) {(not q1), q2} {¬(not q1), ¬q1} assume {q1} {q2, ¬q1} {} {¬q1}
assume {(not q2)}
(not- q2) {¬(not q2), ¬q2} {¬q2} input, the proof term (assume ) proves the unit clause {}. The concrete syntax for the resolution rule is (res prf 1 prf 2) where is the pivot atom and prf 1 and prf 2 are the proof terms for the subproofs. Figure 1 shows a simple proof for the unsatisfiabilty of the assertions (or (not q1) q2), q1, (not q2), where q1, q2 are constants of type Bool. Each proof term proves a clause and the whole proof of unsatisfiability is correct if it proves the empty clause.
Sharing Proofs and Subterms. Proofs often use the same intermediate clause several times. For a succinct representation of such proofs, repeated subproofs may be bound to variables, e.g., the syntax
(let-proof ((C (res (not q) (assume (not q)) (not- q)))) prf ) binds the proof of {¬q} to the variable C. This variable may then be used in prf , i.e., it may be given as argument to res applications whenever a resolution with this clause should be performed. Note that the syntax is similar to the let-syntax for SMT-LIB terms. Furthermore the proof format also supports the let binder with the identical syntax as for SMT-LIB terms to bind terms to variables that are used in axioms or as pivot atoms multiple times. The latter is important for keeping the proof size down, because large subterms may naturally appear several times, for example in proofs where a large input formula is converted into CNF. In fact, in most proofs produced by our solver, every subterm of every asserted term is bound to a variable because it is used multiple times in the proof. In general, proofs grow exponentially if let terms are expanded.
In our proof format, let and let-proof are syntactic sugar and equivalent to their expanded form where every variable is replaced by its definition. As an example,
(let ((x (not q2))) (res x (assume x) (not- q2))) is a valid subproof because x is implicitly expanded to (not q2) and the pivot atom matches the negated atom in the clause (not- q2) : {¬(not q2), ¬q2}. There is no proof rule for let expansion as both the expanded and contracted term are seen as the same term. Internally, our proof checker expands all let terms, using a DAG representation to avoid exponential blow-up.
The two diferent binders let-proof for proofs and let for terms simplify parsing. If let would be used for both, then symbols like res, and+, etc. would need to become predefined symbols and must not be used as user-defined symbols in benchmarks. By using two diferent binders, it is clear from the context whether a term is a proof term or an SMT-LIB term. Defining Functions. In proofs it may be desirable to have prover-defined auxiliary functions that do not appear in the input problem. Our proof format uses the syntax
((define-fun f ((1 1) ...( )) ) prf ) where f is a function symbol and the defining term that uses the variables 1, . . . , of type 1, . . . , . The whole proof term proves the same clause as its subproof prf proves. The subproof prf may use f as if it was a user-defined function. In particular, prf can contain the axioms cong and expand from the core theory.
Oracles. Sometimes it is useful to state a fact without proving it, e.g., because a rigorous proof requires new axioms (when extending the format to a new theory) or because a simplification step should be expressed in proofs before reducing it to the axioms of the theory at a later time. Our proof format supports an oracle axiom with the following syntax.
(oracle ± 1 . . . ± Attributes) Here ± is + (positive literal) or - (negated literal) and Attributes is a user-defined list of keyvalue pairs of the form :key value, where :key is an identifier prefixed by a colon and value an arbitrary s-expression or empty. The oracle itself proves the clause {(¬) 1, . . . , (¬) } where the literal is negated if and only if was prefixed by - in the axiom.
To provide meaning for the built-in SMT-LIB functions of the core theory, several axioms are defined, see Figure 2 for a complete list. For each logical operator there is an introduction axiom, e.g., and+, and an elimination axiom, e.g., and-. These can be used to eliminate or =-1 : {¬(= 0 1), 0, ¬1} =+2 : {(= 0 1), ¬0, ¬1} =-2 : {¬(= 0 1), ¬0, 1} xor+ : {(xor 1), (xor 2), ¬(xor 3)} xor- : {¬(xor 1), ¬(xor 2), ¬(xor 3)} where 1,2,3 are lists of formulas and each formula occurs an even number in total forall+ : {(forall (( )) ), ¬(let (( (choose ( ) (not )))) )} forall- : {¬(forall (( )) ), (let (( )) )} exists+ : {(exists (( )) ), ¬(let (( )) )} exists- : {¬(exists (( )) ), (let (( (choose ( ) ))) )} refl : {(= )}
symm : {(= 0 1), ¬(= 1 0)} trans : {(= 0 ), ¬(= 0 1), . . . , ¬(= − 1 )} cong : {(= (f 0 . . . ) (f ′0 . . . ′)), ¬(= 0 ′0), . . . , ¬(= ′)} =+ : {(= 0 . . . ), ¬(= 0 1), . . . , ¬(= − 1 )} =- : {¬(= 0 . . . ), (= )} distinct+ : {(distinct 0 . . . ), (= 0 1), . . . , (= 0 ), . . . , (= − 1 )} distinct- : {¬(distinct 0 . . . ), ¬(= )} ite1 : {(= (ite 0 1 2) 1), ¬0} ite2 : {(= (ite 0 1 2) 2), 0} del! : {(= (! . . .) )} expand : {(= (f 0 . . . ) (let ((0 0). . .( )) ))}
where f is defined by (define-fun f ((0 0)...( )) ) introduce the corresponding operator into the formula by applying the resolution rule. The axioms are written as application terms that take the instantiated terms as arguments, e.g., (and+ 0 1) : {(and 0 1), ¬0, ¬1}. The axioms and-, or+, =>+, =-, distinct- take as additional argument the value (and ), a literal number between 0 and , e.g., (and- 0 0 1) : {¬(and 0 1), 0}.
Boolean equality in SMT-LIB corresponds to logical equivalence. We define corresponding introduction and elimination axioms =+1 to =-2. These rules may only be used on terms of type Bool and this has to be verified by the proof checker.
Quantifiers are supported using the SMT-LIB 3.0 choose operator, which is Hilbert’s epsilon operator. For brevity, the figure shows the axioms only for one variable, but they are also supported for multiple variables, e.g., the axiom exists- is the following.
(exists- ((1 1) . . . ( )) ) : {¬(exists ((1 1) . . . ( )) ), (let ((1 (choose (1 1) (exists ((2 2) . . . ( )) )))) (let ((2 (choose (2 2) (exists ((3 3) . . . ( )) )))) . . .
(let (( (choose ( ) ))) )· · · ))} The axioms from refl to distinct- are the axioms for the theory of equality. They can also be used for Boolean equality (logical equivalence) and cong can also be used on built-in function symbols like and or even = itself. The axioms ite1 and ite2 can be used for Boolean and non-Boolean ite terms. The axiom del! states that adding annotations to an SMT-LIB term does not change its meaning. Finally, the axiom expand can be used to expand user-defined and prover-defined (see Section 3) function symbols. 4.1. Axioms for Linear Arithmetic For linear arithmetic, purely syntactic rules come to their limit, for example, when proving arithmetic operations on rationals like {(= (+ (/ 1.0 3.0) (/ 1.0 6.0)) (/ 1.0 2.0))}. To ease the reasoning about arithmetic, our proof format has some built-in axioms with side conditions that use addition and/or multiplication of rational numbers and polynomials.
We use the SMT-LIB canonical form for numeric constants, with a slight alteration for rationals. In SMT-LIB, the number 1 of type Real is represented as 1 in the logic LRA and as 1.0 in the logic LIRA. We use 1.0 in both logics. Similarly, we always represent fractions as (/ 1.0 3.0) or (/ (- 2.0) 3.0) (like in SMT-LIB, fractions need to be reduced).
We define a polynomial as a finite map from multisets of SMT-LIB terms to non-zero rational coeficients. Each entry {1, . . . , } ↦→ of this map is a monomial, which is represented as (* 1 . . . ) in SMT-LIB. In this representation, can be omitted if = 1 and > 0. The multiplication symbol is omitted if it has only one argument. The terms 1, . . . , must not be applications of + or * and they must not be numeric constants in canonical form. A polynomial is either of type Real or Int and all terms in all multiset must be of the same type and all coeficients must be integral if the polynomial is of type Int. The term representing a polynomial is (+ 1 . . . ) where 1, . . . , are the monomial representations of the entries of the map. A polynomial with a single entry in the map is represented by 1 and the empty map is represented by 0 or 0.0. As an example, the polynomial {{x, x} ↦→ 2, {x} ↦→ 1, {} ↦→ 1} with x of type Int is represented by the SMT-LIB term (+ (* 2 x x) x 1).
A polynomial can have several representations that difer in the order of the terms, but each SMT-LIB term can only be the representation of at most one polynomial. The sum 1 + 2 of two polynomials 1, 2 is built by conjoining the maps, adding the rational constants if the same multiset appears in both polynomials, and removing the entries whose sum of the constants is zero. The product 1 · 2 is built by computing the sum of the products for each pair of monomials. The product of two monomials is just the union of the multisets mapped to the product of the rational constants. A polynomial of type Int can be cast to real by surrounding each term in each multiset with a to_real application and converting the coeficients to real by appending .0 to the constant. A polynomial is a constant, if it is zero (the empty map) or a singleton map whose multiset is empty. Note that the representation of a constant polynomial is the constant term in canonical form.
Figure 3 shows the axioms for linear arithmetic. The first two axioms poly+ and poly* can be used to simplify arithmetic terms in the input formula and have a side condition that requires polynomial addition or multiplication, respectively. Note that the resulting polynomial has to be given in the proof, as its SMT-LIB representation is not unique, e.g., the axioms (poly+ (+ x y x) (+ (* 2 x) y)) and (poly+ (+ x y x) (+ y (* 2 x))) are both valid and prove diferent clauses. The prover can choose the representation and the proof checker checks that is indeed a valid representation of the polynomial that is the sum or product of 1, . . . , . However, (poly+ (+ x y x) (+ x y x)) is not well-formed (a polynomial can only have one entry for the multiset {}).
The heart of our arithmetic proof is the axiom farkas that proves the unsatisfiability of the conjunction of several literals, whose weighted sum yields a contradiction. A variant of Farkas’ lemma states that a set of inequalities ≤ is unsatisfiable if and only if there is a vector = (1, . . . , ) with ≥ 0, = 0, and < 0. The axiom provides the coeficients 1, . . . , , e.g., (farkas 1 (<= x (* 2 y))) 2 (< y z) 1 (= (+ (* 2 z) 5) x)) is a valid instance proving {¬(<= x (* 2 y))), ¬(< y z), ¬(= (+ (* 2 z) 5) x))}, because the inequalities sum up to the contradiction 5 < 0 and x, y, z cancel out. It is allowed to use both integer and real literals in the same instance of the axiom farkas and in that case the weighted sum is computed after implicitly casting all integer polynomials to real.
We found that farkas, trichotomy, total, and total-int together with the core axioms for equality are complete for linear arithmetic in the sense that any valid disjunction of possibly negated equalities and inequalities of linear polynomials can be proved using just these axioms. The axiom farkas can prove clauses containing negated literals and the other three axioms can be used to rewrite negated literals into their positive form. The axiom total-int can be used to introduce arbitrary integer cuts, since 1 can be an arbitrary term.
If an input term is not already a polynomial, the rules poly* and poly+ together with the axiom cong can be used to rewrite it into a polynomial. To support arbitrary SMT-LIB input formulas, we need a few more axioms to rewrite other operators like >, >=, -, /, div, mod, etc. See the appendix for a complete list.
Our solver SMTInterpol produces proofs in the proof format presented in this paper. The reader is invited to experiment using our web interface for proof production and checking.3
The solver itself proves a benchmark in three phases. In the first phase, the input formula is simplified using equality rewriting and several solver-specific rewriting rules. The second phase converts the input formula into conjunctive normal form (CNF), creating an internal representation for every literal and adding auxiliary clauses. The third phase runs the DPLL( ) algorithm and generates theory lemmas, building the final resolution proof. 3See https://ultimate.informatik.uni-freiburg.de/smtinterpol/online/proof.html (farkas 1 (<=? 1 1′) . . . (<=? ′)) : {¬(<=? 1 1′), . . . , ¬(<=? ′)} where are positive integer constants, the weighted sum 1(1 − 1′) + · · · + ( − ′) is a non-negative constant. <=? stands for <, <=, or =, and if the weighted sum is zero, at least one of the literals must be <.
(trichotomy 1 2) : {(< 1 2), (= 1 2), (< 2 1)}
(total 1 2) : {(<= 1 2), (< 2 1)} (total-int 1 ) : {(<= 1 ), (<= + 1 1)} where 1 has type Int, is an integer constant in canonical form and + 1 the same integer constant increased by one in canonical form.
In the first phase, the input term is inductively rewritten into a simplified term ′. If proof production is enabled, the solver builds a proof for {(= ′)} at the same time it inductively computes ′. The proof mainly uses the cong axiom for the induction step and a set of solverspecific rewrite rules, such as (oracle +(= (ite t1 true t2) (or t1 t2)) :rewrite iteBool3). These rewrite rules can later be easily replaced by their proof.
In the second phase, the formula is split and converted to CNF. If the top-level formula is a conjunction of smaller components, the formula is split into the components and the proof for each component is tracked. The proofs are already generated in the final form, e.g., by resolving the input formula with the and- axiom that corresponds to the component. If the formula is a disjunction, the subproof is resolved with the or- axiom to split the formula into its literals. The literals may be further rewritten into their internal form, which is again explained by rewrite rules in form of oracles. These rewrite steps are integrated into the proof of the clause. Finally the clause is added to the DPLL( ) engine and the clause keeps a reference to its proof. To avoid exponential blow-up of the CNF transformation, a nested and term below a disjunction is treated as a Boolean variable. A named literal is created and new clauses are created using the Plaisted–Greenbaum algorithm. These new clauses are annotated with their proof, which is an instance of the and- or and+ axiom.
In the third phase, producing resolution proofs with the DPLL( ) algorithm is straightforward. Theory lemmas are added by theory-specific decision procedures. These lemmas are added as clauses to the DPLL( ) engine and are annotated with an oracle proof and explained later when the final proof is computed.
An earlier version of SMTInterpol used the rewrite rules and theory lemmas as its axioms and implemented a proof checker that checked these solver-specific rules. However, we found that writing a proof checker for custom rules leaves room for errors. Soundness errors in the proof checker are never caught, as testing is usually only done with correct proofs. While it is possible to write unit tests that specifically create invalid instances of proof rules, this is itself a tedious task with no reward and was never done.
Therefore, we created a proof translator that replaces each solver-specific oracle rule with a corresponding proof using only the axioms. This gives much more confidence, as a wrong rule cannot be explained by a valid proof. The proof translator from the solver-specific rules to the minimal rules is roughly the same size as the old proof checker. The new proof checker only has to handle the much simpler and smaller set of axioms and is less than a third the size of the old proof checker. More importantly, with the new proof format the trusted core does not have to be changed when new rewrite rules are added to the solver. Only the proof translator is afected, which is producing a certificate of correctness.
Our proof format optimizes simplicity of the proof checker over simplicity of the prover. Nonetheless, we think that the language is expressive enough to also allow for advanced proof techniques that exponentially decrease the proof size. In this section we investigate this in detail.
These techniques are made possible by the expressiveness of SMT-LIB, which we use for literals, and by having a complete set of axioms. Normally, resolution is only refutation-complete, i.e., if is valid, one can derive a contradiction from ¬. Our format can prove the unit clause {} from the axioms if is valid: The idea is to prove the clause {(! :x), ¬} from the axioms (del! :x) and (=-1 (! :x) p)). Using refutation completeness, a proof for {(! :x)} can be constructed, and then for {} using the axioms del! and =-2. Logging Proofs is a technique where provers output their proofs on the fly into a file. The main reason for doing this is to keep the memory overhead low. The proofs can be forgotten after writing them to the proof file. Our proof format supports this technique using the let-proof command. Instead of remembering the proof for every clause, one can directly write the line (let-proof (( prf )) into the proof file, where is a unique identifier for the clause and prf the proof for this clause. If was proved by resolution from other clauses, prf can use the identifiers of the other clauses and combine them with the rule res. Deleted clauses can be indicated by assigning a trivial clause, e.g., true+ to the previously used clause identifier.
To avoid repeating shared subterms, they can also be assigned to an identifier using let when they are first used. The prover just needs to give every subterm a unique identifier and subsequently use this identifier to refer to the subterm. To ensure that the parentheses match, the prover only needs to count the number of opening parentheses to add the same number of closing parentheses at the end.
Extended Resolution [
(C2 (and- 0 p1 p2)) (C3 (and- 1 p1 p2))) ...)) Quantifier Introduction is usually done by a rule all-intro that takes a subproof prf for a formula containing a free variable x and returns a proof for (forall ((x )) ). In our proof format, there is no such rule and also free variables are not allowed in proofs. Nonetheless it is possible to express this rule using resolution, let binders and the forall+ axiom.
(let ((x (choose (x ) (not )))) (res prf (forall+ ((x )) )))
Symmetry Breaking is a technique that can greatly reduce the search space by exploiting
symmetry [
This can be formally expressed in our proof format. First define ′1 := (ite (p 1) 1 2) and ′2 := (ite (p 1) 2 1). These definitions can be introduced using the let keyword. Then show that (1, 2) = (′1, ′2) holds by case distinction over (p 1) and exploiting the symmetry if (p 1) is false. Thus one can prove ′ from where ′ is the formula containing ′1 and ′2. Now one can show from (or (p 1) (p 2)) that (p ′1) holds, again by case distinction over (p 1). The remaining proof is now done on the renamed formula, using ′1 and ′2, ignoring their definition but treating them as uninterpreted constants.
The proof for = ′ is linear in the size of and for each of the two cases proceeds by induction over using ite1/ite2 for the leaves, and an instance of cong for every subterm. Commutativity of logical operators needs to be explicitly proved. The proof of (p ′1) is simple and requires ite1, ite2, congruence over p, and equivalence reasoning. An example proof using this technique is provided with the online proof checker on our website.
Böhme and Weber [
For SAT solvers a standardized proof format is DRAT [
CVC5 uses LFSC [
Alethe4 [
The proof format of OpenSMT [
Quip5 is an experimental proof format for first-order and higher-order logic. It aims at proofs that are easy to produce by providing high-level proof rules and redundant rules (e.g. resolution and unit resolution). In return, the proof checker needs to perform more complex reasoning, e.g. congruence closure and other theory-specific reasoning. The format is resolution-based and also uses clauses with SMT-LIB formulas, but it also supports hyperresolution steps. Shared terms are abbreviated by the top-level command deft, which corresponds to let in our format.
The Z3 proof format [
We presented a simple proof format for SMT based on the resolution rule. Its main feature is its restriction to only a few basic axioms. In total we currently define one rule (resolution) and 60 axioms for the core theory, arithmetic, arrays, and datatypes, which is on average two axioms per theory-defined function. By implementing this proof format in our SMT solver, we have shown that despite its simplicity, the format can succinctly express the reasoning steps done by our solver. We have also shown that the format can handle more advanced reasoning techniques like symmetry breaking.
Every single proof format may favour some solvers while making it more dificult for other solvers to express their proofs. Our format is based on the resolution rule, which favours solvers based on DPLL( ). Moreover, the axioms for linear arithmetic, especially the axiom farkas, are inspired by the theory lemmas that our solver produces. However, other proof formats like CVC5’s LFSC, Alethe, and Quip are also based on resolution and Alethe has a rule la_generic that is almost identical to farkas. In fact, most of our axioms are also contained in Alethe in the same or a similar form. Our experience with SMTInterpol gives us confidence that proofs from SMT solvers can be translated into this format with moderate overhead.
In our format, rules with assumptions are expressed as axioms, e.g., modus ponens is expressed as =>- where the premises are negated literals and the conclusion a positive literal. The axiom form is more flexible, e.g., introduction rules can also be used to eliminate negated operators. Also the axioms are needed in this form to explain the Tseitin encoding.
The main reason we do not use the SMT-LIB operators or/not to represent clauses or negated literals is to make a clean separation between the meta-language (resolution proofs) and the language in which the formulas are written. This avoids ambiguity, whether a term (or 1 2) represents a Tseitin literal or a clause. It also avoids problems with double negation; other proof formats interpret terms starting with not as negated literal but double negated literals are seen as positive. Note that the only place we use a concrete syntax for clauses is the oracle rule.
Implicitly expanding let terms seems to go against the goal of a low-level proof format, but this is essential. First, a way of defining names for repeatedly used terms or clauses is needed to avoid exponential blow-up. Second, our solver and proof checker represent formulas and proofs internally using directed acyclic graphs (DAGs). In a way, let is just a concrete syntax to represent DAGs in textual form. Finally, let is the SMT-LIB syntax for substituting variables with terms, which is used in the quantifier elimination and introduction axioms and the expand axiom for function definitions. Thus, we also use it to avoid inventing a new syntax for substitutions.
This work is supported by the German Research Council (DFG) under HO 5606/1-2.
Axioms for the logical operators:
true+ : {true} false- : {¬false} (not+ 0) : {(not 0), 0} (not- 0) : {¬(not 0), ¬0} (and+ 0 . . . ) : {(and 0 . . . ), ¬0, . . . , ¬} (and- 0 . . . ) : {¬(and 0 . . . ), } (or+ 0 . . . ) : {(or 0 . . . ), ¬} (=>+ 0 . . . ) : {(=> 0 . . . ), (¬) } (=>- 0 . . . ) : {¬(=> 0 . . . ), ¬0, . . . , } (=+1 0 1) : {(= 0 1), 0, 1} (=-1 0 1) : {¬(= 0 1), 0, ¬1} (=+2 0 1) : {(= 0 1), ¬0, ¬1} (=-2 0 1) : {¬(= 0 1), ¬0, 1} (xor+ (1) (2) (3)) : {(xor 1), (xor 2), ¬(xor 3)} (xor- (1) (2) (3)) : {¬(xor 1), ¬(xor 2), ¬(xor 3)} where 1,2,3 are lists of terms with each term occurring an even number in total and if is only one term, (xor ) stands for the term .
Axioms for quantifiers: (forall+ ((1 1) . . . ( )) ) : {(forall ((1 1) . . . ( )) ), ¬(let ((1 (choose (1 1) (forall ((2 2) . . . ( )) (not ))))) (let ((2 (choose (2 2) (forall ((3 3) . . . ( )) (not ))))) . . .
(let (( (choose ( ) (not )))) )· · · ))} (forall- ((1 1) . . . ( )) ) :
{¬(forall ((1 1) . . . ( )) ), (let ((1 1). . .( )) )} (exists+ ((1 1) . . . ( )) ) :
{(exists ((1 1) . . . ( )) ), ¬(let ((1 1). . .( )) )} (exists- ((1 1) . . . ( )) ) : {¬(exists ((1 1) . . . ( )) ), (let ((1 (choose (1 1) (exists ((2 2) . . . ( )) )))) (let ((2 (choose (2 2) (exists ((3 3) . . . ( )) )))) . . . (let (( (choose ( ) ))) )· · · ))} In the axioms forall- and exists+ the sorts are automatically determined from the type of the expressions .
Axioms for equality:
(refl ) : {(= )} (symm 0 1) : {(= 0 1), ¬(= 1 0)} (trans 0 . . . ) : {(= 0 ), ¬(= 0 1), . . . , ¬(= − 1 )} (cong (f 0 . . . ) (f ′0 . . . ′)):
{(= (f 0 . . . ) (f ′0 . . . ′)), ¬(= 0 ′0), . . . , ¬(= ′)} (=+ 0 . . . ) : {(= 0 . . . ), ¬(= 0 1), . . . , ¬(= − 1 )} (=- 0 . . . ) : {¬(= 0 . . . ), (= )} where ̸= (distinct+ 0 . . . ) : {(distinct 0 . . . ), (= 0 1), . . . , (= 0 ), . . . , (= − 1 )} (distinct- 0 . . . ) : {¬(distinct 0 . . . ), ¬(= )} where ̸=
(ite1 0 1 2) : {(= (ite 0 1 2) 1), ¬0} (ite2 0 1 2) : {(= (ite 0 1 2) 2), 0}
(del! . . .) : {(= (! . . .) )} (expand (f 0 . . . )) : {(= (f 0 . . . ) (let ((0 0). . .( )) ))} where f is defined by (define-fun f ((0 0)...( )) )
(xor+ (1 2 3) (2) (1 3)) :{(xor 1 2 3), 2, ¬(xor 1 3)} (xor- ( ) ( ) ( )) :{¬(xor )} B. Axioms of Linear Arithmetic (poly+ (+ 1 . . . ) ) : {(= (+ 1 . . . ) )} (poly* (* 1 . . . ) ) : {(= (* 1 . . . ) )} where = 1 + · · · + where = 1 · · · (farkas 1 (<=? 1 1′) . . . (<=? ′)) : {¬(<=? 1 1′), . . . , ¬(<=? ′)} where are positive integer constants, the weighted sum 1(1 − 1′) + · · · + ( − ′) is a non-negative constant. <=? stands for <, <=, or =, and if the weighted sum is zero, at least one of the literals must be <.
(trichotomy 1 2) : {(< 1 2), (= 1 2), (< 2 1)}
(total 1 2) : {(<= 1 2), (< 2 1)} (total-int 1 ) : {(<= 1 ), (<= + 1 1)} where 1 has type Int, is an integer constant in canonical form and + 1 the same integer constant increased by one in canonical form. (to_real ) : {(= (to_real ) ′)}
where ′ is the result of casting the integer polynomial to real.
(>def 1 2) : {(= (> 1 2) (< 2 1))} (>=def 1 2) : {(= (>= 1 2) (<= 2 1))} (/def 1 2 . . . ) : {(= 1 (* 2 . . . (/ 1 2 . . . ))), (= 2 0), . . . , (= 0)} (-def 1) : {(= (- 1) (* (- 1) 1))} (-def 1 2 . . . ) : {(= (- 1 2 . . . ) (+ 1 (* (- 1) 2)) . . . (* (- 1) ))} (to_int-low 1) : {(<= (to_real (to_int 1)) 1)} (to_int-high 1) : {(< 1 (+ (to_real (to_int 1)) 1.0))}
(abs-def 1) : {(= (abs 1) (ite (< 1 0) (- 1) 1))} (div-low 1 2) : {(<= (* 2 (div 1 2)) 1), (= 2 0)} (div-high 1 2) : {(< 1 (+ (* 2 (div 1 2)) (abs 2))), (= 2 0)} (mod-def 1 2) : {(= (mod 1 2) (- 1 (* 2 (div 1 2)))), (= 2 0)} (divisible-def c 1) : {(= ((_ divisible c) 1) (= 1 (* c (div 1 c))))}
We support an extension of the array theory with @diff for returning the elements where two arrays difer and @const for the array that stores the same element for all indices. In these axioms stands for a term of array type, for a term of index type and for a term of element type.
(selectstore1 ) :{(= (select (store ) ) )} (selectstore2 1 2 ) :{(= (select (store 1 ) 2) (select 2)), (= 1 2)} (extdiff 0 1) :{(= 0 1), ¬(= (select 0 (@diff 0 1))
(select 1 (@diff 0 1)))} (const ) :{(= (select (@const ) ) )}
In the following axioms, 1 . . . , are the constructors 1, . . . are the selectors of . (dt_project 1 . . . ) :{(= ( ( 1 . . . )) )}
(dt_cons ) :{¬((_ is ) ), (= ( (1 ). . . ( )) )} (dt_test+ ( 1 . . . )) :{((_ is ) ( 1 . . . ))} (dt_test- ( 1 . . . )) :{¬((_ is ) ( 1 . . . ))} where ̸= (dt_exhaust ) :{((_ is 1) ), . . . , ((_ is ) )} (dt_match (match . . . )) :{(= (match t (( 1 . . . ) ) . . . ) (ite ((_ is ) t) (let ((1 (1 )). . . ( ( ))) ) . . . )}