Skip to content
Snippets Groups Projects
Commit a6a64807 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Restructure sections 

- Move things back to core concepts
- Add paragraphs theire for subproofs etc.
parent a0d5652b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 170 additions and 164 deletions
spec/doc.tex
+ 170
− 164
View file @ a6a64807
......@@ -379,6 +379,11 @@ of all proof rules used by SMT solvers supporting {\formatName}.
\section{Core Concepts of {\formatName}}
\label{sec:coreconcepts}
This section provides an overview of the core concepts of the proof
format and also introduces some notation used throughout this paper.
While the next section provides a formal semantic for the format,
this overview of the core concept should be very helpful for
practitioners.
\todo[inline]{Introduce subproofs and their notation, note that
there can be arbitrary steps between premise and subproof, find good
way to say that the premise can not be in a subproof.}
......@@ -412,7 +417,6 @@ are syntactically equal and the number of leading negations is even
for $\varphi$ and odd for $\bar{\psi}$, or vice versa. To simplify the
notation we will omit the sort of terms when possible.
\paragraph{Steps.}
A proof in the {\formatName} format is an indexed list of steps.
To mimic the concrete syntax we will write a step
......@@ -434,12 +438,9 @@ empty list of arguments $[a_1, \dots, a_m]$. The list of premises
only references earlier steps, such that the proof forms a directed
acyclic graph. The arguments $a_i$ are either terms or tuples $(x_i,
t_i)$ where $x_i$ is a variable and $t_i$ is a term. The interpretation
of the arguments is rule specific. A specialty of the veriT proof
format is the step context. The context is a possible empty list $[c_1,
\dots, c_l]$, where $c_i$ is either a variable or a variable-term tuple
denoted $x_i\mapsto t_i$. Throughout this document $\Gamma$ denotes
an arbitrary context. The context denotes a substitution as described
later in this section.
of the arguments is rule specific. The list \(\c_1, \dots, c_k\) is
the \emph{context} of the step. Contexts have their own section just
below.
Every proof ends with a step that has the empty clause as the conclusion
and an empty context. Section~\ref{sec:rules} provides an overview of
......@@ -455,6 +456,168 @@ assumption $\varphi$ and a formula $\psi$ proved by intermediate steps
from $\varphi$, the \proofRule{subproof} step deduces $\neg \varphi \lor
\psi$ and discharges $\varphi$.
\paragraph{Tautologous Rules and Simple Deduction.}
Most rules introduce tautologies. One example is
the \proofRule{and\_pos} rule: $\neg (\varphi_1 \land \varphi_2 \land
\dots \land \varphi_n) \lor \varphi_i$. Other rules operate on only
one premise. Those rules are primarily used to simplify Boolean
connectives during preprocessing. For example, the \proofRule{implies}
rule removes an implication: From $\varphi_1 \Rightarrow \varphi_2$
it deduces $\neg \varphi_1 \lor \varphi_2$.
\paragraph{Resolution.}
CDCL($T$)-based SMT solvers, and especially their SAT solvers,
are fundamentally based on clauses. Hence, {\formatName} also uses
clauses. Nevertheless, since SMT solvers do not enforce a strict
clausal normal-form, usual disjunction is also used
clauses simplifies checking the rules. For example, in the case of
resolution there is a clear distinction between unit clauses where
the sole literal starts with a disjunction, and non-unit clauses. The
syntax for clauses uses the \smtinline{cl} operator, while disjunctions
use the standard SMT-LIB \smtinline{or} operator. The \proofRule{or}
\emph{rule} is responsible for converting disjunctions to clauses.
The {\formatName} proofs use a generalized propositional
resolution rule with the rule name \proofRule{resolution} or
\proofRule{th\_resolution}. Both names denote the same rule. The
difference only serves to distinguish if the rule was introduced by
the SAT solver or by a theory solver. The resolution step is purely
propositional; there is currently no notion of a unifier.
The premises of a resolution step are clauses and the conclusion
is a clause that has been derived from the premises by some binary
resolution steps.
\paragraph{Quantifier Instantiation.}
To express quantifier instantiation, the rule \proofRule{forall\_inst}
is used. It produces a formula of the form $(\neg \forall x_1 \dots
x_n. \varphi)\lor \varphi[t_1/x_1]\dots[t_n/x_n]$, where $\varphi$ is
a term containing the free variables $(x_i)_{1\leq i\leq n}$, and $t_i$
are new variable free terms with the same sort as $x_i$.
The arguments of a \proofRule{forall\_inst} step is the list \((x_1
, t_1), \dots, (x_n, t_n)\). While this information can
be recovered from the term, providing this information explicitly
aids reconstruction because the implicit reordering of equalities
(see below) obscure which terms have been used as instances.
Existential quantifiers are handled by Skolemization.
\paragraph{Subproofs and Lemmas.}
The proof format supports lemmas that introduces local assumption and
derives a new theorems, like:
\begin{minted}[linenos]{smtlib2.py -x}
(anchor :step t9 :args ())
(assume t9.t1 (cl (= (+ 2 2) 5)))
(step t9.t2 (cl (= (+ 2 2) 4)) :plus_simplify)
(step t9.t3 (cl (= 4 5)) :rule trans :premises (t9.t1 t9.t2))
(step t9 (cl (not (= (+2 2) 5)) (= 4 5)))
\end{minted}
While not part of our rules, such lemmas trivially compile down to the
rules by inlining all assumptions in each step.
\begin{figure}[t]
\begin{minted}[linenos]{smtlib2.py -x}
(assume h1 (not (p a)))
(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
...
(anchor :step t9 :args ((:= z2 vr4)))
(step t9.t1 (cl (= z2 vr4)) :rule refl)
(step t9.t2 (cl (= (p z2) (p vr4))) :rule cong :premises (t9.t1))
(step t9 (cl (= (forall ((z2 U)) (p z2)) (forall ((vr4 U)) (p vr4))))
:rule bind)
...
(step t14 (cl (forall ((vr5 U)) (p vr5)))
:rule th_resolution :premises (t11 t12 t13))
(step t15 (cl (or (not (forall ((vr5 U)) (p vr5))) (p a)))
:rule forall_inst :args ((:= vr5 a)))
(step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
:rule or :premises (t15))
(step t17 (cl) :rule resolution :premises (t16 h1 t14))
\end{minted}
\caption{Example proof output. Assumptions are introduced (line 1--2);
a subproof renames bound variables (line 4--8); the proof finishes with
instantiaton and resolution steps (line 10--15)}\label{fig:proof_ex}
\end{figure}
\paragraph{Contexts.}
A specialty of the veriT proof
format is the step context. The context is a possible empty list $[c_1,
\dots, c_l]$, where $c_i$ is either a variable or a variable-term tuple
denoted $x_i\mapsto t_i$. Throughout this document $\Gamma$ denotes
an arbitrary context. The context denotes a substitution.\todo{Extend}
\paragraph{Skolemization and Other Preprocessing Steps.}
One typical example for a rule with context is the \proofRule{sko\_ex}
rule, which is used to express Skolemization of an existentially
quantified variable. It is a applied to a premise $n$ with a context
that maps a variable $x$ to the appropriate Skolem term and produces
a step $m$ ($m > n$) where the variable is quantified.
\begin{plListEq}
\Gamma, x\mapsto (\epsilon x.\varphi) &\proofsep n.&\varphi \simeq \psi &(\proofRule{\dots})\\
\Gamma &\proofsep m.& (\exists x.\varphi) \simeq \psi &(\proofRule{sko\_ex};\: n)
\end{plListEq}
\begin{example}
To illustrate how such a rule is applied, consider the following example
taken from~\cite{barbosa-2019}. Here the term $\neg p(\epsilon x.\neg
p(x))$ is Skolemized. The \proofRule{refl} rule expresses
a simple tautology on the equality (reflexivity in this case), \proofRule{cong}
is functional congruence, and \proofRule{sko\_forall} works like
\proofRule{sko\_ex}, except that the choice term is $\epsilon x.\neg\varphi$.
\begin{plListEqAlgn}
x\mapsto (\epsilon x.\neg p(x)) \proofsep& 1.& x &\simeq \epsilon x.\neg p(x) &(\proofRule{refl})\\
x\mapsto (\epsilon x.\neg p(x)) \proofsep& 2.& p(x) &\simeq p(\epsilon x.\neg p(x)) &(\proofRule{cong};\: 1)\\
\proofsep& 3.&( \forall x.p(x))&\simeq p(\epsilon x.\neg p(x)) &(\proofRule{sko\_forall};\: 2)\\
\proofsep& 4.&(\neg\forall x.p(x))&\simeq \neg p(\epsilon x.\neg p(x)) &(\proofRule{cong};\: 3)
\end{plListEqAlgn}
\end{example}
\paragraph{Linear Arithmetic.}
Proofs for linear arithmetic use a number of straightforward rules,
such as \proofRule{la\_totality}: $t_1 \leq t_2 \lor t_2 \leq t_1$
and the main rule \proofRule{la\_generic}. The conclusion of an
\proofRule{la\_generic} step is a tautology $\neg \varphi_1, \neg
\varphi_2, \dots, \neg \varphi_n$ where the $\varphi_i$ are linear
(in)equalities. Checking the validity of these formulas amounts to
checking the unsatisfiability of the system of linear equations
$\varphi_1, \varphi_2, \dots, \varphi_n$. The annotation of an
\proofRule{la\_generic} step contains a coefficient for each (in)equality.
The result of forming the linear combination of the literals with
the coefficients is a trivial inequality between constants.
\begin{example}
The following example is the proof generated by veriT for the unsatisfiability
of $(x+y<1) \lor (3<x)$, $x\simeq 2$, and $0\simeq y$.
\begin{plListEq}
\proofsep& 1.& (3 < x) \lor (x + y < 1) &(\proofRule{assume})\\
\proofsep& 2.& x\simeq 2 &(\proofRule{assume})\\
\proofsep& 3.& 0\simeq y &(\proofRule{assume})\\
\proofsep& 4.& \neg (3<x) \lor \neg (x\simeq 2) &(\proofRule{la\_generic};\: ;1.0, 1.0)\\
\proofsep& 5.& \neg (3<x) &(\proofRule{resolution}; 2, 4)\\
\proofsep& 6.& x + y < 1 &(\proofRule{resolution}; 1, 5)\\
\proofsep& 7.& \neg (x + y < 1) \lor \neg (x\simeq 2) \lor \neg (0 \simeq y)
&(\proofRule{la\_generic};\: ;1.0, 1.0, 1.0)\\
\proofsep& 8.& \bot &(\proofRule{resolution};\:\; 7, 6, 2, 3)
\end{plListEq}
\end{example}
\paragraph{Implicit Reordering of Equalities.}
In addition to the explicit steps, solvers might reorder equalities, i.e.,
apply symmetry of the equality predicate, without generating steps.
The SMT solver veriT currently applies this liberty in a restricted
form: equalities are only reordered
when the term below the equality change during proof search. One such
case is the instantiation of universally quantified variables. If an
instantiated variable appears below an equality, then the equality might
have an arbitrary order after instantiation.
Nevertheless, consumers of {\formatName} must consider the possible
implicit reordering of equalities.
\section{The Concrete Semantics}
\label{sec:semantic}
......@@ -703,163 +866,6 @@ applicability. In particular the {\Taut} rule is very hard to check und is
specialized.
\paragraph{Tautologous Rules and Simple Deduction.}
Most rules introduce tautologies. One example is
the \proofRule{and\_pos} rule: $\neg (\varphi_1 \land \varphi_2 \land
\dots \land \varphi_n) \lor \varphi_i$. Other rules operate on only
one premise. Those rules are primarily used to simplify Boolean
connectives during preprocessing. For example, the \proofRule{implies}
rule removes an implication: From $\varphi_1 \Rightarrow \varphi_2$
it deduces $\neg \varphi_1 \lor \varphi_2$.
\paragraph{Skolemization and Other Preprocessing Steps.}
One typical example for a rule with context is the \proofRule{sko\_ex}
rule, which is used to express Skolemization of an existentially
quantified variable. It is a applied to a premise $n$ with a context
that maps a variable $x$ to the appropriate Skolem term and produces
a step $m$ ($m > n$) where the variable is quantified.
\begin{plListEq}
\Gamma, x\mapsto (\epsilon x.\varphi) &\proofsep n.&\varphi \simeq \psi &(\proofRule{\dots})\\
\Gamma &\proofsep m.& (\exists x.\varphi) \simeq \psi &(\proofRule{sko\_ex};\: n)
\end{plListEq}
\begin{example}
To illustrate how such a rule is applied, consider the following example
taken from~\cite{barbosa-2019}. Here the term $\neg p(\epsilon x.\neg
p(x))$ is Skolemized. The \proofRule{refl} rule expresses
a simple tautology on the equality (reflexivity in this case), \proofRule{cong}
is functional congruence, and \proofRule{sko\_forall} works like
\proofRule{sko\_ex}, except that the choice term is $\epsilon x.\neg\varphi$.
\begin{plListEqAlgn}
x\mapsto (\epsilon x.\neg p(x)) \proofsep& 1.& x &\simeq \epsilon x.\neg p(x) &(\proofRule{refl})\\
x\mapsto (\epsilon x.\neg p(x)) \proofsep& 2.& p(x) &\simeq p(\epsilon x.\neg p(x)) &(\proofRule{cong};\: 1)\\
\proofsep& 3.&( \forall x.p(x))&\simeq p(\epsilon x.\neg p(x)) &(\proofRule{sko\_forall};\: 2)\\
\proofsep& 4.&(\neg\forall x.p(x))&\simeq \neg p(\epsilon x.\neg p(x)) &(\proofRule{cong};\: 3)
\end{plListEqAlgn}
\end{example}
\paragraph{Linear Arithmetic.}
Proofs for linear arithmetic use a number of straightforward rules,
such as \proofRule{la\_totality}: $t_1 \leq t_2 \lor t_2 \leq t_1$
and the main rule \proofRule{la\_generic}. The conclusion of an
\proofRule{la\_generic} step is a tautology $\neg \varphi_1, \neg
\varphi_2, \dots, \neg \varphi_n$ where the $\varphi_i$ are linear
(in)equalities. Checking the validity of these formulas amounts to
checking the unsatisfiability of the system of linear equations
$\varphi_1, \varphi_2, \dots, \varphi_n$. The annotation of an
\proofRule{la\_generic} step contains a coefficient for each (in)equality.
The result of forming the linear combination of the literals with
the coefficients is a trivial inequality between constants.
\begin{example}
The following example is the proof generated by veriT for the unsatisfiability
of $(x+y<1) \lor (3<x)$, $x\simeq 2$, and $0\simeq y$.
\begin{plListEq}
\proofsep& 1.& (3 < x) \lor (x + y < 1) &(\proofRule{assume})\\
\proofsep& 2.& x\simeq 2 &(\proofRule{assume})\\
\proofsep& 3.& 0\simeq y &(\proofRule{assume})\\
\proofsep& 4.& \neg (3<x) \lor \neg (x\simeq 2) &(\proofRule{la\_generic};\: ;1.0, 1.0)\\
\proofsep& 5.& \neg (3<x) &(\proofRule{resolution}; 2, 4)\\
\proofsep& 6.& x + y < 1 &(\proofRule{resolution}; 1, 5)\\
\proofsep& 7.& \neg (x + y < 1) \lor \neg (x\simeq 2) \lor \neg (0 \simeq y)
&(\proofRule{la\_generic};\: ;1.0, 1.0, 1.0)\\
\proofsep& 8.& \bot &(\proofRule{resolution};\:\; 7, 6, 2, 3)
\end{plListEq}
\end{example}
\paragraph{Resolution.}
CDCL($T$)-based SMT solvers, and especially their SAT solvers,
are fundamentally based on clauses. Hence, {\formatName} also uses
clauses. Nevertheless, since SMT solvers do not enforce a strict
clausal normal-form, usual disjunction is also used
clauses simplifies checking the rules. For example, in the case of
resolution there is a clear distinction between unit clauses where
the sole literal starts with a disjunction, and non-unit clauses. The
syntax for clauses uses the \smtinline{cl} operator, while disjunctions
use the standard SMT-LIB \smtinline{or} operator. The \proofRule{or}
\emph{rule} is responsible for converting disjunctions to clauses.
The {\formatName} proofs use a generalized propositional
resolution rule with the rule name \proofRule{resolution} or
\proofRule{th\_resolution}. Both names denote the same rule. The
difference only serves to distinguish if the rule was introduced by
the SAT solver or by a theory solver. The resolution step is purely
propositional; there is currently no notion of a unifier.
The premises of a resolution step are clauses and the conclusion
is a clause that has been derived from the premises by some binary
resolution steps.
\paragraph{Quantifier Instantiation.}
To express quantifier instantiation, the rule \proofRule{forall\_inst}
is used. It produces a formula of the form $(\neg \forall x_1 \dots
x_n. \varphi)\lor \varphi[t_1/x_1]\dots[t_n/x_n]$, where $\varphi$ is
a term containing the free variables $(x_i)_{1\leq i\leq n}$, and $t_i$
are new variable free terms with the same sort as $x_i$.
The arguments of a \proofRule{forall\_inst} step is the list \((x_1
, t_1), \dots, (x_n, t_n)\). While this information can
be recovered from the term, providing this information explicitly
aids reconstruction because the implicit reordering of equalities
(see below) obscure which terms have been used as instances.
Existential quantifiers are handled by Skolemization.
\paragraph{Implicit Reordering of Equalities.}
In addition to the explicit steps, solvers might reorder equalities, i.e.,
apply symmetry of the equality predicate, without generating steps.
The SMT solver veriT currently applies this liberty in a restricted
form: equalities are only reordered
when the term below the equality change during proof search. One such
case is the instantiation of universally quantified variables. If an
instantiated variable appears below an equality, then the equality might
have an arbitrary order after instantiation.
Nevertheless, consumers of {\formatName} must consider the possible
implicit reordering of equalities.
\paragraph{Lemmas}
Our proof format supports lemmas that introduces local assumption and derives a
new theorems, like:
\begin{minted}[linenos]{smtlib2.py -x}
(anchor :step t9 :args ())
(assume t9.t1 (cl (= (+ 2 2) 5)))
(step t9.t2 (cl (= (+ 2 2) 4)) :plus_simplify)
(step t9.t3 (cl (= 4 5)) :rule trans :premises (t9.t1 t9.t2))
(step t9 (cl (not (= (+2 2) 5)) (= 4 5)))
\end{minted}
While not part of our rules, such lemmas trivially compile down to the rules by
inlining all assumptions in each step.
\begin{figure}[t]
\begin{minted}[linenos]{smtlib2.py -x}
(assume h1 (not (p a)))
(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
...
(anchor :step t9 :args ((:= z2 vr4)))
(step t9.t1 (cl (= z2 vr4)) :rule refl)
(step t9.t2 (cl (= (p z2) (p vr4))) :rule cong :premises (t9.t1))
(step t9 (cl (= (forall ((z2 U)) (p z2)) (forall ((vr4 U)) (p vr4))))
:rule bind)
...
(step t14 (cl (forall ((vr5 U)) (p vr5)))
:rule th_resolution :premises (t11 t12 t13))
(step t15 (cl (or (not (forall ((vr5 U)) (p vr5))) (p a)))
:rule forall_inst :args ((:= vr5 a)))
(step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
:rule or :premises (t15))
(step t17 (cl) :rule resolution :premises (t16 h1 t14))
\end{minted}
\caption{Example proof output. Assumptions are introduced (line 1--2);
a subproof renames bound variables (line 4--8); the proof finishes with
instantiaton and resolution steps (line 10--15)}\label{fig:proof_ex}
\end{figure}
\section{The Concrete Syntax}
\label{sec:syntax}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment