Proof rules

enum
class
cvc5
::
internal
::
PfRule
:
uint32_t

An enumeration for proof rules. This enumeration is analogous to Kind for Node objects.
All proof rules are given as inference rules, presented in the following form:
\[\texttt{RULENAME}: \inferruleSC{\varphi_1 \dots \varphi_n \mid t_1 \dots t_m}{\psi}{if $C$}\]where we call \(\varphi_i\) its premises or children, \(t_i\) its arguments, \(\psi\) its conclusion, and \(C\) its side condition. Alternatively, we can write the application of a proof rule as
(RULENAME F1 ... Fn :args t1 ... tm)
, omitting the conclusion (since it can be uniquely determined from premises and arguments). Note that premises are sometimes given as proofs, i.e., application of proof rules, instead of formulas. This abuses the notation to see proof rule applications and their conclusions interchangeably.Conceptually, the following proof rules form a calculus whose target user is the Nodelevel theory solvers. This means that the rules below are designed to reason about, among other things, common operations on Node objects like Rewriter::rewrite or Node::substitute. It is intended to be translated or printed in other formats.
The following PfRule values include core rules and those categorized by theory, including the theory of equality.
The “core rules” include two distinguished rules which have special status: (1)
ASSUME
, which represents an open leaf in a proof; and (2)SCOPE
, which encloses a scope (a subproof) with a set of scoped assumptions. The core rules additionally correspond to generic operations that are done internally on nodes, e.g. calling Rewriter::rewrite.Rules with prefix
MACRO_
are those that can be defined in terms of other rules. These exist for convenience and can be replaced by their definition in postprocessing.Values:

enumerator
ASSUME

Assumption (a leaf)
\[\inferrule{ \mid F}{F}\]This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified. An assume leaf is analogous to a free variable in a term, where we say “F is a free assumption in proof P” if it contains an application of F that is not bound by
SCOPE
(see below).

enumerator
SCOPE

Scope (a binder for assumptions)
\[\inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$}\]This rule has a dual purpose with
ASSUME
. It is a way to close assumptions in a proof. We require that \(F_1 \dots F_n\) are free assumptions in P and say that \(F_1 \dots F_n\) are not free in(SCOPE P)
. In other words, they are bound by this application. For example, the proof node:(SCOPE (ASSUME F) :args F)
has the conclusion \(F \Rightarrow F\) and has no free assumptions. More generally, a proof with no free assumptions always concludes a valid formula.

enumerator
SUBS

Builtin theory – Substitution
\[\inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)}\]where \(\sigma_{ids}(F_i)\) are substitutions, which notice are applied in reverse order. Notice that \(ids\) is a MethodId identifier, which determines how to convert the formulas \(F_1 \dots F_n\) into substitutions. It is an optional argument, where by default the premises are equalities of the form (= x y) and converted into substitutions \(x\mapsto y\) .

enumerator
REWRITE

Builtin theory – Rewrite
\[\inferrule{ \mid t, idr}{t = \texttt{Rewriter}_{idr}(t)}\]where \(idr\) is a MethodId identifier, which determines the kind of rewriter to apply, e.g. Rewriter::rewrite.

enumerator
EVALUATE

Builtin theory – Evaluate
\[\inferrule{ \mid t}{t = \texttt{Evaluator::evaluate}(t)}\]Note this is equivalent to:
(REWRITE t MethodId::RW_EVALUATE)
.

enumerator
MACRO_SR_EQ_INTRO

Builtin theory – Substitution + Rewriting equality introduction
In this rule, we provide a term \(t\) and conclude that it is equal to its rewritten form under a (proven) substitution.
\[\inferrule{F_1 \dots F_n \mid t, (ids (ida (idr)?)?)?}{t = \texttt{Rewriter}_{idr}(t \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]In other words, from the point of view of Skolem forms, this rule transforms \(t\) to \(t'\) by standard substitution + rewriting.
The arguments \(ids\) , \(ida\) and \(idr\) are optional and specify the identifier of the substitution, the substitution application and rewriter respectively to be used. For details, see theory/builtin/proof_checker.h .

enumerator
MACRO_SR_PRED_INTRO

Builtin theory – Substitution + Rewriting predicate introduction
In this rule, we provide a formula \(F\) and conclude it, under the condition that it rewrites to true under a proven substitution.
\[\inferrule{F_1 \dots F_n \mid F, (ids (ida (idr)?)?)?}{F}\]where \(\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \top\) and \(ids\) and \(idr\) are method identifiers.
More generally, this rule also holds when \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \top\) where \(F'\) is the result of the left hand side of the equality above. Here, notice that we apply rewriting on the original form of \(F'\) , meaning that this rule may conclude an \(F\) whose Skolem form is justified by the definition of its (fresh) Skolem variables. For example, this rule may justify the conclusion \(k = t\) where \(k\) is the purification Skolem for \(t\) , e.g. where the original form of \(k\) is \(t\) .
Furthermore, notice that the rewriting and substitution is applied only within the side condition, meaning the rewritten form of the original form of \(F\) does not escape this rule.

enumerator
MACRO_SR_PRED_ELIM

Builtin theory – Substitution + Rewriting predicate elimination
\[\inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]where \(ids\) and \(idr\) are method identifiers.
We rewrite only on the Skolem form of \(F\) , similar to
MACRO_SR_EQ_INTRO
.

enumerator
MACRO_SR_PRED_TRANSFORM

Builtin theory – Substitution + Rewriting predicate elimination
\[\inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G}\]where \(\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \texttt{Rewriter}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))\) .
More generally, this rule also holds when: \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))\) where \(F'\) and \(G'\) are the result of each side of the equation above. Here, original forms are used in a similar manner to
MACRO_SR_PRED_INTRO
above.

enumerator
ENCODE_PRED_TRANSFORM

Builtin theory – Encode predicate transformation .. math:
\inferrule{F \mid G}{G}
where \(F\) and \(G\) are equivalent up to their encoding in an external proof format. This is currently verified by
:math: ` texttt{RewriteDbNodeConverter::convert}(F) =
texttt{RewriteDbNodeConverter::convert}(G)`. This rule can be treated as a noop when appropriate in external proof formats.

enumerator
DSL_REWRITE

Builtin theory – DSL rewrite .. math:
\inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F}
where the DSL rewrite rule with the given identifier is \(\forall x_1 \dots x_n. (G_1 \wedge G_n) \Rightarrow G\) where for \(i=1, \dots n\) , we have that \(F_i = \sigma(G_i)\) and \(F = \sigma(G)\) where \(\sigma\) is the substitution \(\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}\) .
Notice that the application of the substitution takes into account the possible list semantics of variables \(x_1 \ldots x_n\) . If \(x_i\) is a variable with list semantics, then \(t_i\) denotes a list of terms. The substitution (see expr::narySubstitute) replaces each \(x_i\) with the list \(t_i\) in its place.

enumerator
ANNOTATION

Builtin theory – Annotation
\[\inferrule{F \mid a_1 \dots a_n}{F}\]The terms \(a_1 \dots a_n\) can be anything used to annotate the proof node, one example is where \(a_1\) is a theory::InferenceId.

enumerator
REMOVE_TERM_FORMULA_AXIOM

Processing rules – Remove Term Formulas Axiom
\[\inferrule{ \mid t}{\texttt{RemoveTermFormulas::getAxiomFor}(t)}\]

enumerator
THEORY_LEMMA

Trusted rules – Theory lemma
\[\inferrule{ \mid F, tid}{F}\]where \(F\) is a (Tvalid) theory lemma generated by theory with TheoryId \(tid\) . This is a “coarsegrained” rule that is used as a placeholder if a theory did not provide a proof for a lemma or conflict.

enumerator
THEORY_REWRITE

Trusted rules – Theory rewrite
\[\inferrule{ \mid F, tid, rid}{F}\]where \(F\) is an equality of the form \(t = t'\) where \(t'\) is obtained by applying the kind of rewriting given by the method identifier \(rid\) , which is one of:
RW_REWRITE_THEORY_PRE
,RW_REWRITE_THEORY_POST
,RW_REWRITE_EQ_EXT
. Notice that the checker for this rule does not replay the rewrite to ensure correctness, since theory rewriter methods are not static. For example, the quantifiers rewriter involves constructing new bound variables that are not guaranteed to be consistent on each call.

enumerator
THEORY_PREPROCESS

Trusted rules – Theory preprocessing
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality of the form \(t = \texttt{Theory::ppRewrite}(t)\) for some theory.

enumerator
THEORY_PREPROCESS_LEMMA

Trusted rules – Theory preprocessing
\[\inferrule{ \mid F}{F}\]where \(F\) was added as a new assertion by theory preprocessing from the theory with identifier tid.

enumerator
PREPROCESS

Trusted rules – Preprocessing
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality of the form \(t = t'\) where \(t\) was replaced by \(t'\) based on some preprocessing pass, or otherwise \(F\) was added as a new assertion by some preprocessing pass.

enumerator
PREPROCESS_LEMMA

Trusted rules – Preprocessing new assertion
\[\inferrule{ \mid F}{F}\]where \(F\) was added as a new assertion by some preprocessing pass.

enumerator
THEORY_EXPAND_DEF

Trusted rules – Theory expand definitions
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality of the form \(t = t'\) where \(t\) was replaced by \(t'\) based on theory expand definitions.

enumerator
WITNESS_AXIOM

Trusted rules – Witness term axiom
\[\inferrule{ \mid F}{F}\]where \(F\) is an existential
(exists ((x T)) (P x))
used for introducing a witness term(witness ((x T)) (P x))
.

enumerator
TRUST_REWRITE

Trusted rules – Nonreplayable rewriting
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality t = t’ that holds by a form of rewriting that could not be replayed during proof postprocessing.

enumerator
TRUST_FLATTENING_REWRITE

** Trusted rules – Nonsupported flattening rewrite **
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality t = t’ where both t and t’ are applications of associative operators but the rewriter does not support flattening them to the same normal form.

enumerator
TRUST_SUBS

Trusted rules – Nonreplayable substitution
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality \(t = t'\) that holds by a form of substitution that could not be replayed during proof postprocessing.

enumerator
TRUST_SUBS_MAP

Trusted rules – Nonreplayable substitution map
\[\inferrule{ \mid F}{F}\]where \(F\) is an equality \(t = t'\) that holds by a form of substitution that could not be determined by the TrustSubstitutionMap. This inference may contain possibly multiple children corresponding to the formulas used to derive the substitution.

enumerator
TRUST_SUBS_EQ

Trusted rules – Solved equality
\[\inferrule{F' \mid F}{F}\]where \(F\) is a solved equality of the form \(x = t\) derived as the solved form of \(F'\) .

enumerator
THEORY_INFERENCE

Theoryspecific inference
\[\inferrule{ \mid F}{F}\]where \(F\) is a fact derived by a theoryspecific inference.

enumerator
SAT_REFUTATION

SAT Refutation for assumptionbased unsat cores
\[\inferrule{F_1 \dots F_n \mid }{\bot}\]where \(F_1 \dots F_n\) correspond to the unsat core determined by the SAT solver.

enumerator
RESOLUTION

Boolean – Resolution
\[\inferrule{C_1, C_2 \mid pol, L}{C}\]where

\(C_1\) and \(C_2\) are nodes viewed as clauses, i.e., either an
OR
node with each children viewed as a literal or a node viewed as a literal. Note that anOR
node could also be a literal. 
\(pol\) is either true or false, representing the polarity of the pivot on the first clause

\(L\) is the pivot of the resolution, which occurs as is (resp. under a
NOT
) in \(C_1\) and negatively (as is) in \(C_2\) if \(pol = \top\) ( \(pol = \bot\) ).
\(C\) is a clause resulting from collecting all the literals in \(C_1\) , minus the first occurrence of the pivot or its negation, and \(C_2\) , minus the first occurrence of the pivot or its negation, according to the policy above. If the resulting clause has a single literal, that literal itself is the result; if it has no literals, then the result is false; otherwise it’s an
OR
node of the resulting literals.Note that it may be the case that the pivot does not occur in the clauses. In this case the rule is not unsound, but it does not correspond to resolution but rather to a weakening of the clause that did not have a literal eliminated.


enumerator
CHAIN_RESOLUTION

Boolean – Nary Resolution
\[\inferrule{C_1 \dots C_n \mid pol_1,L_1 \dots pol_{n1},L_{n1}}{C}\]where

let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined above

let \(C_1 \diamond_{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\) , as defined above

let \(C_1' = C_1\) ,

for each \(i > 1\) , let \(C_i' = C_{i1} \diamond{L_{i1}, \mathit{pol}_{i1}} C_i'\)
The result of the chain resolution is \(C = C_n'\)


enumerator
FACTORING

Boolean – Factoring
\[\inferrule{C_1 \mid }{C_2}\]where the set representations of \(C_1\) and \(C_2\) are the same and the number of literals in \(C_2\) is smaller than that of \(C_1\) .

enumerator
REORDERING

Boolean – Reordering
\[\inferrule{C_1 \mid C_2}{C_2}\]where the set representations of \(C_1\) and \(C_2\) are the same and the number of literals in \(C_2\) is the same of that of \(C_1\) .

enumerator
MACRO_RESOLUTION

Boolean – Nary Resolution + Factoring + Reordering
\[\inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n1},L_{n1}}{C}\]where

let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined in
RESOLUTION

let \(C_1 \diamond{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\) , as defined in
RESOLUTION

let \(C_1'\) be equal, in its set representation, to \(C_1\) ,

for each \(i > 1\) , let \(C_i'\) be equal, it its set representation, to \(C_{i1} \diamond{L_{i1},\mathit{pol}_{i1}} C_i'\)
The result of the chain resolution is \(C\) , which is equal, in its set representation, to \(C_n'\)


enumerator
MACRO_RESOLUTION_TRUST

Boolean – Nary Resolution + Factoring + Reordering unchecked
Same as
MACRO_RESOLUTION
, but not checked by the internal proof checker.

enumerator
SPLIT

Boolean – Split
\[\inferrule{ \mid F}{F \lor \neg F}\]

enumerator
EQ_RESOLVE

Boolean – Equality resolution
\[\inferrule{F_1, (F_1 = F_2) \mid }{F_2}\]Note this can optionally be seen as a macro for
EQUIV_ELIM1
+RESOLUTION
.

enumerator
MODUS_PONENS

Boolean – Modus Ponens
\[\inferrule{F_1, (F_1 \rightarrow F_2) \mid }{F_2}\]Note this can optionally be seen as a macro for
IMPLIES_ELIM
+RESOLUTION
.

enumerator
NOT_NOT_ELIM

Boolean – Double negation elimination
\[\inferrule{\neg (\neg F) \mid }{F}\]

enumerator
CONTRA

Boolean – Contradiction
\[\inferrule{F, \neg F \mid }{\bot}\]

enumerator
AND_ELIM

Boolean – And elimination
\[\inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i}\]

enumerator
AND_INTRO

Boolean – And introduction
\[\inferrule{F_1 \dots F_n \mid }{(F_1 \land \dots \land F_n)}\]

enumerator
NOT_OR_ELIM

Boolean – Not Or elimination
\[\inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i}\]

enumerator
IMPLIES_ELIM

Boolean – Implication elimination
\[\inferrule{F_1 \rightarrow F_2 \mid }{\neg F_1 \lor F_2}\]

enumerator
NOT_IMPLIES_ELIM1

Boolean – Not Implication elimination version 1
\[\inferrule{\neg(F_1 \rightarrow F_2) \mid }{F_1}\]

enumerator
NOT_IMPLIES_ELIM2

Boolean – Not Implication elimination version 2
\[\inferrule{\neg(F_1 \rightarrow F_2) \mid }{\neg F_2}\]

enumerator
EQUIV_ELIM1

Boolean – Equivalence elimination version 1
\[\inferrule{F_1 = F_2 \mid }{\neg F_1 \lor F_2}\]

enumerator
EQUIV_ELIM2

Boolean – Equivalence elimination version 2
\[\inferrule{F_1 = F_2 \mid }{F_1 \lor \neg F_2}\]

enumerator
NOT_EQUIV_ELIM1

Boolean – Not Equivalence elimination version 1
\[\inferrule{F_1 \neq F_2 \mid }{F_1 \lor F_2}\]

enumerator
NOT_EQUIV_ELIM2

Boolean – Not Equivalence elimination version 2
\[\inferrule{F_1 \neq F_2 \mid }{\neg F_1 \lor \neg F_2}\]

enumerator
XOR_ELIM1

Boolean – XOR elimination version 1
\[\inferrule{F_1 \xor F_2 \mid }{F_1 \lor F_2}\]

enumerator
XOR_ELIM2

Boolean – XOR elimination version 2
\[\inferrule{F_1 \xor F_2 \mid }{\neg F_1 \lor \neg F_2}\]

enumerator
NOT_XOR_ELIM1

Boolean – Not XOR elimination version 1
\[\inferrule{\neg(F_1 \xor F_2) \mid }{F_1 \lor \neg F_2}\]

enumerator
NOT_XOR_ELIM2

Boolean – Not XOR elimination version 2
\[\inferrule{\neg(F_1 \xor F_2) \mid }{\neg F_1 \lor F_2}\]

enumerator
ITE_ELIM1

Boolean – ITE elimination version 1
\[\inferrule{(\ite{C}{F_1}{F_2}) \mid }{\neg C \lor F_1}\]

enumerator
ITE_ELIM2

Boolean – ITE elimination version 2
\[\inferrule{(\ite{C}{F_1}{F_2}) \mid }{C \lor F_2}\]

enumerator
NOT_ITE_ELIM1

Boolean – Not ITE elimination version 1
\[\inferrule{\neg(\ite{C}{F_1}{F_2}) \mid }{\neg C \lor \neg F_1}\]

enumerator
NOT_ITE_ELIM2

Boolean – Not ITE elimination version 2
\[\inferrule{\neg(\ite{C}{F_1}{F_2}) \mid }{C \lor \neg F_2}\]

enumerator
NOT_AND

Boolean – De Morgan – Not And
\[\inferrule{\neg(F_1 \land \dots \land F_n) \mid }{\neg F_1 \lor \dots \lor \neg F_n}\]

enumerator
CNF_AND_POS

Boolean – CNF – And Positive
\[\inferrule{ \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i}\]

enumerator
CNF_AND_NEG

Boolean – CNF – And Negative
\[\inferrule{ \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n}\]

enumerator
CNF_OR_POS

Boolean – CNF – Or Positive
\[\inferrule{ \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n}\]

enumerator
CNF_OR_NEG

Boolean – CNF – Or Negative
\[\inferrule{ \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i}\]

enumerator
CNF_IMPLIES_POS

Boolean – CNF – Implies Positive
\[\inferrule{ \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2}\]

enumerator
CNF_IMPLIES_NEG1

Boolean – CNF – Implies Negative 1
\[\inferrule{ \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1}\]

enumerator
CNF_IMPLIES_NEG2

Boolean – CNF – Implies Negative 2
\[\inferrule{ \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2}\]

enumerator
CNF_EQUIV_POS1

Boolean – CNF – Equiv Positive 1
\[\inferrule{ \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2}\]

enumerator
CNF_EQUIV_POS2

Boolean – CNF – Equiv Positive 2
\[\inferrule{ \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2}\]

enumerator
CNF_EQUIV_NEG1

Boolean – CNF – Equiv Negative 1
\[\inferrule{ \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2}\]

enumerator
CNF_EQUIV_NEG2

Boolean – CNF – Equiv Negative 2
\[\inferrule{ \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2}\]

enumerator
CNF_XOR_POS1

Boolean – CNF – XOR Positive 1
\[\inferrule{ \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2}\]

enumerator
CNF_XOR_POS2

Boolean – CNF – XOR Positive 2
\[\inferrule{ \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_2}\]

enumerator
CNF_XOR_NEG1

Boolean – CNF – XOR Negative 1
\[\inferrule{ \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2}\]

enumerator
CNF_XOR_NEG2

Boolean – CNF – XOR Negative 2
\[\inferrule{ \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2}\]

enumerator
CNF_ITE_POS1

Boolean – CNF – ITE Positive 1
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1}\]

enumerator
CNF_ITE_POS2

Boolean – CNF – ITE Positive 2
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2}\]

enumerator
CNF_ITE_POS3

Boolean – CNF – ITE Positive 3
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2}\]

enumerator
CNF_ITE_NEG1

Boolean – CNF – ITE Negative 1
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \not F_1}\]

enumerator
CNF_ITE_NEG2

Boolean – CNF – ITE Negative 2
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2}\]

enumerator
CNF_ITE_NEG3

Boolean – CNF – ITE Negative 3
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2}\]

enumerator
REFL

Equality – Reflexivity
\[\inferrule{\mid t}{t = t)}\]

enumerator
SYMM

Equality – Symmetry
\[\inferrule{t_1 = t_2\mid }{t_2 = t_1}\]or
\[\inferrule{t_1 \neq t_2\mid }{t_2 \neq t_1}\]

enumerator
TRANS

Equality – Transitivity
\[\inferrule{t_1=t_2,\dots,t_{n1}=t_n\mid }{t_1 = t_n}\]

enumerator
CONG

Equality – Congruence
\[\inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?)(t_1,\dots, t_n) = k(f?)(s_1,\dots, s_n)}\]where \(k\) is the application kind. Notice that \(f\) must be provided iff \(k\) is a parameterized kind, e.g.
APPLY_UF
. The actual node for \(k\) is constructible viaProofRuleChecker::mkKindNode
.

enumerator
TRUE_INTRO

Equality – True intro
\[\inferrule{F\mid }{F = \top}\]

enumerator
TRUE_ELIM

Equality – True elim
\[\inferrule{F=\top\mid }{F}\]

enumerator
FALSE_INTRO

Equality – False intro
\[\inferrule{\neg F\mid }{F = \bot}\]

enumerator
FALSE_ELIM

Equality – False elim
\[\inferrule{F=\bot\mid }{\neg F}\]

enumerator
HO_APP_ENCODE

Equality – Higherorder application encoding
\[\inferrule{\mid t}{t= \texttt{TheoryUfRewriter::getHoApplyForApplyUf}(t)}\]For example, this rule concludes \(f(x,y) = @(@(f,x),y)\) , where \(@\) isthe
HO_APPLY
kind.

enumerator
HO_CONG

Equality – Higherorder congruence
\[\inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid }{f(t_1,\dots, t_n) = g(s_1,\dots, s_n)}\]Notice that this rule is only used when the application kinds are
APPLY_UF
.

enumerator
BETA_REDUCE

Equality – Beta reduction
\[\inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n} {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}}\]The right hand side of the equality in the conclusion is computed using standard substitution (Node::substitute).

enumerator
ARRAYS_READ_OVER_WRITE

Arrays – Read over write
\[\inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)}\]

enumerator
ARRAYS_READ_OVER_WRITE_CONTRA

Arrays – Read over write, contrapositive
\[\inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid }{i_1=i_2}\]

enumerator
ARRAYS_READ_OVER_WRITE_1

Arrays – Read over write 1
\[\inferrule{\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e}\]

enumerator
ARRAYS_EXT

Arrays – Arrays extensionality
\[\inferrule{a \neq b\mid } {\mathit{select}(a,k)\neq\mathit{select}(b,k)}\]where \(k\) is \(\texttt{arrays::SkolemCache::getExtIndexSkolem}(a\neq b)\) .

enumerator
ARRAYS_EQ_RANGE_EXPAND

Arrays – Expansion of array range equality
\[\inferrule{\mid \mathit{eqrange}(a,b,i,j)} {\mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x)}\]

enumerator
BV_BITBLAST

Bitvectors – Bitblast
\[\inferrule{\mid t}{t = \texttt{bitblast}(t)}\]where
bitblast()
represents the result of the bitblasted term as a bitvector consisting of the output bits of the bitblasted circuit representation of the term. Terms are bitblasted according to the strategies defined intheory/bv/bitblast/bitblast_strategies_template.h
.

enumerator
BV_BITBLAST_STEP

Bitvectors – Bitblast bitvector constant, variable, and terms
For constant and variables:
\[\inferrule{\mid t}{t = \texttt{bitblast}(t)}\]For terms:
\[\inferrule{\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)}\]where \(t\) is \(k(t_1,\dots,t_n)\) .

enumerator
BV_EAGER_ATOM

Bitvectors – Bitvector eager atom
\[\inferrule{\mid F}{F = F[0]}\]where \(F\) is of kind
BITVECTOR_EAGER_ATOM
.

enumerator
DT_UNIF

Datatypes – Unification
\[\inferrule{C(t_1,\dots,t_n)= C(s_1,\dots,s_n)\mid i}{t_1 = s_i}\]where \(C\) is a constructor.

enumerator
DT_INST

Datatypes – Instantiation
\[\inferrule{\mid t,n}{\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))}\]where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of t, and \(\mathit{is}_C\) is the discriminator (tester) for \(C\) .

enumerator
DT_COLLAPSE

Datatypes – Collapse
\[\inferrule{\mid \mathit{sel}_i(C_j(t_1,\dots,t_n))}{ \mathit{sel}_i(C_j(t_1,\dots,t_n)) = r}\]where \(C_j\) is a constructor, \(r\) is \(t_i\) if \(\mathit{sel}_i\) is a correctly applied selector, or
TypeNode::mkGroundTerm()
of the proper type otherwise. Notice that the use ofmkGroundTerm
differs from the rewriter which usesmkGroundValue
in this case.

enumerator
DT_SPLIT

Datatypes – Split
\[\inferrule{\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)}\]where \(C_1,\dots,C_n\) are all the constructors of the type of \(t\) .

enumerator
DT_CLASH

Datatypes – Clash
\[\inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid }{\bot} {if $i\neq j$}\]

enumerator
SKOLEM_INTRO

Quantifiers – Skolem introduction
\[\inferrule{\mid k}{k = t}\]where \(t\) is the unpurified form of skolem \(k\) .

enumerator
SKOLEMIZE

Quantifiers – Skolemization
\[\inferrule{\exists x_1\dots x_n.\> F\mid }{F\sigma}\]or
\[\inferrule{\neg (\forall x_1\dots x_n.\> F)\mid }{\neg F\sigma}\]where \(\sigma\) maps \(x_1,\dots,x_n\) to their representative skolems obtained by
SkolemManager::mkSkolemize
, returned in the skolems argument of that method. The witness terms for the returned skolems can be obtained bySkolemManager::getWitnessForm
.

enumerator
INSTANTIATE

Quantifiers – Instantiation
\[\inferrule{\forall x_1\dots x_n.\> F\mid t_1,\dots,t_n, (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}}\]The optional argument \(id\) indicates the inference id that caused the instantiation. The term \(t\) indicates an additional term (e.g. the trigger) associated with the instantiation, which depends on the id. If the id has prefix
QUANTIFIERS_INST_E_MATCHING
, then \(t\) is the trigger that generated the instantiation.

enumerator
ALPHA_EQUIV

Quantifiers – Alpha equivalence
\[\inferruleSC{\mid F, y_1=z_1,\dots, y_n=z_n} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables}\]Notice that this rule is correct only when \(z_1,\dots,z_n\) are not contained in \(FV(F) \setminus \{ y_1,\dots, y_n \}\) , where \(FV(\varphi)\) are the free variables of \(\varphi\) . The internal quantifiers proof checker does not currently check that this is the case.

enumerator
QUANTIFIERS_PREPROCESS

Quantifiers – (Trusted) quantifiers preprocessing
\[\inferrule{?\mid F}{F}\]where \(F\) is an equality of the form \(t = \texttt{QuantifiersPreprocess::preprocess(t)}\) .

enumerator
CONCAT_EQ

Strings – Core rules – Concatenation equality
\[\inferrule{(t_1\cdot\ldots \cdot t_n \cdot t) = (t_1 \cdot\ldots \cdot t_n\cdot s)\mid b}{t = s}\]where \(\cdot\) stands for string concatenation and \(b\) indicates if the direction is reversed.
Notice that \(t\) or \(s\) may be empty, in which case they are implicit in the concatenation above. For example, if the premise is \(x\cdot z = x\) , then this rule, with argument \(\bot\) , concludes \(z = ''\) .
Also note that constants are split, such that for \((\mathsf{'abc'} \cdot x) = (\mathsf{'a'} \cdot y)\) , this rule, with argument \(\bot\) , concludes \((\mathsf{'bc'} \cdot x) = y\) . This splitting is done only for constants such that
Word::splitConstant
returns nonnull.

enumerator
CONCAT_UNIFY

Strings – Core rules – Concatenation unification
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid b}{t_1 = s_1}\]where \(b\) indicates if the direction is reversed.

enumerator
CONCAT_CONFLICT

Strings – Core rules – Concatenation conflict
\[\inferrule{(c_1\cdot t) = (c_2 \cdot s)\mid b}{\bot}\]where \(b\) indicates if the direction is reversed, \(c_1,\,c_2\) are constants such that \(\texttt{Word::splitConstant}(c_1,c_2, \mathit{index},b)\) is null, in other words, neither is a prefix of the other. Note it may be the case that one side of the equality denotes the empty string.
Alternatively, if the equality is between sequences, this rule has the form:
\[\inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot}\]where t_1 and s_1 are constants of length one, or otherwise one side of the equality is the empty sequence and t_1 or s_1 corresponding to that side is the empty sequence.

enumerator
CONCAT_SPLIT

Strings – Core rules – Concatenation split
\[\inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{(t_1 = s_1\cdot r_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\bot$}\]where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{suf}(s_1,\mathit{len}(t_1)))\) .
\[\inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{(t_1 = s_1\cdot r_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\top$}\]where \(r_t\) is \(\mathit{skolem}(\mathit{pre}(t_2,\mathit{len}(t_2)  \mathit{len}(s_2)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{pre}(s_2,\mathit{len}(s_2)  \mathit{len}(t_2)))\) .
Above, \(\mathit{suf}(x,n)\) is shorthand for \(\mathit{substr}(x,n, \mathit{len}(x)  n)\) and \(\mathit{pre}(x,n)\) is shorthand for \(\mathit{substr}(x,0,n)\) .

enumerator
CONCAT_CSPLIT

Strings – Core rules – Concatenation split for constants
\[\inferrule{(t_1\cdot t_2) = (c \cdot s_2),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)}\]where \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,1))\) .
Alternatively for the reverse:
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot c),\, \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot c)}\]where \(r\) is \(\mathit{skolem}(\mathit{pre}(t_2,\mathit{len}(t_2)  1))\) .

enumerator
CONCAT_LPROP

Strings – Core rules – Concatenation length propagation
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r_t)}\]where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\) .
Alternatively for the reverse:
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) > \mathit{len}(s_2)\mid \top}{(t_2 = r_t\cdot s_2)}\]where \(r_t\) is \(\mathit{skolem}(\mathit{pre}(t_2,\mathit{len}(t_2)  \mathit{len}(s_2)))\) .

enumerator
CONCAT_CPROP

Strings – Core rules – Concatenation constant propagation
\[\inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = w_3\cdot r)}\]where \(w_1,\,w_2,\,w_3\) are words, \(w_3\) is \(\mathit{pre}(w_2,p)\) , \(p\) is \(\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)\) , and \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(w_3)))\) . Note that \(\mathit{suf}(w_2,p)\) is the largest suffix of \(\mathit{suf}(w_2,1)\) that can contain a prefix of \(w_1\) ; since \(t_1\) is nonempty, \(w_3\) must therefore be contained in \(t_1\) .
Alternatively for the reverse:
\[\inferrule{(t_1\cdot w_1\cdot t_2) = (s \cdot w_2),\, \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot w_3)}\]where \(w_1,\,w_2,\,w_3\) are words, \(w_3\) is \(\mathit{suf}(w_2, \mathit{len}(w_2)  p)\) , \(p\) is \(\texttt{Word::roverlap}(\mathit{pre}(w_2, \mathit{len}(w_2)  1), w_1)\) , and \(r\) is \(\mathit{skolem}(\mathit{pre}(t_2, \mathit{len}(t_2)  \mathit{len}(w_3)))\) . Note that \(\mathit{pre}(w_2, \mathit{len}(w_2)  p)\) is the largest prefix of \(\mathit{pre}(w_2, \mathit{len}(w_2)  1)\) that can contain a suffix of \(w_1\) ; since \(t_2\) is nonempty, \(w_3\) must therefore be contained in \(t_2\) .

enumerator
STRING_DECOMPOSE

Strings – Core rules – String decomposition
\[\inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n}\]or alternatively for the reverse:
\[\inferrule{\mathit{len}(t) \geq n\mid \top}{t = w_1\cdot w_2 \wedge \mathit{len}(w_2) = n}\]where \(w_1\) is \(\mathit{skolem}(\mathit{pre}(t,n)\) and \(w_2\) is \(\mathit{skolem}(\mathit{suf}(t,n)\) .

enumerator
STRING_LENGTH_POS

Strings – Core rules – Length positive
\[\inferrule{\mid t}{(\mathit{len}(t) = 0\wedge t= '')\vee \mathit{len}(t) > 0}\]

enumerator
STRING_LENGTH_NON_EMPTY

Strings – Core rules – Length nonempty
\[\inferrule{t\neq ''\mid }{\mathit{len}(t) \neq 0}\]

enumerator
STRING_REDUCTION

Strings – Extended functions – Reduction
\[\inferrule{\mid t}{R\wedge t = w}\]where \(w\) is \(\texttt{strings::StringsPreprocess::reduce}(t, R, \dots)\) . In other words, \(R\) is the reduction predicate for extended term \(t\) , and \(w\) is \(skolem(t)\) .
Notice that the free variables of \(R\) are \(w\) and the free variables of \(t\) .

enumerator
STRING_EAGER_REDUCTION

Strings – Extended functions – Eager reduction
\[\inferrule{\mid t}{R}\]where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\) .

enumerator
RE_INTER

Strings – Regular expressions – Intersection
\[\inferrule{t\in R_1,\,t\in R_2\mid }{t\in \mathit{inter}(R_1,R_2)}\]

enumerator
RE_UNFOLD_POS

Strings – Regular expressions – Positive Unfold
\[\inferrule{t\in R\mid }{\texttt{RegExpOpr::reduceRegExpPos}(t\in R)}\]corresponding to the onestep unfolding of the premise.

enumerator
RE_UNFOLD_NEG

Strings – Regular expressions – Negative Unfold
\[\inferrule{t\not\in R\mid }{\texttt{RegExpOpr::reduceRegExpNeg}(t\not\in R)}\]corresponding to the onestep unfolding of the premise.

enumerator
RE_UNFOLD_NEG_CONCAT_FIXED

Strings – Regular expressions – Unfold negative concatenation, fixed
\[\inferrule{t\not\in R\mid }{\texttt{RegExpOpr::reduceRegExpNegConcatFixed}(t\not\in R,L,i)}\]where \(\texttt{RegExpOpr::getRegExpConcatFixed}(t\not\in R, i) = L\) , corresponding to the onestep unfolding of the premise, optimized for fixed length of component \(i\) of the regular expression concatenation \(R\) .

enumerator
RE_ELIM

Strings – Regular expressions – Elimination
\[\inferrule{\mid F,b}{F = \texttt{strings::RegExpElimination::eliminate}(F, b)}\]where \(b\) is a Boolean indicating whether we are using aggressive eliminations. Notice this rule concludes \(F = F\) if no eliminations are performed for \(F\) .

enumerator
STRING_CODE_INJ

Strings – Code points
\[\inferrule{\mid t,s}{\mathit{to\_code}(t) = 1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t\neq s}\]

enumerator
STRING_SEQ_UNIT_INJ

Strings – Sequence unit
\[\inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid }{x = y}\]Also applies to the case where \(\mathit{unit}(y)\) is a constant sequence of length one.

enumerator
STRING_INFERENCE

Strings – (Trusted) String inference
\[\inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F}\]used to bookkeep an inference that has not yet been converted via \(\texttt{strings::InferProofCons::convert}\) .

enumerator
MACRO_ARITH_SCALE_SUM_UB

Arithmetic – Adding inequalities
An arithmetic literal is a term of the form \(p \diamond c\) where \(\diamond \in \{ <, \leq, =, \geq, > \}\) , \(p\) a polynomial and \(c\) a rational constant.
\[\inferrule{l_1 \dots l_n \mid k_1 \dots k_n}{t_1 \diamond t_2}\]where \(k_i \in \mathbb{R}, k_i \neq 0\) , \(\diamond\) is the fusion of the \(\diamond_i\) (flipping each if its \(k_i\) is negative) such that \(\diamond_i \in \{ <, \leq \}\) (this implies that lower bounds have negative \(k_i\) and upper bounds have positive \(k_i\) ), \(t_1\) is the sum of the scaled polynomials and \(t_2\) is the sum of the scaled constants:
\[ \begin{align}\begin{aligned}t_1 \colon= k_1 \cdot p_1 + \cdots + k_n \cdot p_n\\t_2 \colon= k_1 \cdot c_1 + \cdots + k_n \cdot c_n\end{aligned}\end{align} \]

enumerator
ARITH_SUM_UB

Arithmetic – Sum upper bounds
\[\inferrule{P_1 \dots P_n \mid }{L \diamond R}\]where \(P_i\) has the form \(L_i \diamond_i R_i\) and \(\diamond_i \in \{<, \leq, =\}\) . Furthermore \(\diamond = <\) if \(\diamond_i = <\) for any \(i\) and \(\diamond = \leq\) otherwise, \(L = L_1 + \cdots + L_n\) and \(R = R_1 + \cdots + R_n\) .

enumerator
INT_TIGHT_UB

Arithmetic – Tighten strict integer upper bounds
\[\inferrule{i < c \mid }{i \leq \lfloor c \rfloor}\]where \(i\) has integer type.

enumerator
INT_TIGHT_LB

Arithmetic – Tighten strict integer lower bounds
\[\inferrule{i > c \mid }{i \geq \lceil c \rceil}\]where \(i\) has integer type.

enumerator
ARITH_TRICHOTOMY

Arithmetic – Trichotomy of the reals
\[\inferrule{A, B \mid C}{C}\]where \(\neg A, \neg B, C\) are \(x < c, x = c, x > c\) in some order. Note that \(\neg\) here denotes arithmetic negation, i.e., flipping \(\geq\) to \(<\) etc.

enumerator
ARITH_OP_ELIM_AXIOM

Arithmetic – Operator elimination
\[\inferrule{ \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}}\]

enumerator
ARITH_POLY_NORM

Arithmetic – Polynomial normalization
\[\inferrule{ \mid t = s}{t = s}\]where \(\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top\) .

enumerator
ARITH_MULT_SIGN

Arithmetic – Sign inference
\[\inferrule{ \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0}\]where \(f_1 \dots f_k\) are variables compared to zero (less, greater or not equal), \(m\) is a monomial from these variables and \(\diamond\) is the comparison (less or equal) that results from the signs of the variables. All variables with even exponent in \(m\) should be given as not equal to zero while all variables with odd exponent in \(m\) should be given as less or greater than zero.

enumerator
ARITH_MULT_POS

Arithmetic – Multiplication with positive factor
\[\inferrule{ \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r}\]where \(\diamond\) is a relation symbol.

enumerator
ARITH_MULT_NEG

Arithmetic – Multiplication with negative factor
\[\inferrule{ \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r}\]where \(\diamond\) is a relation symbol and \(\diamond_{inv}\) the inverted relation symbol.

enumerator
ARITH_MULT_TANGENT

Arithmetic – Multiplication tangent plane
\[ \begin{align}\begin{aligned}\inferruleSC{ \mid t, x, y, a, b, \sigma}{(t \leq tplane) \leftrightarrow ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = 1$}\\\inferruleSC{ \mid t, x, y, a, b, \sigma}{(t \geq tplane) \leftrightarrow ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = 1$}\end{aligned}\end{align} \]where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\) (possibly under rewriting), \(a,b\) are real constants, \(\sigma \in \{ 1, 1\}\) and \(tplane := b \cdot x + a \cdot y  a \cdot b\) is the tangent plane of \(x \cdot y\) at \((a,b)\) .

enumerator
ARITH_TRANS_PI

Arithmetic – Transcendentals – Assert bounds on Pi
\[\inferrule{ \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u}\]where \(l,u\) are valid lower and upper bounds on \(\pi\) .

enumerator
ARITH_TRANS_EXP_NEG

Arithmetic – Transcendentals – Exp at negative values
\[\inferrule{ \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)}\]

enumerator
ARITH_TRANS_EXP_POSITIVITY

Arithmetic – Transcendentals – Exp is always positive
\[\inferrule{ \mid t}{\exp(t) > 0}\]

enumerator
ARITH_TRANS_EXP_SUPER_LIN

Arithmetic – Transcendentals – Exp grows superlinearly for positive values
\[\inferrule{ \mid t}{t \leq 0 \lor \exp(t) > t+1}\]

enumerator
ARITH_TRANS_EXP_ZERO

Arithmetic – Transcendentals – Exp at zero
\[\inferrule{ \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)}\]

enumerator
ARITH_TRANS_EXP_APPROX_ABOVE_NEG

Arithmetic – Transcendentals – Exp is approximated from above for negative values
\[\inferrule{ \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\) . Let \(p\) be the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function. \(\texttt{secant}(\exp, l, u, t)\) denotes the secant of \(p\) from \((l, \exp(l))\) to \((u, \exp(u))\) evaluated at \(t\) , calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\) , then \(\exp(t\) is below the secant of \(p\) from \(l\) to \(u\) .

enumerator
ARITH_TRANS_EXP_APPROX_ABOVE_POS

Arithmetic – Transcendentals – Exp is approximated from above for positive values
\[\inferrule{ \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secantpos}(\exp, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\) . Let \(p^*\) be a modification of the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function as follows where \(p(d1)\) is the regular Maclaurin series of degree \(d1\) :
\[p^* := p(d1) \cdot \frac{1 + t^n}{n!}\]\(\texttt{secantpos}(\exp, l, u, t)\) denotes the secant of \(p\) from \((l, \exp(l))\) to \((u, \exp(u))\) evaluated at \(t\) , calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\) , then \(\exp(t\) is below the secant of \(p\) from \(l\) to \(u\) .

enumerator
ARITH_TRANS_EXP_APPROX_BELOW

Arithmetic – Transcendentals – Exp is approximated from below
\[\inferrule{ \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)}\]where \(d\) is an odd positive number, \(t\) an arithmetic term and \(\texttt{maclaurin}(\exp, d, c)\) is the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at \(c\) . The Maclaurin series for the exponential function is the following:
\[\exp(x) = \sum_{n=0}^{\infty} \frac{x^n}{n!}\]

enumerator
ARITH_TRANS_SINE_BOUNDS

Arithmetic – Transcendentals – Sine is always between 1 and 1
\[\inferrule{ \mid t}{\sin(t) \leq 1 \land \sin(t) \geq 1}\]

enumerator
ARITH_TRANS_SINE_SHIFT

Arithmetic – Transcendentals – Sine is shifted to pi…pi
\[\inferrule{ \mid x, y, s}{\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})}\]where \(x\) is the argument to sine, \(y\) is a new real skolem that is \(x\) shifted into \(\pi \dots \pi\) and \(s\) is a new integer slolem that is the number of phases \(y\) is shifted.

enumerator
ARITH_TRANS_SINE_SYMMETRY

Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument
\[\inferrule{ \mid t}{\sin(t)  \sin(t) = 0}\]

enumerator
ARITH_TRANS_SINE_TANGENT_ZERO

Arithmetic – Transcendentals – Sine is bounded by the tangent at zero
\[\inferrule{ \mid t}{(t > 0 \rightarrow \sin(t) < t) \land (t < 0 \rightarrow \sin(t) > t)} \]

enumerator
ARITH_TRANS_SINE_TANGENT_PI

Arithmetic – Transcendentals – Sine is bounded by the tangents at pi and pi
\[\inferrule{ \mid t}{(t > \pi \rightarrow \sin(t) > \pi  t) \land (t < \pi \rightarrow \sin(t) < \pi  t)} \]

enumerator
ARITH_TRANS_SINE_APPROX_ABOVE_NEG

Arithmetic – Transcendentals – Sine is approximated from above for negative values
\[\inferrule{ \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\) ) and \(l,u\) the evaluated lower and upper bounds on \(t\) . Let \(p\) be the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{secant}(\sin, l, u, t)\) denotes the secant of \(p\) from \((l, \sin(l))\) to \((u, \sin(u))\) evaluated at \(t\) , calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\) , then \(\sin(t)\) is below the secant of \(p\) from \(l\) to \(u\) .

enumerator
ARITH_TRANS_SINE_APPROX_ABOVE_POS

Arithmetic – Transcendentals – Sine is approximated from above for positive values
\[\inferrule{ \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\) ). Let \(p\) be the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{upper}(\sin, c)\) denotes the upper bound on \(\sin(c)\) given by \(p\) and \(lb,up\) such that \(\sin(t)\) is the maximum of the sine function on \((lb,ub)\) .

enumerator
ARITH_TRANS_SINE_APPROX_BELOW_NEG

Arithmetic – Transcendentals – Sine is approximated from below for negative values
\[\inferrule{ \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\) ). Let \(p\) be the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{lower}(\sin, c)\) denotes the lower bound on \(\sin(c)\) given by \(p\) and \(lb,up\) such that \(\sin(t)\) is the minimum of the sine function on \((lb,ub)\) .

enumerator
ARITH_TRANS_SINE_APPROX_BELOW_POS

Arithmetic – Transcendentals – Sine is approximated from below for positive values
\[\inferrule{ \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\) ) and \(l,u\) the evaluated lower and upper bounds on \(t\) . Let \(p\) be the \(d\) ’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{secant}(\sin, l, u, t)\) denotes the secant of \(p\) from \((l, \sin(l))\) to \((u, \sin(u))\) evaluated at \(t\) , calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\) , then \(\sin(t)\) is above the secant of \(p\) from \(l\) to \(u\) .

enumerator
ARITH_NL_COVERING_DIRECT

Arithmetic – Coverings – Direct conflict
We use \(\texttt{IRP}_k(poly)\) for an IndexedRootPredicate that is defined as the \(k\) ’th root of the polynomial \(poly\) . Note that \(poly\) may not be univariate; in this case, the value of \(\texttt{IRP}_k(poly)\) can only be calculated with respect to a (partial) model for all but one variable of \(poly\) .
A formula \(\texttt{Interval}(x_i)\) describes that a variable \(x_i\) is within a particular interval whose bounds are given as IRPs. It is either an open interval or a point interval:
\[ \begin{align}\begin{aligned}\texttt{IRP}_k(poly) < x_i < \texttt{IRP}_k(poly)\\x_i = \texttt{IRP}_k(poly)\end{aligned}\end{align} \]A formula \(\texttt{Cell}(x_1 \dots x_i)\) describes a portion of the real space in the following form:
\[\texttt{Interval}(x_1) \land \dots \land \texttt{Interval}(x_i)\]A cell can also be empty (for \(i = 0\) ).
A formula \(\texttt{Covering}(x_i)\) is a set of intervals, implying that \(x_i\) can be in neither of these intervals. To be a covering (of the real line), the union of these intervals should be the real numbers.
\[\inferrule{\texttt{Cell}, A \mid }{\bot}\]A direct interval is generated from an assumption \(A\) (in variables \(x_1 \dots x_i\) ) over a \(\texttt{Cell}(x_1 \dots x_i)\) . It derives that \(A\) evaluates to false over the cell. In the actual algorithm, it means that \(x_i\) can not be in the topmost interval of the cell.

enumerator
ARITH_NL_COVERING_RECURSIVE

Arithmetic – Coverings – Recursive interval
See
ARITH_NL_COVERING_DIRECT
for the necessary definitions.\[\inferrule{\texttt{Cell}, \texttt{Covering} \mid }{\bot}\]A recursive interval is generated from \(\texttt{Covering}(x_i)\) over \(\texttt{Cell}(x_1 \dots x_{i1})\) . It generates the conclusion that no \(x_i\) exists that extends the cell and satisfies all assumptions.

enumerator
LFSC_RULE

External – LFSC
Place holder for LFSC rules.
\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, A_1,\dots, A_m}{Q}\]Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external LFSC calculus.

enumerator
ALETHE_RULE

External – Alethe
Place holder for Alethe rules.
\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, Q', A_1,\dots, A_m}{Q}\]Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external Alethe calculus, and that \(Q'\) be the representation of Q to be printed by the Alethe printer.

enumerator
UNKNOWN

enumerator
ASSUME