diff --git a/spec/alethe_rules.tex b/spec/alethe_rules.tex
index b65e1d19d72c790a7128a83d1259b598257376e6..c9c1b4d31ce0b323202918c8f29d9f941d4cc9d6 100644
--- a/spec/alethe_rules.tex
+++ b/spec/alethe_rules.tex
@@ -20,29 +20,29 @@ to quickly find the definition of rules.
\begin{xltabular}{\linewidth}{l X}
\caption{Special rules.}
\label{rule-tab:special}\\
- Rule & Description \\
- \hline
- \ruleref{assume} & Repetition of an input assumption. \\
- \ruleref{hole} & Placeholder for rules not defined here. \\
- \ruleref{subproof} & Concludes a subproof and discharges local assumptions. \\
+ Rule & Description \\
+ \hline
+ \ruleref{assume} & Repetition of an input assumption. \\
+ \ruleref{hole} & Placeholder for rules not defined here. \\
+ \ruleref{subproof} & Concludes a subproof and discharges local assumptions. \\
\end{xltabular}
\begin{xltabular}{\linewidth}{l X}
\caption{Resolution and related rules.}
\label{rule-tab:resolution}\\
- Rule & Description \\
- \hline
- \ruleref{resolution} & Chain resolution of two or more clauses. \\
- \ruleref{th_resolution} & As \proofRule{resolution}, but used by theory solvers. \\
- \ruleref{tautology} & Simplification of tautological clauses to $\top$. \\
- \ruleref{contraction} & Removal of duplicated literals. \\
+ Rule & Description \\
+ \hline
+ \ruleref{resolution} & Chain resolution of two or more clauses. \\
+ \ruleref{th_resolution} & As \proofRule{resolution}, but used by theory solvers. \\
+ \ruleref{tautology} & Simplification of tautological clauses to $\top$. \\
+ \ruleref{contraction} & Removal of duplicated literals. \\
\end{xltabular}
\begin{xltabular}{\linewidth}{l X}
\caption{Rules introducing tautologies.}
\label{rule-tab:tautologies}\\
- Rule & Description \\
- \hline
+ Rule & Description \\
+ \hline
\ruleref{true} & $\top$ \\
\ruleref{false} & $\neg\bot$ \\
\ruleref{not_not} & $\neg(\neg\neg\varphi), \varphi$ \\
@@ -104,8 +104,8 @@ to quickly find the definition of rules.
\begin{xltabular}{\linewidth}{l X}
\caption{Linear arithmetic rules.}
\label{rule-tab:la-tauts}\\
- Rule & Description \\
- \hline
+ Rule & Description \\
+ \hline
\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
\ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
@@ -123,8 +123,8 @@ to quickly find the definition of rules.
\begin{xltabular}{\linewidth}{l X}
\caption{Quantifier handling.}
\label{rule-tab:quants}\\
- Rule & Description \\
- \hline
+ Rule & Description \\
+ \hline
\ruleref{forall_inst} & Instantiation of a universal variable. \\
\ruleref{bind} & Renaming of bound variables. \\
\ruleref{sko_ex} & Skolemization of existential variables. \\
@@ -139,8 +139,8 @@ to quickly find the definition of rules.
\begin{xltabular}{\linewidth}{l X}
\caption{Skolemization rules.}
\label{rule-tab:skos}\\
- Rule & Description \\
- \hline
+ Rule & Description \\
+ \hline
\ruleref{sko_ex} & Skolemization of existential variables. \\
\ruleref{sko_forall} & Skolemization of universal variables. \\
\end{xltabular}
@@ -149,8 +149,8 @@ to quickly find the definition of rules.
\caption{Clausification rules. These rules can be used to perform propositional
clausification.}
\label{rule-tab:clausification}\\
- Rule & Description \\
- \hline
+ Rule & Description \\
+ \hline
\ruleref{and} & And elimination. \\
\ruleref{not_or} & Elimination of a negated disjunction. \\
\ruleref{or} & Disjunction to clause. \\
@@ -204,8 +204,8 @@ $\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \\
\caption{Simplification rules. These rules represent typical operator-level
simplifications.}
\label{rule-tab:simplification}\\
- Rule & Description \\
- \hline
+ Rule & Description \\
+ \hline
\ruleref{connective_def} & Definition of the Boolean connectives. \\
\ruleref{and_simplify} & Simplification of a conjunction. \\
\ruleref{or_simplify} & Simplification of a disjunction. \\
@@ -236,12 +236,12 @@ simplifications.}
\begin{AletheX}
$i$. & \ctxsep & $\varphi$ & \currule \\
\end{AletheX}
- where $\varphi$ corresponds up to the orientation of equalities
- to a formula asserted in the input problem.
- \ruleparagraph{Remark.}
- This rule can not be used by the
- \inlineAlethe{(step }\dots\inlineAlethe{)} command. Instead it corresponds to the dedicated
- \inlineAlethe{(assume }\dots\inlineAlethe{)} command.
+ where $\varphi$ corresponds up to the orientation of equalities
+ to a formula asserted in the input problem.
+ \ruleparagraph{Remark.}
+ This rule can not be used by the
+ \inlineAlethe{(step }\dots\inlineAlethe{)} command. Instead it corresponds to the dedicated
+ \inlineAlethe{(assume }\dots\inlineAlethe{)} command.
\end{RuleDescription}
\begin{RuleDescription}{hole}
@@ -400,11 +400,11 @@ each $i$, let $\varphi := \varphi_i$ and $a := a_i$.
\begin{enumerate}
\item If $\varphi = s_1 > s_2$, then let $\varphi := s_1 \leq s_2$.
- If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
- If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
- If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
- the literal.
- \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
+ If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
+ If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
+ If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
+ the literal.
+ \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
\item Replace $\varphi$ by $\sum_{i=0}^{n}c_i\times{}t_i - \sum_{i=n+1}^{m} c_i\times{}t_i
\bowtie d$ where $d := d_2 - d_1$.
\item \label{la_generic:str}Now $\varphi$ has the form $s_1 \bowtie d$. If all
@@ -537,8 +537,8 @@ as for the rule \proofRule{la_generic}.
\begin{AletheXS}
\aletheLineSB
$j$. & \spctx{ $\Gamma, y_1,\dots, y_n, x_1 \mapsto y_1, \dots , x_n \mapsto y_n$}
- & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
- \spsep
+ & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
+ \spsep
$k$. & & \ctxsep &
$\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
& \currule{} \\
@@ -554,8 +554,8 @@ The \currule{} rule skolemizes existential quantifiers.
\aletheLineS
$j$. &
\spctx{$\Gamma, x_1 \mapsto \varepsilon_1, \dots , x_n \mapsto \varepsilon_n$}
- & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
- \spsep
+ & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
+ \spsep
$k$. & & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
\end{AletheXS}
where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
@@ -569,7 +569,7 @@ The \currule{} rule skolemizes universal quantifiers.
\aletheLineS
$j$. &
\spctx{$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots, x_n \mapsto (\varepsilon x_n.\neg\varphi)$}
- & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
+ & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
\spsep
$k$. & & \ctxsep & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
\end{AletheXS}
@@ -1080,11 +1080,11 @@ The possible transformations are:
\item $\bot \rightarrow \varphi ⇒ \top$
\item $ \varphi \rightarrow \top ⇒ \top$
\item $\top \rightarrow \varphi ⇒ \varphi$
- \item $ \varphi \rightarrow \bot ⇒ \neg \varphi$
- \item $ \varphi \rightarrow \varphi ⇒ \top$
- \item $\neg \varphi \rightarrow \varphi ⇒ \varphi$
- \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
- \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒ \varphi_1\lor \varphi_2$
+ \item $ \varphi \rightarrow \bot ⇒ \neg \varphi$
+ \item $ \varphi \rightarrow \varphi ⇒ \top$
+ \item $\neg \varphi \rightarrow \varphi ⇒ \varphi$
+ \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
+ \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒ \varphi_1\lor \varphi_2$
\end{itemize}
\end{RuleDescription}
@@ -1122,13 +1122,13 @@ where $\psi$ is the transformed term.
The possible transformations are:
\begin{itemize}
- \item $\neg(\varphi_1\rightarrow \varphi_2) ⇒ (\varphi_1 \land \neg \varphi_2)$
- \item $\neg(\varphi_1\lor \varphi_2) ⇒ (\neg \varphi_1 \land \neg \varphi_2)$
- \item $\neg(\varphi_1\land \varphi_2) ⇒ (\neg \varphi_1 \lor \neg \varphi_2)$
- \item $(\varphi_1 \rightarrow (\varphi_2\rightarrow \varphi_3)) ⇒ (\varphi_1\land \varphi_2) \rightarrow \varphi_3$
- \item $((\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2) ⇒ (\varphi_1\lor \varphi_2)$
- \item $(\varphi_1 \land (\varphi_1\rightarrow \varphi_2)) ⇒ (\varphi_1 \land \varphi_2)$
- \item $((\varphi_1\rightarrow \varphi_2) \land \varphi_1) ⇒ (\varphi_1 \land \varphi_2)$
+ \item $\neg(\varphi_1\rightarrow \varphi_2) ⇒ (\varphi_1 \land \neg \varphi_2)$
+ \item $\neg(\varphi_1\lor \varphi_2) ⇒ (\neg \varphi_1 \land \neg \varphi_2)$
+ \item $\neg(\varphi_1\land \varphi_2) ⇒ (\neg \varphi_1 \lor \neg \varphi_2)$
+ \item $(\varphi_1 \rightarrow (\varphi_2\rightarrow \varphi_3)) ⇒ (\varphi_1\land \varphi_2) \rightarrow \varphi_3$
+ \item $((\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2) ⇒ (\varphi_1\lor \varphi_2)$
+ \item $(\varphi_1 \land (\varphi_1\rightarrow \varphi_2)) ⇒ (\varphi_1 \land \varphi_2)$
+ \item $((\varphi_1\rightarrow \varphi_2) \land \varphi_1) ⇒ (\varphi_1 \land \varphi_2)$
\end{itemize}
\end{RuleDescription}
@@ -1165,9 +1165,9 @@ The possible transformations are:
\item $\lsymb{ite}\, \psi \, t \, t ⇒ t$
\item $\lsymb{ite}\, \neg \varphi \, t_1 \, t_2 ⇒ \lsymb{ite}\, \varphi \, t_2 \, t_1$
\item $\lsymb{ite}\, \psi \, (\lsymb{ite}\, \psi\,t_1\,t_2)\, t_3 ⇒
- \lsymb{ite}\, \psi\, t_1\, t_3$
+ \lsymb{ite}\, \psi\, t_1\, t_3$
\item $\lsymb{ite}\, \psi \, t_1\, (\lsymb{ite}\, \psi\,t_2\,t_3) ⇒
- \lsymb{ite}\, \psi\, t_1\, t_3$
+ \lsymb{ite}\, \psi\, t_1\, t_3$
\item $\lsymb{ite}\, \psi \, \top\, \bot ⇒ \psi$
\item $\lsymb{ite}\, \psi \, \bot\, \top ⇒ \neg\psi$
\item $\lsymb{ite}\, \psi \, \top \, \varphi ⇒ \psi\lor\varphi$
@@ -1193,7 +1193,7 @@ variables that can only have one value.
\begin{AletheXS}
\aletheLineS
$j$. & \spctx{$\Gamma, x_{k_1},\dots, x_{k_m}, x_{j_1} \mapsto t_{j_1}, \dots , x_{j_o} \mapsto t_{j_o}$}
- & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
+ & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
\spsep
$k$. & & \ctxsep & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
\end{AletheXS}
@@ -1283,9 +1283,9 @@ The possible transformations are:
\begin{itemize}
\item $t\, /\, t ⇒ 1$
\item $t\, /\, 1 ⇒ t$
- \item $t_1\, /\, t_2 ⇒ t_3$
- if $t_1$ and $t_2$ are constants and $t_3$ is $t_1$
- divided by $t_2$ according to the semantic of the current theory.
+ \item $t_1\, /\, t_2 ⇒ t_3$
+ if $t_1$ and $t_2$ are constants and $t_3$ is $t_1$
+ divided by $t_2$ according to the semantic of the current theory.
\end{itemize}
\end{RuleDescription}
@@ -1305,12 +1305,12 @@ The possible transformations are:
\item $t_1\times\cdots\times t_n ⇒ 0$ if any
$t_i$ is $0$.
\item $t_1\times\cdots\times t_n ⇒
- c \times t_{k_1}\times\cdots\times t_{k_n}$ where $c$
- is the product of the constants of $t_1, \dots, t_n$ and
- $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
- with the constants removed.
+ c \times t_{k_1}\times\cdots\times t_{k_n}$ where $c$
+ is the product of the constants of $t_1, \dots, t_n$ and
+ $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
+ with the constants removed.
\item $t_1\times\cdots\times t_n ⇒
- t_{k_1}\times\cdots\times t_{k_n}$: same as above if $c$ is $1$.
+ t_{k_1}\times\cdots\times t_{k_n}$: same as above if $c$ is $1$.
\end{itemize}
\end{RuleDescription}
@@ -1360,13 +1360,13 @@ The possible transformations are:
\item $t_1+\cdots+t_n ⇒ c$ where all
$t_i$ are constants and $c$ is their sum.
\item $t_1+\cdots+t_n ⇒
- c + t_{k_1}+\cdots+t_{k_n}$ where $c$
- is the sum of the constants of $t_1, \dots, t_n$ and
- $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
- with the constants removed.
+ c + t_{k_1}+\cdots+t_{k_n}$ where $c$
+ is the sum of the constants of $t_1, \dots, t_n$ and
+ $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
+ with the constants removed.
\item $t_1+\cdots+t_n ⇒
- t_{k_1}+\cdots+t_{k_n}$: same as above if $c$ is
- $0$.
+ t_{k_1}+\cdots+t_{k_n}$: same as above if $c$ is
+ $0$.
\end{itemize}
\end{RuleDescription}
@@ -1405,16 +1405,16 @@ $i_1$. & $\Gamma$ & \ctxsep & $t_{1} ≈ s_{1}$ & ($\dots$) \\
$i_n$. & $\Gamma$ & \ctxsep & $t_{n} ≈ s_{n}$ & ($\dots$) \\
\aletheLineS
$j$. & \spctx{$\Gamma, x_1 \mapsto s_1, \dots, x_n \mapsto s_n$}
- & \ctxsep & $u ≈ u'$ & ($\dots$) \\
+ & \ctxsep & $u ≈ u'$ & ($\dots$) \\
\spsep
$k$. & $\Gamma$ & \ctxsep &
$(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u) ≈ u'$
& (\currule{}\;$i_1$, \dots, $i_n$) \\
\end{AletheXS}
- The premise $i_1, \dots, i_n$ must be in the same subproof as
- the \currule{} step. If for $t_i≈ s_i$ the $t_i$ and $s_i$
- are syntactically equal, the premise
+ The premise $i_1, \dots, i_n$ must be in the same subproof as
+ the \currule{} step. If for $t_i≈ s_i$ the $t_i$ and $s_i$
+ are syntactically equal, the premise
is skipped.
\end{RuleDescription}
@@ -1515,7 +1515,7 @@ The term $t$ (the formula $\varphi$) contains the $\lsymb{ite}$ operator.
Let $s_1, \dots, s_n$ be the terms starting with $\lsymb{ite}$, i.e.
$s_i := \lsymb{ite}\,\psi_i\,r_i\,r'_i$, then $u_i$ has the form
\[
- \lsymb{ite}\,\psi_i\,(s_i ≈ r_i)\,(s_i ≈ r'_i)
+ \lsymb{ite}\,\psi_i\,(s_i ≈ r_i)\,(s_i ≈ r'_i)
\]
The term $t'$ is equal to the term $t$ up to the
reordering of equalities where one argument is an $\lsymb{ite}$
diff --git a/spec/spec.tex b/spec/spec.tex
index e0547d5994fb15cb25702ebf0a4578d33fa3389f..aeb5c6e4ab6b1ee403bd9ac8976065a101d155d9 100644
--- a/spec/spec.tex
+++ b/spec/spec.tex
@@ -89,7 +89,7 @@
\newcolumntype{Y}{>{\centering\arraybackslash}X}
\newcommand{\ruleTypeImpl}[1]{%
- \microtypesetup{tracking=false}\textsf{#1}\microtypesetup{tracking=true}%
+ \microtypesetup{tracking=false}\textsf{#1}\microtypesetup{tracking=true}%
}
\def\ruleType#1{\ruleTypeImpl{\detokenize{#1}}} % non linked rule (for examples)
\def\proofRule#1{\hyperref[rule:\detokenize{#1}]{\ruleTypeImpl{\detokenize{#1}}}} % linked rule
@@ -199,10 +199,10 @@ break
\and Hans-Jörg Schurr\textsuperscript{4}}
\date{}
\publishers{
- \textsuperscript{1} Universidade Federal de Minas Gerais, Brazil\\
- \textsuperscript{2} Albert-Ludwig-Universität Freiburg, Germany\\
- \textsuperscript{3} Université de Liège, Belgium\\
- \textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy, France\\
+ \textsuperscript{1} Universidade Federal de Minas Gerais, Brazil\\
+ \textsuperscript{2} Albert-Ludwig-Universität Freiburg, Germany\\
+ \textsuperscript{3} Université de Liège, Belgium\\
+ \textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy, France\\
}
@@ -583,7 +583,7 @@ variable.
\spsep
5.& & \ctxsep & $\forall x.\,(P\,x) ≈ \forall y.\,(P\,y)$ & $\proofRule{bind}$ \\
6.& & \ctxsep &
- $\neg(\forall x.\,(P\,x) ≈ \forall y.\,(P\,y))$, $\neg(\forall x.\,(P\,x)), (\forall y.\,(P\,y))$
+ $\neg(\forall x.\,(P\,x) ≈ \forall y.\,(P\,y))$, $\neg(\forall x.\,(P\,x)), (\forall y.\,(P\,y))$
& $\proofRule{equiv_pos2}$ \\
7.& &\ctxsep & $\bot$ & $(\proofRule{resolution}\,1, 2, 5, 6)$ \\
\end{AletheS}
@@ -630,7 +630,7 @@ logic and term language, it also uses commands to structure the proof.
An Alethe proof is a list of commands.
\begin{figure}[t]
- \begin{AletheVerb}
+ \begin{AletheVerb}
(assume h1 (not (p a)))
(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
...
@@ -650,7 +650,7 @@ An Alethe proof is a list of commands.
(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{AletheVerb}
+ \end{AletheVerb}
\caption{Example proof output. Assumptions are
introduced; a subproof renames bound variables; the proof finishes with
instantiation and resolution steps.}
@@ -660,7 +660,7 @@ An Alethe proof is a list of commands.
\begin{figure}[t]
\[
- \begin{array}{r c l}
+ \begin{array}{r c l}
\grNT{proof} &\grRule & \grNT{proof\_command}^{*} \\
\grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
&\grOr & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
@@ -681,10 +681,10 @@ An Alethe proof is a list of commands.
\grNT{context\_annotation} &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{context\_assignment}^{+}\,\textAlethe{)} \\
\grNT{context\_assignment} &\grRule & \textAlethe{(} \,\grNT{sorted\_var}\,\textAlethe{)} \\
& \grOr & \textAlethe{(:=}\, \grNT{symbol}\;\grNT{proof\_term}\,\textAlethe{)} \\
- \end{array}
- \]
- \caption{The proof grammar.}
- \label{fig:grammar}
+ \end{array}
+ \]
+ \caption{The proof grammar.}
+ \label{fig:grammar}
\end{figure}
@@ -840,7 +840,7 @@ expressed as a concrete proof.
system/.style={draw, thin, rounded corners},
}
- \begin{figure}[t]
+ \begin{figure}[t]
\center
\begin{tikzpicture}[node distance=2cm, auto,>=latex', thick,scale=0.8]
\node[solver] (unsat) {\textsf{Unsat mode}};
@@ -926,18 +926,18 @@ no \inlineAlethe{define-fun} commands are issued, and the constants are expanded
\paragraph{Implicit Transformations}
Overall, the following aspects are treated implicitly by Alethe.
\begin{itemize}
- \item Symmetry of equalities that are not top-most equalities in steps with
- non-empty context.
- \item The order of literals in the clauses.
- \item The unfolding of names introduced by
- \inlineAlethe{(!}\,$t$\,\inlineAlethe{:named }\;$s$\,\inlineAlethe{)}.
- \item The removal of other {\smtlib} annotations of the form
- \inlineAlethe{(!}\,$t$\,\dots\,\inlineAlethe{)}.
- \item The unfolding of function symbols introduced by
- \inlineAlethe{define-fun}.\footnote{For {\verit} this is only used when the user
- introduces {\verit} to print Skolem terms as defined functions. User defined
- functions in the input problem are not supported by {\verit} in proof production
- mode.}
+ \item Symmetry of equalities that are not top-most equalities in steps with
+ non-empty context.
+ \item The order of literals in the clauses.
+ \item The unfolding of names introduced by
+ \inlineAlethe{(!}\,$t$\,\inlineAlethe{:named }\;$s$\,\inlineAlethe{)}.
+ \item The removal of other {\smtlib} annotations of the form
+ \inlineAlethe{(!}\,$t$\,\dots\,\inlineAlethe{)}.
+ \item The unfolding of function symbols introduced by
+ \inlineAlethe{define-fun}.\footnote{For {\verit} this is only used when the user
+ introduces {\verit} to print Skolem terms as defined functions. User defined
+ functions in the input problem are not supported by {\verit} in proof production
+ mode.}
\end{itemize}
Alethe proofs contain steps for other aspects that are commonly left implicit, such
@@ -1005,7 +1005,7 @@ It is easy to calculate the context of the first-innermost subproof.
\begin{definition}[Calculated Context]
Let $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$ be
the first-innermost subproof of $P$.
- For $\mathit{start} \leq i < \mathit{end}$, let
+ For $\mathit{start} \leq i < \mathit{end}$, let
$A_1, \dots, A_m$ be the anchors among $C_1, \dots, C_{i-1}$.
The \index{context!calculated}calculated context of $C_i$ is the context
@@ -1039,9 +1039,9 @@ in the subproof. The conditions of each rule are listed in
Section~\ref{apx:rules}.
\begin{definition}[Valid First-Innermost Subproof]
- Let $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$
- be the first-innermost subproof of $P$.
- The subproof is \index{subproof!valid}{\em valid} if
+ Let $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$
+ be the first-innermost subproof of $P$.
+ The subproof is \index{subproof!valid}{\em valid} if
\begin{itemize}
\item all steps $C_i$ with $\mathit{start} < i <
\mathit{end}$ only use premises $C_j$ with $\mathit{start} <
@@ -1049,7 +1049,7 @@ Section~\ref{apx:rules}.
\item all $C_i$ that are steps adhere to the conditions of their
rule under the calculated context of $C_i$,
\item the step $C_{\mathit{end}}$
- adheres to the conditions of its
+ adheres to the conditions of its
rule under the calculated context of $C_{\mathit{start}}$.
\end{itemize}
\end{definition}
@@ -1102,19 +1102,19 @@ Since this proof contains no subproof, it is also $P_{\mathit{last}}$.
\begin{definition}[Well-Formed Proof]
- \label{def:well_formed_proof}
+ \label{def:well_formed_proof}
The Alethe proof $P$ is \index{proof!well-formed}well-formed
if every step uses a unique index and $P_{\mathit{last}}$
contains no anchor or step that uses a concluding rule.
\end{definition}
\begin{definition}[Valid Alethe Proof]
- The proof $P$ is a \index{proof!valid}{\em valid Alethe proof} if
+ The proof $P$ is a \index{proof!valid}{\em valid Alethe proof} if
\begin{itemize}
- \item $P$\, is well-formed,
- \item $P$\, does not contain any step that uses the \proofRule{hole} rule,
+ \item $P$\, is well-formed,
+ \item $P$\, does not contain any step that uses the \proofRule{hole} rule,
\item $P_{\mathit{last}}$ contains a step that has the empty clause as its conclusion,
- \item the first-innermost subproof of every $P_i$, $i < \mathit{last}$ is valid,
+ \item the first-innermost subproof of every $P_i$, $i < \mathit{last}$ is valid,
\item all steps $C_i$ in $P_{\mathit{last}}$ only use premises
$C_j$ in $P_{\mathit{last}}$ with $1 \leq j < i$,
\item all steps $C_i$ in $P_{\mathit{last}}$ adhere to the conditions of their
@@ -1172,8 +1172,8 @@ According to this definition, a metaterm is either a boxed term, a
The annotation $\groundbox{$t$}$ delimits terms from the context, a simple
λ-abstraction is used to express fixed variables, and the
application expresses simulations substitution of $n$ terms.\footnote{
- The box annotation used here is unrelated to the boxes
- within the SMT solver discussed in the introduction.}
+ The box annotation used here is unrelated to the boxes
+ within the SMT solver discussed in the introduction.}
We use $=_{\alpha\beta}$ to denote syntactic equivalence modulo
α-equivalence and β-reduction.
@@ -1296,13 +1296,13 @@ In this section we will address the soundness of concrete Alethe
proofs.
\begin{theorem}[Soundness of Concrete Alethe Proofs]
- \label{thm:sound}
- If there is a valid Alethe proof $P = [C_1, \dots, C_n]$ that has the formulas
- $\varphi_1, \dots, \varphi_m$ as the conclusions of the outermost \proofRule{assume}
- steps, then
- \[
- \varphi_1, \dots, \varphi_m \vDash \bot.
- \]
+ \label{thm:sound}
+ If there is a valid Alethe proof $P = [C_1, \dots, C_n]$ that has the formulas
+ $\varphi_1, \dots, \varphi_m$ as the conclusions of the outermost \proofRule{assume}
+ steps, then
+ \[
+ \varphi_1, \dots, \varphi_m \vDash \bot.
+ \]
\end{theorem}
Here, $\vDash$ represents
@@ -1321,7 +1321,7 @@ We start with simple subproofs with empty contexts and without
nested subproofs.
\begin{lemma}
- \label{lem:sound_subproof}
+ \label{lem:sound_subproof}
Let $P$\, be a proof that contains a valid first-innermost subproof where
$C_{\mathit{end}}$ is a \proofRule{subproof} step. Let
$\psi$ be the conclusion of $C_{\mathit{end}}$.
@@ -1359,22 +1359,22 @@ nested subproofs.
The step $C_{\mathit{end}-1}$ is the last step of the subproof that
does not use a concluding rule.
- At this step we have $V_{\mathit{end}-1} \vDash \psi_{\mathit{end}-1}$.
- Since $C_{\mathit{end}}$ is not an \proofRule{assume} step, the
- set $V_{\mathit{end}-1} = \{\varphi_1, \dots, \varphi_m\}$ contains
- all assumptions in the subproof.
- By the deduction theorem we get
- \[
- \vDash \varphi_1 \land \cdots \land \varphi_m → \psi_{\mathit{end}-1}.
- \]
- This can be transformed into the clause
- \[
- \vDash \neg\varphi_1, \cdots, \neg\varphi_m, l_1, \dots, l_o.
- \]
- where $l_1, \dots, l_o$ are the literals of $\psi_{\mathit{end}-1}$.
- This clause is exactly the conclusion of the
- step $C_{\mathit{end}}$
- according to the definition of the \proofRule{subproof} rule.
+ At this step we have $V_{\mathit{end}-1} \vDash \psi_{\mathit{end}-1}$.
+ Since $C_{\mathit{end}}$ is not an \proofRule{assume} step, the
+ set $V_{\mathit{end}-1} = \{\varphi_1, \dots, \varphi_m\}$ contains
+ all assumptions in the subproof.
+ By the deduction theorem we get
+ \[
+ \vDash \varphi_1 \land \cdots \land \varphi_m → \psi_{\mathit{end}-1}.
+ \]
+ This can be transformed into the clause
+ \[
+ \vDash \neg\varphi_1, \cdots, \neg\varphi_m, l_1, \dots, l_o.
+ \]
+ where $l_1, \dots, l_o$ are the literals of $\psi_{\mathit{end}-1}$.
+ This clause is exactly the conclusion of the
+ step $C_{\mathit{end}}$
+ according to the definition of the \proofRule{subproof} rule.
\end{proof}
\noindent
@@ -1407,7 +1407,7 @@ subproofs with contexts. This is slightly complicated by the
$C_{\mathit{start}}$, and let $\Gamma$ be the calculated context
of $C_{\mathit{start}}$.
$\Gamma' = \Gamma, c_1, \dots, c_n$.
- is the calculated context of the steps in the subproof after
+ is the calculated context of the steps in the subproof after
$C_{\mathit{start}}$.
The step $C_{\mathit{end}}$ is a step
@@ -1461,45 +1461,45 @@ a valid, concrete Alethe proof is sound. That is, we can show
Theorem~\ref{thm:sound}.
\begin{proof}
- Since $P =[C_1, \dots, C_n]$ is valid, all steps that do not use the
- \proofRule{hole} rule adhere to their rule. Since we assume that the
- abstract notation and the rules are sound, we only have to
- worry about the steps using the \proofRule{hole} rule.
- Those should be sound, i.e., for a \proofRule{hole} step with the conclusion
- $\psi$, premises $V$, and context $\Gamma$
- the judgment $V \vDash \Gamma \vartriangleright \psi$ must hold.
-
- Since $P$\, is a valid proof there is a sequence
- $[P_0, \dots, P_{\mathit{last}}]$ as discussed in Section~\ref{sec:alethe:semantic}.
- For $i < \mathit{last}$, $E(P_i) = P_{i+1}$ replaces the
- first-innermost subproof in $P_i$ by a hole with the conclusion
- $\psi$. Furthermore, the context of the introduced hole
- corresponds to the context $\Gamma$ of the start of the subproof.
- Since $P$ is a valid proof, the first-innermost subproof eliminated by $E$ is
- always valid.
- Therefore,
- we can apply Lemma~\ref{lem:sound_subproof}
- or Lemma~\ref{lem:sound_subproof_context} to conclude that the hole introduced
- by $E$ is sound.
-
- Since $P_0$ does not contain any holes, the holes in each proof
- $P_i$ are all introduced by innermost-first subproof elimination.
- Therefore, they are sound. In consequence, all holes in $P_{\mathit{last}}$ are
- sound and we can perform the same
- argument as
- in the proof of Lemma~\ref{lem:sound_subproof} to the proof
- $P_{\mathit{last}}$.
-
- Let $j$ be the index of the step in $P_{\mathit{last}}$ that concludes
- with the empty clause.
- Let $\mathit{start} = 1$
- and $\mathit{end} = j$ in the argument of Lemma~\ref{lem:sound_subproof}.
- This shows that $V \vDash \bot$, where $V$ is the
- conclusion of the \proofRule{assume} steps in the sublist $[C_1, \dots, C_j]$
- of $P_{\mathit{last}}$. We can weaken
- this by adding the conclusions of the \proofRule{assume} steps in
- $[C_j, \dots, C_n]$ of $P_{\mathit{last}}$
- to get $\varphi_1, \dots, \varphi_m \vDash \bot$.
+ Since $P =[C_1, \dots, C_n]$ is valid, all steps that do not use the
+ \proofRule{hole} rule adhere to their rule. Since we assume that the
+ abstract notation and the rules are sound, we only have to
+ worry about the steps using the \proofRule{hole} rule.
+ Those should be sound, i.e., for a \proofRule{hole} step with the conclusion
+ $\psi$, premises $V$, and context $\Gamma$
+ the judgment $V \vDash \Gamma \vartriangleright \psi$ must hold.
+
+ Since $P$\, is a valid proof there is a sequence
+ $[P_0, \dots, P_{\mathit{last}}]$ as discussed in Section~\ref{sec:alethe:semantic}.
+ For $i < \mathit{last}$, $E(P_i) = P_{i+1}$ replaces the
+ first-innermost subproof in $P_i$ by a hole with the conclusion
+ $\psi$. Furthermore, the context of the introduced hole
+ corresponds to the context $\Gamma$ of the start of the subproof.
+ Since $P$ is a valid proof, the first-innermost subproof eliminated by $E$ is
+ always valid.
+ Therefore,
+ we can apply Lemma~\ref{lem:sound_subproof}
+ or Lemma~\ref{lem:sound_subproof_context} to conclude that the hole introduced
+ by $E$ is sound.
+
+ Since $P_0$ does not contain any holes, the holes in each proof
+ $P_i$ are all introduced by innermost-first subproof elimination.
+ Therefore, they are sound. In consequence, all holes in $P_{\mathit{last}}$ are
+ sound and we can perform the same
+ argument as
+ in the proof of Lemma~\ref{lem:sound_subproof} to the proof
+ $P_{\mathit{last}}$.
+
+ Let $j$ be the index of the step in $P_{\mathit{last}}$ that concludes
+ with the empty clause.
+ Let $\mathit{start} = 1$
+ and $\mathit{end} = j$ in the argument of Lemma~\ref{lem:sound_subproof}.
+ This shows that $V \vDash \bot$, where $V$ is the
+ conclusion of the \proofRule{assume} steps in the sublist $[C_1, \dots, C_j]$
+ of $P_{\mathit{last}}$. We can weaken
+ this by adding the conclusions of the \proofRule{assume} steps in
+ $[C_j, \dots, C_n]$ of $P_{\mathit{last}}$
+ to get $\varphi_1, \dots, \varphi_m \vDash \bot$.
\end{proof}
@@ -1561,8 +1561,8 @@ is used. It produces a formula of the form $(\neg \forall \bar
x_n.\,\varphi) \lor \varphi[\bar t_n]$, where $\varphi$ is
a term containing the free variables $\bar x_n$, and for each $i$ the
ground term $t_i$ is a new term with the same sort as $x_i$.\footnote{
- For historical reasons, \proofRule{forall} has a unit clause with a disjunction
- as its conclusion and not the clause $(\neg \forall \bar x_n.\,\varphi), \varphi[\bar t_n]$.
+ For historical reasons, \proofRule{forall} has a unit clause with a disjunction
+ as its conclusion and not the clause $(\neg \forall \bar x_n.\,\varphi), \varphi[\bar t_n]$.
}
The arguments of a \proofRule{forall_inst} step is the list $(x_1 , t_1),
@@ -1575,7 +1575,7 @@ Existential quantifiers are handled by skolemization.
\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$)\footnote{
- This rule also has a unit clause with a disjunction as its conclusion.}
+ This rule also has a unit clause with a disjunction as its conclusion.}
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