Skip to content
Snippets Groups Projects

Backport specification from my PhD thesis

Merged Backport specification from my PhD thesis
devel/thesis-backport into master
Merged Hans-Jörg requested to merge devel/thesis-backport into master
Viewing commit 8efa1d66
Prev Next
Show latest version
1 file
+ 4
− 4
Compare changes
  • Side-by-side
  • Inline
spec/doc.tex
+ 1358
− 1343
@@ -4,94 +4,147 @@
\documentclass{scrartcl}
\usepackage[utf8]{inputenc}
\usepackage{scrlayer-scrpage}
\usepackage{hyperref}
\usepackage{breakurl}
\usepackage{underscore}
\usepackage{siunitx}
\usepackage{ccicons}
\usepackage{mdframed}
\usepackage{etoolbox}
\usepackage[useregional]{datetime2}
\usepackage{tabularx}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{thmtools}
\usepackage{environ}
\usepackage{mathtools}
\usepackage[mathcal]{eucal}
\usepackage{longtable}
\usepackage{stmaryrd}
\usepackage{todonotes}
\usepackage{tikz}
\usepackage{scalerel}
\usepackage{unicode-math}
\usepackage{fontsetup}
\usepackage{minted}
\usemintedstyle{trac}
\usepackage{array}
\usepackage{booktabs}
\renewcommand{\MintedPygmentize}{./highlight.py}
\newminted[AletheVerb]{smt-lib}{}
\newmintinline[inlineAlethe]{smt-lib}{}
\usepackage{cite}
\usepackage{url}
\usepackage[useregional]{datetime2}
\usepackage{xltabular} % Gives us stretchable, breakable tables. for proofs
\usepackage{longtable} % Gives us longtables for proof
\usepackage{environ} % Gives us NewEnviron to define environements with tables
\usepackage{fancyvrb} % Gives us \Verb which can be used in footnotes
\usepackage{amsthm}
\usepackage{thmtools}
\usepackage{ccicons} % Gives us CC icons for title page
\usepackage[nottoc,notlot,notlof]{tocbibind}
\usepackage{imakeidx}
\makeindex
\makeindex[name=rules,options= -s rule_index_style.ist]
% We provide a command that discards the argument to the index. This
% allows us to do the sectioning of the index manually and give different
% sectin levels to the rule index and the overall index
\newcommand\indexsection[1]{}
\indexsetup{level=\indexsection,firstpagestyle=headings,noclearpage}
% Must come after imakeidx
\usepackage[hidelinks=true]{hyperref}
\usepackage{breakurl}
\usepackage{tikz}
\usetikzlibrary{tikzmark,positioning}
\usetikzlibrary{shapes,arrows,fit, scopes}
\usetikzlibrary{arrows.meta}
\usetikzlibrary{svg.path}
\usepackage{bussproofs}
\EnableBpAbbreviations
\usepackage{amsthm}
\usepackage[english]{babel}
\nonfrenchspacing
\usepackage{empheq}
\usepackage{longfbox}
\usepackage[final,tracking=true,kerning=true,spacing=true,stretch=10,shrink=10]{microtype}
\usepackage[final,tracking=true,stretch=10,shrink=10]{microtype}
\microtypecontext{spacing=nonfrench}
% Used for Aletheia in greek
%\newfontfamily\greekfont[Script=Greek, Scale=MatchUppercase, Ligatures=TeX]{CMU Serif}
\hyphenation{Isa-belle Nieuw-en-huis meta-logic multi-set multi-sets non-unit Mini-Sat}
% ========================================
% Commands
% ========================================
% Environment for discussion, conditional
\ifdef{\nocomments}
{\NewEnviron{comment}[1]{}}
{\global\mdfdefinestyle{commentstyle}{%
frametitlebackgroundcolor=gray!20,%
frametitlefont={\sffamily\bfseries},%
linecolor=gray!90,%
linewidth=1pt,%
\newcommand\smtlib{SMT-LIB}
\newcommand\cdclt{CDCL(T)}
\newcommand\tool[1]{\textsf{#1}}
\newcommand\tactic[1]{\texttt{#1}}
\newcommand\verit{\tool{veriT}}
\newcommand\cvcfive{\tool{cvc5}}
\newcommand\cvcfour{\tool{CVC4}}
\newcommand\isabelle{\tool{Isabelle/HOL}}
\newcommand\lsymb[1]{\mathbf{#1}}
\DeclareMathOperator*{\subst}{subst}
\DeclareMathOperator*{\reify}{reify}
\newcommand\groundbox[1]{\boxed{#1}}
% Proofs
\newcommand\textAlethe[1]{\texttt{#1}}
\newcommand\ctxsep{$\vartriangleright$}
\newcommand\spctxsep{\multicolumn{1}{|c}{\ctxsep}}
\newcommand\spctx[1]{\multicolumn{1}{|c}{#1}}
\newcommand\spsep{\cline{2-4}}
% Empty lines with dots
\newcommand\aletheLine{ & & $\vdots$ & \\}
\newcommand\aletheLineB{& \multicolumn{1}{|c}{} & $\vdots$ & \\}
% with subproof line to the left
\newcommand\aletheLineS {& & & $\vdots$ & \\}
\newcommand\aletheLineSB{& \multicolumn{1}{|c}{} & & $\vdots$ & \\}
% Tables for proofs
\newcolumntype{Y}{>{\centering\arraybackslash}X}
\newcommand{\ruleTypeImpl}[1]{%
\microtypesetup{tracking=false}\textsf{#1}\microtypesetup{tracking=true}%
}
\NewEnviron{comment}[1]{%
\begin{mdframed}[style=commentstyle, frametitle={\small Comment by #1}]%
\def\ruleType#1{\ruleTypeImpl{\detokenize{#1}}} % non linked rule (for examples)
\def\proofRule#1{\hyperref[rule:\detokenize{#1}]{\ruleTypeImpl{\detokenize{#1}}}} % linked rule
%\newcommand{\ruleref}[1]{\ruleType{\nameref{rule:#1}}~(\ref{rule:#1})}
\def\ruleref#1{\hyperref[rule:\detokenize{#1}]{\ruleTypeImpl{\detokenize{#1}}}~(\ref{rule:\detokenize{#1}})} % for the rule tables
\NewEnviron{Alethe}{%
\renewcommand\spsep{\cline{2-4}}
\setlength{\arrayrulewidth}{0.8pt}
\addtolength{\tabcolsep}{-4pt}
\begin{xltabular}{\linewidth}{l c Y r}
\BODY
\end{xltabular}
\addtolength{\tabcolsep}{+4pt}
}
\NewEnviron{AletheS}{%
\renewcommand\spsep{\cline{2-5}}
\setlength{\arrayrulewidth}{0.8pt}
\addtolength{\tabcolsep}{-4pt}
\begin{xltabular}{\linewidth}{l l c Y r}
\BODY
\end{mdframed}%
}}
\end{xltabular}
\addtolength{\tabcolsep}{+4pt}
}
\newcounter{ProofRuleCounter}
% These avoid the xltabular environment. While xltabular can break on pages
% it seems to interact badly with the RuleDescription enviornment.
\NewEnviron{AletheX}{%
\renewcommand\spsep{\cline{2-4}}%
\setlength{\arrayrulewidth}{0.8pt}%
\addtolength{\tabcolsep}{-4pt}%
\noindent
\begin{tabularx}{\linewidth}{l c Y r}
\BODY
\end{tabularx}
\addtolength{\tabcolsep}{+4pt}
}
\NewEnviron{AletheXS}{%
\renewcommand\spsep{\cline{2-5}}%
\setlength{\arrayrulewidth}{0.8pt}%
\addtolength{\tabcolsep}{-4pt}%
\noindent
\begin{tabularx}{\linewidth}{l l c Y r}
\BODY
\end{tabularx}
\addtolength{\tabcolsep}{+4pt}
}
% Environment for proof-rules
\declaretheoremstyle[
bodyfont=\normalfont,%
headfont=\sffamily\bfseries,%
notebraces={(}{)},%
headformat={\NAME~\NUMBER \NOTE},%
]{simple}
\theoremstyle{simple}
\declaretheorem[name=Example,style=simple]{exmp}
\declaretheorem[name=Example,parent=ProofRuleCounter,style=simple]{rule-example}
\newcommand\currule{\proofRule{none}}
\newcounter{ProofRuleCounter}
\newcommand\currule{\textbf{ERROR}}
\declaretheoremstyle[
headfont=\sffamily\bfseries,%
@@ -105,202 +158,68 @@ break
\declaretheorem[name=Rule,style=proof-rule-style,sibling=ProofRuleCounter]{inner-rule}
\newenvironment{proof-rule}[2]{%
\begin{inner-rule}[#1]\label{rule:#1}
\renewcommand\currule{\proofRule{#1}}%
}{%
\end{inner-rule}
\makeatletter
\newcommand{\ruleparagraph}{%
\@startsection{paragraph}{4}%
{\z@}{1ex \@plus 0.5ex \@minus .2ex}{-1em}%
{\normalfont\normalsize\bfseries}%
}
\makeatother
% Proof rules
\newcommand{\ruleType}[1]{\microtypesetup{tracking=false}\texttt{#1}\microtypesetup{tracking=true}}
\newcommand{\ruleref}[1]{\ruleType{\nameref{rule:#1}}~(\ref{rule:#1})}
%\newcommand{\proofRule}[1]{\microtypesetup{tracking=false}\texttt{#1}\microtypesetup{tracking=true}}
\newcommand{\proofRule}[1]{\ruleType{\nameref{rule:#1}}}
% == Theorem environments ==
\newcommand{\isaTac}[1]{\texttt{#1}}
\newcommand\IfThenElse[3]{\ensuremath{\mathit{if}~#1~\mathit{then}~#2~\mathit{else}~#3}}
\newcommand{\proofsep}{\;\vartriangleright\;}
\newcommand{\proofsepI}{\;\blacktriangleright\;}
\newcommand{\smtinline}[1]{\mintinline{smtlib2.py -x}{#1}}
\newcommand{\plLine}{&&\vdots&}
\newcolumntype{Y}{>{\centering\arraybackslash\(}X<{\)}}
\newcolumntype{L}{>{\(}l<{\)}}
\newcolumntype{R}{>{\(}r<{\)}}
\NewEnviron{plList}{%
\par\noindent%
\centering\begin{tabularx}{\textwidth}{L@{\,}RYR}%
\BODY
\end{tabularx}\\%
}
\NewEnviron{plSubList}{%
\setlength{\arrayrulewidth}{1pt}%
\par\noindent%
\centering\begin{tabularx}{\textwidth}{|L@{\,}RYR}%
\BODY
\hline
\end{tabularx}\\%
}
\NewEnviron{RuleDescription}[1]{%
\renewcommand\currule{\proofRule{#1}}
\index[rules]{#1}
\NewEnviron{plContainer}{% The following line break is important!
\begin{inner-rule}[\detokenize{#1}]\label{rule:#1}
\parbox{\textwidth}{%
\setlength{\topsep}{0.2\baselineskip}%
\begin{center}
\BODY
\end{center}
}\leavevmode\newline%
\BODY
\end{inner-rule}
}
\NewEnviron{plListEq}{%
\[\begin{array}{r@{\,}lcr}%
\BODY
\end{array}\]%
}
\theoremstyle{definition}
\newtheorem{RuleExample}{Example}[inner-rule]
\NewEnviron{plListEqAlgn}{%
\[\begin{array}{r@{\,}lr@{\,}lr}%
\BODY
\end{array}\]%
}
% TODO: synchronize colors!
\definecolor{SmtBlue}{HTML}{00007f}
\definecolor{SmtGreen}{HTML}{3b7f31}
\definecolor{SmtStepId}{HTML}{3b7f31}
\NewEnviron{plCompact}{%
\begingroup\abovedisplayskip=0pt \belowdisplayskip=0pt%
\begin{align*}%
\BODY
\end{align*}%
\endgroup
}
\newcommand{\grNT}[1]{\textcolor{SmtGreen}{\langle\texttt{#1}\rangle}}
\newcommand{\grT}[1]{\textcolor{SmtBlue}{\texttt{#1}}}
\newcommand{\grRule}{≔}
\newcommand{\grOr}{|}
\newtheorem{example}{Example}
\newtheorem{theorem}{Theorem}[example]
\newtheorem{lemma}{Lemma}[example]
\newtheorem{definition}{Definition}[example]
\newtheorem{seppara}{}
% == Commands for Grammar ==
\definecolor{SmtBlue}{HTML}{00007f}
\definecolor{SmtGreen}{HTML}{3b7f31}
\newcommand{\grNT}[1]{\textcolor{SmtGreen}{\langle\texttt{#1}\rangle}}
\newcommand{\grT}[1]{\textcolor{SmtBlue}{\texttt{#1}}}
\newcommand{\grRule}{\quad\Coloneqq\quad}
\newcommand{\grOr}{\quad|\quad}
\newcommand\vvthinspace{\kern+0.041667em}
\newcommand\vthinspace{\kern+0.083333em}
\newcommand\negvthinspace{\kern-0.083333em}
\newcommand\negvvthinspace{\kern-0.041667em}
\newcommand{\limp}{\rightarrow}
\newcommand\metafun[1]{\ensuremath{\mathit{#1}}}
\newcommand\sort[1]{\mathsf{#1}}
\newcommand\sym[1]{\mathsf{#1}}
\newcommand\GAMMA{\mathrm{\Gamma}}
\newcommand\emptyctx{\varnothing}
\newcommand\substname{\metafun{subst}}
\newcommand\subname{\metafun{repl}}
\newcommand\reify{\metafun{reify}}
\newcommand\subst[1]{\substname(#1)}
\newcommand\substapp[2]{#1(#2)}
\newcommand\judgei[1]{\proofsep#1}
\newcommand\judge[2]{#1\;\vthinspace\proofsep#2}
\newcommand\judgealti[1]{\proofsepI#1}
\newcommand\judgealt[2]{#1\;\vthinspace\proofsepI#2}
\newcommand\eqa{=_{\alpha}}
\newcommand\eqb{=_{\beta}}
\newcommand\eqab{=_{\alpha\beta}}
\newcommand\Refl{\textsc{Refl}}
\newcommand\Taut{\textsc{Taut}}
\newcommand\Tautof[1]{\Taut\smash{\ensuremath{_{#1}}}}
\newcommand\TautT{\Tautof{\mathcal T}}
\newcommand\Trans{\textsc{Trans}}
\newcommand\Cong{\textsc{Cong}}
\newcommand\Bind{\textsc{Bind}}
\newcommand\Sko{\textsc{Sko}}
\newcommand\SkoEx{\Sko\smash{\ensuremath{_{\,\exists}}}}
\newcommand\SkoAll{\Sko\smash{\ensuremath{_{\,\forall}}}}
\newcommand\Choicename{\varepsilon}
\newcommand\Choice[2]{\Choicename #1.\>#2}
\newcommand\All[2]{\forall #1.\;#2}
\newcommand\Ex[2]{\exists #1.\;#2}
\newcommand\Not{{\lnot}\,}
\newcommand\Let{\textsc{Let}}
\newcommand\FV[1]{\metafun{FV}(#1)}
\newcommand\BV[1]{\metafun{BV}(#1)}
\newcommand\var[1]{\metafun{V}(#1)}
\newcommand\intro[1]{\metafun{intr}(#1)}
\newcommand\axiomstrut{\vrule height 1.25ex depth 0pt width 0pt} %% TYPESETTING
\DeclareDocumentCommand{\enum}{ O{n} m O{,} O{} O{1}}{#2_#5#4#3\dots #3#2_{#1}#4}
% == Tikz Setup ==
\usetikzlibrary{tikzmark,positioning}
\usetikzlibrary{shapes,arrows,fit, scopes}
\usetikzlibrary{arrows.meta}
\usetikzlibrary{svg.path}
\tikzstyle{every picture}+=[remember picture]
\tikzset{
std/.style={draw, thin, fill=blue!20},
system/.style={draw, thin, fill=red!20, rounded corners},
code/.style={red, inner sep=0.15cm, text=black, draw, thick, rounded corners, fill=red!20}
}
% Hack to make line numbers less ugly
\renewcommand{\theFancyVerbLine}{\footnotesize{\arabic{FancyVerbLine}}\hspace{-0.5em}}
% == Theorem environments ==
\newpairofpagestyles{titlestyle}{
\ifdef{\nocomments}
{\ofoot{Version \input{|"./version.sh"}\unskip . Typeset on {\today}.}}%
{\ofoot{Version \input{|"./version.sh"}with comments. Typeset on {\today}.}}%
\ofoot{Version \input{|"./version.sh"}\unskip . Typeset on {\today}.}%
\ifoot{\ccby}%
}
\renewcommand*{\titlepagestyle}{titlestyle}
\setkomafont{publishers}{\small}
% ========================================
% Document
% ========================================
\title{The Alethe Proof Format}
\subtitle{A Speculative Specification and Reference}
\subtitle{An Evolving Specification and Reference}
\author{Haniel Barbosa\textsuperscript{1}
\and Mathias Fleury\textsuperscript{2}
\and Pascal Fontaine\textsuperscript{3}
\and Hans-Jörg Schurr\textsuperscript{4}}
\date{}
\publishers{
\textsuperscript{1} Universidade Federal de Minas Gerais\\
\textsuperscript{2} Johannes Kepler University Linz\\
\textsuperscript{3} Université de Liège\\
\textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy\\
\textsuperscript{1} Universidade Federal de Minas Gerais, Brazil\\
\textsuperscript{2} Albert-Ludwig-Universität Freiburg, Germany\\
\textsuperscript{3} Université de Liège, Belgium\\
<<<<<<< HEAD
\textsuperscript{4} University of Iowa, Iowa City, USA\\
=======
\textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy, France\\
>>>>>>> dc5a965 (Move spec to "doc.tex" and update Makefile/pipeline)
}
\makeatletter
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
\makeatother
\begin{document}
@@ -318,10 +237,10 @@ format. The language also includes a flexible mechanism to reason
about bound variables which allows fine-grained preprocessing proofs.
%
On the other side, the rules are structured around resolution and the
introduction of theory lemmas, in the same way as CDCL($\mathcal{T}$)-based SMT
introduction of theory lemmas, in the same way as CDCL(T)-based SMT
solvers.
The specification is speculative in the sense that it is not yet
The specification is not yet
cast in stone, but it will evolve over time. It emerged from a list
of proof rules used by the SMT solver veriT collected in a document
called ``Proofonomicon''. Following the fate presupposed by its name,
@@ -352,916 +271,666 @@ implement support for Alethe into their own tools. Please
get in touch!
\bigskip
\hspace*{\fill}The authors in the summer of 2021.
\hspace*{\fill}The authors.
\end{abstract}
\section{Introduction}
This document is a reference of the Alethe proof format. Alethe is
This document is a reference of the
Alethe\footnote{Alethe is a genus of small birds that occur in West Africa~\cite{wp:alethe}.
The name was chosen because it
resembles the Greek word {αλήθεια} (alítheia) -- truth.} proof format. Alethe is
designed to be a flexible format to represent unsatisfiability proofs
generated by SMT solvers. Alethe proofs can be consumed by other systems,
such as interactive theorem provers or proof checkers. The overall design
follows a few core concepts, such as a natural-deduction style structure
and rules generating and operating on ground first-order clauses.
such as interactive theorem provers or proof checkers. The design
is based on natural-deduction style structure
and rules generating and operating on first-order clauses.
%
The Alethe calculus consists of two parts: the proof language based on
SMT-LIB and a collection of proof rules.
Section~\ref{sec:language} introduces the language. First as an abstract language,
then as a concrete syntax.
The Alethe proof format consists of two parts: the proof
language based on {\smtlib} and a collection of proof rules.
Section~\ref{sec:alethe:language} introduces the language. First as an
abstract language, then as a concrete syntax.
Section~\ref{sec:alethe:semantics} then discusses an abstract procedure
to check Alethe proofs. This abstract checking procedure specifies
the semantics of Alethe proofs.
%
Section~\ref{sec:rules-generic} discusses the core
concepts behind the Alethe proof rules.
The Alethe proof rules are discussed in two sections.
First, Section~\ref{sec:alethe:rules-generic} discusses the core
concepts behind the rules.
%
At the end of the document Section~\ref{sec:rules} presents a list of
all proof rules used by SMT solvers supporting Alethe.
Second, Section~\ref{apx:rules} presents a list of
all proof rules currently used by {\verit}.
Alethe follows a few core design principles. First, proofs should
be easy to understand by humans to ensure working with Alethe proofs
is effortless. Second, the logic of the format should directly
correspond to the logic used by the solver. Since many solvers use the
SMT-LIB logic, Alethe also uses this logic. Third, the language should
be uniform for all theories used by SMT solvers. With the expectation
of clauses for propositional reasoning, there is dedicated syntax for
any logic
The semantics (Section~\ref{sec:semantic}) and concrete syntax
(Section~\ref{sec:syntax}) are based on the SMT-LIB~\cite{SMTLIB}
format, widely used as the input and output standard for SMT solvers.
%
Hence, Alethe's base logic is the many-sorted first-order logic of SMT-LIB. This
document assumes the reader is familiar with the SMT-LIB standard.
The format is currently used by the SMT solver veriT~\cite{verit}. If requested
by the user, veriT outputs a proof if it can deduce that the input problem is
unsatisfiable. In proof production mode, veriT supports the theory of
is easy. Second, the language of the format should directly
correspond to the language used by the solver. Since many solvers use the
{\smtlib} language, Alethe also uses this language.
Therefore, Alethe's base logic is the many-sorted first-order logic of {\smtlib}.
Third, the format should
be uniform for all theories used by SMT solvers. With the exception
of clauses for propositional reasoning, there is no dedicated syntax for
any theory.
The Alethe format was originally developed for the SMT solver {\verit}. If requested
by the user, {\verit} outputs a proof if it can deduce that the input problem is
unsatisfiable. In proof production mode, {\verit} supports the theory of
uninterpreted functions, the theory of linear integer and real arithmetic, and
quantifiers.
The SMT solver {\cvcfive}~\cite{barbosa-2022} (the successor of
{\cvcfour}) supports Alethe experimentally as one of its multiple proof
output formats.
%
The Alethe proofs can be reconstructed by the \texttt{smt} tactic
of the proof assistant Isabelle/HOL~\cite{fleury-2019,schurr-2021}, as well as
by SMTCoq in the proof assistant Coq~\cite{SMTCoq}.
Alethe proofs can be reconstructed by the \tactic{smt} tactic of
the proof assistant {\isabelle}~\cite{fleury-2019,schurr-2021}.
The \tool{SMTCoq} tool can
reconstruct an older version of the format in the
proof assistant \tool{Coq}~\cite{SMTCoq}. An effort to update the
tool to the latest version of Alethe is ongoing.
%
The SMT solver cvc5 (the successor of CVC4~\cite{CVC4}) supports Alethe
experimentally as one of its multiple proof output formats.
Furthermore, \tool{Carcara} is an experimental
high-performance \index{proof checker}proof checker written in Rust.\footnote{Available at
\url{https://github.com/ufmg-smite/carcara}.}
In addition to this reference, the proof format has been discussed in past
publications which provide valuable background information. The core of
publications, which provide valuable background information. The core of
the format goes back to 2011 when two publications at the PxTP workshop
outlined the fundamental ideas behind the format~\cite{besson-2011}
and proposed rules for quantifier instantiation~\cite{deharbe-2011}.
%
More recently the format has gained support for reasoning typically used for
processing, such as Skolemization, substitutions, and other manipulations of
More recently, the format has gained support for reasoning typically used for
processing, such as skolemization, substitutions, and other manipulations of
bound variables~\cite{barbosa-2019}.
\subsection{Notations}
The notation used in this document is similar to the notation
used by the SMT-LIB standard. The Alethe proof format uses
the SMT-LIB logic. Since the SMT-LIB language is based on
S-expressions\index{S-expression}, SMT-LIB formulas are written using
a λ-calculus style. That is, instead of $f(1,2)$, we write $(f\,1\,2)$.
However, connectives that are usually written using infix notation, also
use infix notation here. That is, we write $t_1 \lor t_2$, not
$(\lor\,t_1\,t_2)$.
We use $x, y, z$ to indicate variables,
$f, g$ for functions, and $P, Q$ for predicates (functions with co-domain
sort $\lsymb{Bool}$. To indicate terms we use $t, u$ and to indicate
formulas (terms of sort $\lsymb{Bool}$) we use $\varphi, \psi$.
To distinguish syntactic equality and the SMT-LIB equality predicate,
we write $=$ for the former, and $≈$ for the latter.
We will write pre-defined SMT-LIB symbols, such as sorts and functions,
in bold (e.g., $\lsymb{Bool}$, $\lsymb{ite}$).
We will use $θ$ to denote a substitution\index{substitution}.
The notation $[x₁ ↦ t₁, …, x_n ↦ t_n]$ denotes the substitution
that maps $x_i$ to $t_i$ for $1 ≤ i ≤ n$ and corresponds to the
identity function for all other variables.
%
If $θ$ and $η$ are two
substitutions, then $θη$ denotes the result of first applying $θ$
and then $η$ (i.e., $η(θ(.))$). A substitution can naturally be extended
to a function that maps terms to terms by replacing the occurrences of
free variables.
%
The application of a substitution $θ$ to a term $t$ (i.e., $θ(t)$)
is capture-avoiding; bound variables in $t$ are renamed as necessary.
We write $t[u]$ for a term that contains the term $u$ as a subterm. If $u$
is subsequently replaced by a term $v$, we write $t[v]$ for the
new term.
%
We also use this notation with multiple terms.
%
The notation $t[u_1, \dots, u_n]$ stands for a term may contain the
pairwise distinct terms $u_1, \dots, u_n$.
%
Then, $t[s_1,\dots, s_n]$ is the respective term where the
variables $u_1,\dots, u_n$ are
simultaneously replaced by $s_1,\dots, s_n$. Usually, $u_1, \dots, u_n$ will
be variables.
Note that we will introduce the Alethe specific notation to write proof steps
in the following sections.
\section{The Alethe Language}
\label{sec:language}
\label{sec:alethe:language}
This section provides an overview of the core concepts of the Alethe
language and also introduces some notation used throughout this document.
While the next section provides a formal definition of the language,
this overview of the core concepts should be helpful for
practitioners.
This section provides an overview of the core concepts of the
\index{Alethe}Alethe language and also introduces some notation used
throughout this chapter.
The section first introduces an abstract notation to write Alethe proofs.
Then, it introduces the concrete, {\smtlib}-based syntax. Finally,
we show how a concrete Alethe proof can be checked.
\paragraph{Multi-Sorted First-Order Logic.}
\begin{example}
The following example shows a simple Alethe proof
expressed in the abstract notation used in this document.
It uses quantifier instantiation and resolution to show a contradiction.
The paragraphs below describe the concepts necessary to
understand the proof step by step.
Many SMT solvers use the SMT-LIB language~\cite{SMTLIB} as both its
input and output language and Alethe builds on this language.
%
This includes its multi-sorted first-order logic. The available sorts depend on
the selected SMT-LIB theory/logic as well as on those defined by the user, but a
distinguished $\mathbf{Bool}$ sort is always available.
\begin{Alethe}
1.& \ctxsep & $\forall x.\, (P\,x)$ & $ \proofRule{assume}$ \\
2.& \ctxsep & $\neg (P\,a) $ & $ \proofRule{assume}$ \\
3.& \ctxsep & $\neg (\forall x.\, (P\,x)) \lor (P\,a)$ & $\proofRule{forall_inst}\,[(x, a)]$ \\
4.& \ctxsep & $\neg (\forall x.\, (P\,x)), (P\,a)$ & $ (\proofRule{or}\:3)$ \\
5.& \ctxsep & $\bot $ & $ (\proofRule{resolution}\: 1, 2, 4)$ \\
\end{Alethe}
\end{example}
We use $\sigma$ to denote substitutions and $t\sigma$ to denote the application
of the substitution on the term $t$. To denote the substitution which maps $x$
to $t$ we write $\{x\mapsto t\}$
\paragraph{Many-Sorted First-Order Logic.}
Alethe builds on the {\smtlib} language.
%
The notation $t[\bar x_n]$ stands for a term that may depend on distinct
variables $\bar x_n$.
This includes its many-sorted first-order logic.
The available sorts depend on
the selected {\smtlib} theory/logic as well as on those defined by the user, but the
distinguished $\lsymb{Bool}$ sort is always available.
%
$t[\bar s_n]$ is the respective term where the variables $\bar x_n$ are
simultaneously substituted by $\bar s_n$.
In addition to the multi-sorted first-order logic used by SMT-LIB,
Alethe also uses Hilbert's choice operator $\varepsilon$.
However, Alethe also extends this logic with Hilbert's choice
operator $\varepsilon$.
%
The term $\varepsilon x.\, \varphi[x]$ stands for a value $v$,
The term $\varepsilon x.\, \varphi[x]$ stands for a value $v$
such that $\varphi[v]$ is true if such a value exists. Any value is
possible otherwise. Alethe requires that $\varepsilon$ is functional
with respect to logical equivalence: if for two formulas $\varphi$, $\psi$
that contain the free variable $x$, it holds that
$(\forall x.\,\varphi\leftrightarrow\psi)$,
then $(\varepsilon x.\, \varphi)\simeq (\varepsilon x.\, \psi)$ must also hold.
As a matter of notation, we use the symbols $x$, $y$, $z$ for variables,
$f$, $g$, $h$ for functions, and $P$, $Q$ for predicates, i.e.,
functions with result sort $\mathbf{Bool}$. The symbols $r$, $s$, $t$,
$u$ stand for terms. The symbols $\varphi$, $\psi$ denote formulas, i.e.,
terms of sort $\mathbf{Bool}$.
%
We use $=$ to denote syntactic equality and $\simeq$ to denote the sorted
equality predicate.
To simplify the
notation we will omit the sort of terms when possible.
$(\forall x.\,\varphi ≈ \psi)$,
then $(\varepsilon x.\, \varphi)\approx(\varepsilon x.\, \psi)$ must also hold.
Note that choice terms can only appear in Alethe proofs, not in {\smtlib} problems.
%\end{seppara}
\begin{example} The following example shows a simple Alethe proof
expressed in the abstract calculus used in this document.
It uses quantifier instantiation and resolution to show a contradiction.
The sections below step-by-step describe the concepts necessary to
understand the proof intuitively.
\begin{plContainer}
\begin{plList}
\proofsep& 1.& \forall x.\, P(x) &\proofRule{assume}\\
\proofsep& 2.& \neg P(a) &\proofRule{assume}\\
\proofsep& 3.& \neg (\forall x.\, P(x)) \lor P(a) &\proofRule{forall_inst}\,[(x, a)]\\
\proofsep& 4.& \neg (\forall x.\, P(x)), P(a) &(\proofRule{or}\:3)\\
\proofsep& 5.& \bot &(\proofRule{resolution}\: 1, 2, 4)\\
\end{plList}
\end{plContainer}
\paragraph{Steps.}
A \index{proof}proof in the Alethe language is an indexed list of \index{step}steps.
To mimic the concrete syntax of Alethe proofs, proof steps in the
abstract notation have the form
\end{example}
\begin{AletheS}
$i$.& $c_1,\,\dots,\, c_j$ & \ctxsep &
$l_1,\dots ,l_k$ & $(\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]$ \\
\end{AletheS}
\paragraph{Steps.}
A proof in the Alethe language is an indexed list of steps.
To mimic the concrete syntax we write a step in the form
\begin{plListEq}
c_1,\,\dots,\, c_k &\proofsep i. & \varphi_1,\dots ,\varphi_l &
(\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]
\end{plListEq}
\noindent
Each step has a unique index \(i \in \mathbb{I}\), where \(\mathbb{I}\) is a countable
infinite set of valid indices. In the concrete syntax all SMT-LIB symbols are
Each step has a unique index $i \in \mathbb{I}$, where $\mathbb{I}$ is a countable
infinite set of valid indices. In the concrete syntax all {\smtlib} symbols are
valid indices, but for examples we will use natural numbers.
%
Furthermore, a step has a clause \(\varphi_1,
\dots ,\varphi_l\) as its conclusion. If a step has the empty clause
as its conclusion (i.e., \(l = 0\)) we will write \(\bot\). While this
muddles the water a bit with regards to steps which have the unit clause
with the unit literal \(\bot\) as their conclusion, it simplifies the
Furthermore, $l_1, \dots ,l_k$ is a clause with the literals
$l_i$. It is the conclusion of the step. If a step has the empty clause
as its conclusion (i.e., $k = 0$) we write $\bot$. While this
muddles the water a bit with regard to steps which have the unit clause
with the unit literal $\bot$ as their conclusion, it simplifies the
notation. We will remark on the difference if it is relevant. The rule
name \ruleType{rule} is taken from a set of possible proof
rules (Section~\ref{sec:rules}).
rules (see Section~\ref{apx:rules}).
Furthermore, each step has a possibly empty set of premises $\{p_1,
\dots, p_n\}$ with $p_i\in\mathbb{I}$,
\dots, p_n\} \subseteq \mathbb{I}$,
and a rule-dependent and possibly
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,
acyclic graph. If the list of premises is empty, we will drop the
parentheses around the proof rule.
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. The list \(c_1, \dots, c_k\) is
the \emph{context} of the step. Contexts have their own section below.
of the arguments is rule specific. The list $c_1, \dots, c_j$ is
the \index{context}{\em context} of the step. Contexts are discussed below.
Every proof ends with a step that has the empty clause as the conclusion
and an empty context.
The example above consists of five steps. Step 4 and 5 use premises.
Since step 3 introduces a tautology, it uses no premises. However,
it uses arguments to express the substitution $x\mapsto a$ used to instantiate
the quantifier. Step 4 translates the disjunction into a clause.
and an empty context. The list of proof rules
in Section~\ref{apx:rules}
also uses
this notation to define the proof rules.
The example above consists of five steps. Step~4 and~5 use premises.
Since step~3 introduces a tautology, it uses no premises. However,
it uses arguments to express the substitution $[x\mapsto a]$ used to instantiate
the quantifier. Step~4 translates the disjunction into a clause.
In the example above, the contexts are all empty.
\paragraph{Assumptions.}
A \proofRule{assume} step introduces a term as an assumption. The
proof starts with a number of \ruleType{assume} steps. Each such step
corresponds to an input assertion. Additional assumptions can be introduced
too. In this case each assumption must be discharged with an appropriate
An \proofRule{assume} step introduces a term as an
\index{assumption}assumption. The proof starts with a number of
\proofRule{assume} steps. Each such step corresponds to an input
assertion. Within a subproof, additional assumptions can be introduced
too. In this case, each assumption must be discharged with an appropriate
step. The rule \proofRule{subproof} can be used to do so. In the concrete
syntax \ruleType{assume} steps have a dedicated command $\grT{assume}$ to
clearly distinguish them from normal steps that use the $\grT{step}$ command
(see Section~\ref{sec:syntax}).
syntax, \proofRule{assume} steps have a dedicated command \inlineAlethe{assume}
to clearly distinguish them from normal steps that use the \inlineAlethe{step}
command (see~Section~\ref{sec:alethe:syntax}).
The example above uses two assumptions which are introduced in the first
two steps.
\paragraph{Subproofs and Lemmas.}
Alethe uses subproofs to prove lemmas and to create and manipulate the context.
%
To prove lemmas, a subproof can
introduce local assumptions. The \proofRule{subproof} \emph{rule} discharges the
To prove \index{lemma}lemmas, a \index{subproof}subproof can
introduce local assumptions. The \proofRule{subproof} {\em rule} discharges the
local assumptions.
From an
assumption $\varphi$ and a formula $\psi$ proved by intermediate steps
from $\varphi$, the \proofRule{subproof} rule deduces the clause $\neg \varphi,
assumption $\varphi$ and a formula $\psi$ proved
from $\varphi$, the \proofRule{subproof} rule deduces the clause $\neg \varphi,
\psi$ that discharges the local assumption $\varphi$.
%
A \proofRule{subproof} step can not use premise from a subproof nested within the current subproof.
\begin{comment}{Mathias Fleury}
There are two ways to export one element from the subproof:
\begin{itemize}
\item rely on the order and take the last one
\item add an explicit :premises in the conclusion stop to give the exported step
\end{itemize}
\end{comment}
A \proofRule{subproof} step cannot use a premise from a subproof nested
within the current subproof.
Subproofs are also used to manipulate the context.
As the example below shows, within this document we denote subproofs by a
frame around the rules within the subproof.
\begin{example} This example show a contradiction proof for the
formula \((2 + 2) \simeq 5\). The proof uses a subproof to prove the
lemma \(((2 + 2) \simeq 5) \Rightarrow 4 \simeq 5\).
\begin{plContainer}
\begin{plList}
\proofsep& 1.& (2 + 2) \simeq 5 &\proofRule{assume}\\
\end{plList}
\begin{plSubList}
\proofsep& 2.& (2 + 2) \simeq 5 &\proofRule{assume}\\
\proofsep& 3.& (2 + 2) \simeq 4 &\proofRule{sum_simplify}\\
\proofsep& 4.& 4 \simeq 5 &(\proofRule{trans}\;1, 2)\\
\end{plSubList}
\begin{plList}
\proofsep& 5.& \neg((2 + 2) \simeq 5), 4 \simeq 5 &\proofRule{subproof}\\
\proofsep& 6.& (4 \simeq 5)\leftrightarrow \bot &\proofRule{eq_simplify}\\
\proofsep& 7.& \neg((4 \simeq 5)\leftrightarrow \bot), \neg(4\simeq 5), \bot &\proofRule{equiv_pos2}\\
\proofsep& 8.& \bot &(\proofRule{resolution}\; 1, 5, 7, 8)\\
\end{plList}
\end{plContainer}
As the example below shows, the abstract notation denotes subproofs by a
frame around the steps in the subproof. In this case the subproof
concludes with a step that does not use the \proofRule{subproof} rule,
but another rule, such as the \proofRule{bind} rule.
\begin{example}
This example shows a refutation of the
formula $(2 + 2) ≈ 5$. The proof uses a subproof to prove the
lemma $((2 + 2) ≈ 5) \Rightarrow 4 ≈ 5$.
\begin{Alethe}
1.& \ctxsep & $(2 + 2) ≈ 5$ & $\proofRule{assume}$ \\
2.& \spctxsep & $(2 + 2) ≈ 5 $ & $\proofRule{assume}$ \\
3.& \spctxsep & $(2 + 2) ≈ 4 $ & $\proofRule{sum_simplify}$ \\
4.& \spctxsep & $4 ≈ 5 $ & $(\proofRule{trans}\ 2, 3)$ \\
\spsep
5.& \ctxsep & $\neg((2 + 2) ≈ 5), 4 ≈ 5$ & $\proofRule{subproof}$ \\
6.& \ctxsep & $(4 ≈ 5)≈ \bot$ & $\proofRule{eq_simplify}$ \\
7.& \ctxsep & $\neg((4 ≈ 5)≈ \bot), \neg(4≈ 5), \bot $ & $\proofRule{equiv_pos2}$ \\
8.& \ctxsep & $\bot $ & $(\proofRule{resolution}\ 1, 5, 6, 7)$ \\
\end{Alethe}
\end{example}
\paragraph{Contexts.}
A specialty of the Alethe proofs
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$. In the first case, we say that $c_i$ \emph{fixes} its
variable. Throughout this document $\Gamma$ denotes
an arbitrary context. Alethe contexts are a general mechanism to write
substitutions and to change them by attaching new elements to the list.
Hence, every context $\Gamma$ induces a substitution
\(\operatorname{subst}(\Gamma)\). If $\Gamma$ is the empty list,
\(\operatorname{subst}(\Gamma)\) is the empty substitution, i.e, the
identity function. When $\Gamma$ ends in a mapping, the substitution is extended
with this mapping: \(\operatorname{subst}([c_1,\dots, c_{n-1}, x_n\mapsto t_n]) =
\operatorname{subst}([c_1,\dots, c_{n-1}])\circ \{x_n\mapsto t_n\}\).
Finally, \(\operatorname{subst}([c_1,\dots, c_{n-1}, x_n])\)
is \(\operatorname{subst}([c_1,\dots, c_{n-1}])\), but $x_n$ maps to $x_n$.
The last case fixes $x_n$ and allows the context to shadow a previously defined
substitution for $x_n$. The following example illustrates this idea:
\begin{align*}
\operatorname{subst}([x\mapsto 7, x \mapsto g(x)]) &= \{x\mapsto g(7)\}\\
\operatorname{subst}([x\mapsto 7, x, x \mapsto g(x)]) &= \{x\mapsto g(x)\}\\
\end{align*}
Formally, the context can be translated to $\lambda$-abstraction and
application. This is discussed in the next section.
\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 changes 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 Alethe must consider the possible
implicit reordering of equalities.
\subsection{The Semantics of the Alethe Language}
\label{sec:semantic}
An Alethe proof is a list of steps and anchors, but not every list of
steps and anchors is an Alethe proof. In this sections we first give the
restrictions that separate an Alethe proof from lists of steps and anchors
that are not Alethe proof. Then we show that Alethe proofs are sound.
That is, if an Alethe proof contains the empty clause as a conclusion
not within a subproof, then the input assertions are contradictory.
We will not prove that every rule is sound.
An Alethe proof $P$ is a list $[s_1, \dots, s_n]$ of steps and anchors.
\emph{Anchors} capture the point in a proof where a subproof starts.
In the graphical notation we are using this is the start of the
vertical black line. Furthermore, the context
only changes at an anchor and the steps that conclude a subproof
and an anchor only ever extends the context. Hence, every
anchor is associated with an, possibly empty, list
of variables and variable, term tuples. The steps among $s_1, \dots, s_n$
are not associated with a context. Instead the context can be computed.
In the following a concluding rule is a proof rule that concludes a
subproof (such as \proofRule{subproof}, \proofRule{bind}, and so forth).
In the following we assume, without loss of generality, that each step
$s_i$ in $P$ uses $i$ as its index. Furthermore, $\vDash$ represents
semantic consequence in the many-sorted first order logic of SMT-LIB
with the theories of uninterpreted functions and linear arithmetic.
\begin{definition}[Calculated Context]
Let $s_i$ be a step or anchor in $P$ such that no step $s_j$
where $j < i$ uses a concluding rule.
Let $a_1, \dots, a_m$ be the anchors among $s_1, \dots, s_{i-1}$.
The calculated context of $s_i$ is the context
\[
c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}
\]
where $c_{k,1}, \dots, c_{k, n_k}$ is the list of variables
and variable, term tuples associated with $a_k$.
Note that if $s_i$ is an anchor, its calculated context does not
contain the the variables and variable, term tuples associated with $s_i$.
Hence, the context of $s_i$ is the context just before $s_i$ is applied.
\end{definition}
To check the validity of a proof we can inductively eliminate subproofs
until we reach a proof without subproof.
If we always eliminate the first
subproof that does not contain another subproof we can calculate the context
and check the validity of the subproof directly.
The following notion captures the idea of a subproof that can be eliminated.
\begin{definition}[Admissible Subproof]
Let $P$ be the proof $[s_1, \dots, s_n]$ and $1 \leq \mathit{start}
< \mathit{end} \leq n$ such that
\begin{itemize}
\item $s_{\mathit{start}}$ is an anchor,
\item $s_{\mathit{end}}$ is a step that uses a concluding rule,
\item no $s_k$ with $k < \mathit{start}$ uses a concluding rule,
\item no $s_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
a step that uses a concluding rule,
\end{itemize}
The proof $P$ contains an \emph{admissible subproof} if there are such
$\mathit{start}$, $\mathit{end}$ and
\begin{itemize}
\item all steps $s_k$ with $\mathit{start} \leq k <
\mathit{end}$ only use the premises $s_l$ with $\mathit{start} <
l < k$,
\item all steps $s_k$ are valid application of their rule under the
calculated context of $s_{\mathit{end}}$,
\item the step $s_{\mathit{end}}$ is a valid application of its rule
under its calculated context of $s_{\mathit{start}}$.
\end{itemize}
\end{definition}
Since the \proofRule{assume} rule expects an empty context, an admissible
subproof can only contain assumptions if the rule used by $s_{\mathit{end}}$
is the \proofRule{subproof} rule.
To eliminate a part of a proof, we can replace some steps with a hole.
To do soe we create a new step $s'$ that uses the \proofRule{hole} rule, has
the conclusion and index of $s_{\mathit{end}}$.
The new proof is: $P' = [s_1, \dots, s_{\mathit{start}-1}, s', s_{\mathit{end}+1}, \dots, s_n]$.
Since proofs are finite, this process stops at some admissible proof
$P_{\mathit{last}}$. If the structure of the proof is not well formed
there will still be some anchors and steps using concluding rules in
$P_{\mathit{last}}$. Otherwise, we can check $P_{\mathit{last}}$ to
see if the overall proof is valid.
\begin{definition}[Admissible Proof]
\label{def:valid_proof}
An Alethe proof $P = [s_1, \dots, s_n]$ is an admissible proof
if every step uses an unique index and one of the following two sets
of conditions hold:
\begin{itemize}
\item It contains no anchor steps, or steps that use a concluding rule,
\item all steps $s_i$ only use the premises $s_j$ with $1 \leq j < i$,
\item all steps are valid applications of their rules under the empty context,
\item and it contains a step that has the empty clause as its conclusion.
\end{itemize}
or
\begin{itemize}
\item It contains an admissible subproof
\item and the proof $P'$ constructed as above is an admissible proof.
\end{itemize}
\end{definition}
In this document we will call the proof that terminates this iterative
process by fulfilling the first set of conditions the \emph{outermost proof}.
\begin{definition}[Valid Alethe Proof]
An admissible proof $P$ is a \emph{valid Alethe proof} if it contains
no step that uses the \proofRule{hole} rule.
\end{definition}
\subsubsection{Soundness}
To show the soundness of a valid Alethe proof $P = [s_1, \dots, s_n]$
we can use the same approach as for the definition of validity: consider
subproof free subproofs and then replace subproofs by holes.
\begin{theorem}[Soundness of Alethe]
\label{thm:sound}
If there is a valid Alethe proof $P$ that has the formulas
$\varphi_1, \dots, \varphi_m$ as the conclusions of the \proofRule{assume}
steps in its outermost proof, then
A specificity of the Alethe proofs
is the step \index{context}context.
Alethe contexts are a general mechanism to write
substitutions and to change them by attaching new elements.
A context is a possibly empty list $c_1,
\dots, c_l$, where each element is either a variable or a variable-term tuple
denoted $x_i\mapsto t_i$.
%
In the first case, we say that $c_i$ {\em fixes} the
variable. The second case is a mapping.
Throughout this chapter, $\Gamma$ denotes
an arbitrary context.
Every context $\Gamma$ induces a capture-avoiding substitution
$\subst(\Gamma)$. If $\Gamma$ is the empty list,
$\subst(\Gamma)$ is the empty substitution, i.e, the
identity function.
The first case fixes $x_n$ and allows the context to shadow a previously defined
substitution for $x_n$:
\[
\varphi_1, \dots, \varphi_m \vDash \bot
\subst([c_1,\dots, c_{n-1}, x_n])
\text{ is }\subst([c_1,\dots, c_{n-1}])\text{, but }x_n\text{ maps to }x_n.
\]
\end{theorem}
We wills start with simple subproofs without subproofs and with empty contexts.
Here, we will assume that every rule is sound.
\begin{lemma}
\label{lem:sound_subproof}
Let $P$ be a proof that contains an admissible subproof where
$s_{\mathit{end}}$ is a \proofRule{subproof} step. Let
$\psi$ be the conclusion of $s_{\mathit{end}}$
and $\varphi_1, \dots, \varphi_m$ are the conclusion of the
\proofRule{assume} steps between $s_{\mathit{start}}$ and
$s_{\mathit{end}}$.
Then $\vDash \varphi_1, \dots, \varphi_m \limp \psi$ holds.
\end{lemma}
\begin{proof}
First, we use induction on the number of steps $n$ after
$s_{\mathit{start}}$. Let $\psi_n$ be the conclusion
of $s_{\mathit{start}+n}$ and $V_n$ the conclusions of
the \proofRule{assume} steps in $[s_{\mathit{start}}, \dots,
s_{\mathit{start}+n}]$. We will
show $V_n \vDash \psi_n$ if $\mathit{start}+n < \mathit{end}$.
If $n = 1$ then $s_{\mathit{start}+1}$ must
be either a tautology, or an assume step. In the first case,
$\vDash \psi_{\mathit{start}+1}$ holds and in the second case
$\psi_{\mathit{start}+1} \vDash \psi_{\mathit{start}+1}$.
For subsequent $n$, $s_{\mathit{start}+n}$ is
either an ordinary step, or an assume step. In the second case,
$\psi_{\mathit{start}+n} \vDash \psi_{\mathit{start}+n}$ which can
be weakened to $V_n \vDash \psi_{\mathit{start}+n}$.
In the first case, the step $s_{\mathit{start}+n}$ has a set of
premises $P$.
For each step $s_{\mathit{start}+i} \in P$ we have $i < n$ and
$V_i \vDash \psi_{\mathit{start}+i}$ due to the induction
hypothesis. Since $i < n$, the premises $V_i$ are a subset of $V_n$ and
we can weaken $V_i \vDash \psi_{\mathit{start}+i}$
to $V_n \vDash \psi_{\mathit{start}+i}$. Since all premises of
$s_{\mathit{start}+n}$ are the consequence of $V_n$ we get
$V_n \vDash \psi_n$.
This process ends when $s_{\mathit{end}}$ is reached and we
get $\varphi_1, \dots, \varphi_n \vDash \psi$ and by definition of
\proofRule{subproof} $\vDash \varphi_1, \dots, \varphi_m \limp \psi$.
\end{proof}
\subsubsection{Contexts and Metaterms}
We now direct our attention to subproofs with contexts. Contexts are
local in the sense that they only affect the proof step they are
applied to. Since we already assume that all rules are sound and are
used correctly in a valid Alethe proof, it is not necessary for us to
discuss them further to show the soundness of Alethe proofs. However,
it is useful to give a precise semantic to context to have the tools
to check that rules that use contexts are sound.
For the full details on contexts see~\cite{barbosa-2019}.
The presentation here is adapted from this publication, but omits
some details.
To handle subproofs with contexts, we translate the contexts into
$\lambda$-terms.
These $\lambda$-terms are called \emph{metaterms}
\begin{definition}[Metaterm]
Metaterms are expressions constructed by the grammar
\[
M \,::=\, \boxed{t}\,\mid\, \lambda x.\,M\,\mid\,(\lambda \bar{x}_n.\,
M)\,\bar{t}_n
\]
where $t$ is an ordinary term and $t_i$ and $x_i$ have the same sort for
all $0 \leq i \leq 1$.
\end{definition}
According to this definition, a metaterm is either a boxed term, a
$\lambda$ abstraction, or an application to an uncurried $\lambda$-term.
The annotation $\boxed{t}$ delimits terms from the context, a simple
$\lambda$ abstraction is used to express fixed variables, and the
application expresses simulations substitution of $n$ terms.
We use $=_{\alpha\beta}$ to denote syntactic equivalence module modulo
$\alpha$-equivalence and $\beta$-reduction.
A proof step
\begin{plListEq}
\Gamma &\proofsep i. & t \simeq u & (\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]
\end{plListEq}
\noindent
is encoded into
\begin{plListEq}
&\proofsep i. & L(\Gamma)[t] \simeq R(\Gamma)[u] & (\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]
\end{plListEq}
where
\begin{align*}
L(\emptyset)[t] &= \boxed{t} & R(\emptyset)[u] &= \boxed{u} \\
L(x, \bar{c}_m)[t] &= \lambda x.\,L(\bar{c}_m)[t] & R(x, \bar{c}_m)[u] &= \lambda x.\,R(\bar{c}_m)[u] \\
L(\bar{x}_n\mapsto\bar{s}_n, \bar{c}_m)[t] &= (\lambda \bar{x}_n.\,L(\bar{c}_m)[t]) \bar{s}_n
& R(\bar{x}_n\mapsto\bar{s}_n, \bar{c}_m)[u] &= R(\bar{c}_m)[u] \\
\end{align*}
When $\Gamma$ ends in a mapping, the substitution is extended
with this mapping\label{page:ctxdef}:
\[
\subst([c_1,\dots, c_{n-1}, x_n\mapsto t_n]) =
\subst([c_1,\dots, c_{n-1}])\circ \{x_n\mapsto t_n\}.
\]
\begin{example}
This translation, together with $=_{\alpha\beta}$,
applies the $\subst$ function. For example:
\label{ex:alethe:substctx}The following example illustrates this idea.
\begin{align*}
L(x\mapsto 7, x \mapsto g(x))[x] = (\lambda x.\,(\lambda. x\,\boxed{x})\,(g(x)))\, 7
=_{\alpha\beta} \boxed{g(7)} \\
L(x\mapsto 7, x, x \mapsto g(x))[x] = (\lambda x.\,\lambda x.\,(\lambda. x\,\boxed{x})\,(g(x)))\, 7
=_{\alpha\beta} \boxed{g(x)} \\
\subst([x\mapsto 7, x \mapsto g(x)]) &= \{x\mapsto g(7)\} \\
\subst([x\mapsto 7, x, x \mapsto g(x)]) &= \{x\mapsto g(x)\} \\
\end{align*}
\end{example}
Most proof rules that operate with contexts can easily be translated into
proof rules using metaterms. The exception are the tautologous rules,
such as \proofRule{refl} and the \ruleType{..._simplify} rules.
Steps that use such rules always encode a judgment
$\vDash \Gamma \vartriangleright t \simeq u$. With the encoding described above
we get $L(\Gamma)[t] \simeq R(\Gamma)[u]
=_{\alpha\beta} \lambda \bar{x}_n.\,\boxed{t'} \simeq
\lambda \bar{x}_n.\,\boxed{u'}$ with some terms $t'$, $u'$.
To handle those terms, we use the $\reify$ function.
This function is defined as $\reify(\lambda \bar{x}_n.\,\boxed{t} \simeq
\lambda \bar{x}_n.\,\boxed{u}) = \forall \bar{x}_n.\,t \simeq u$.
Hence,
all tautological rules with contexts represent a judgment
$\vDash \reify(T \simeq U)$
where $T =_{\alpha\beta} L(\Gamma)[t]$ and $U =_{\alpha\beta} R(\Gamma)[u]$.
\begin{example}
Consider the step
\begin{plListEq}
y, x \mapsto y &\proofsep i. & x + 0 \simeq y & \ruleType{sum_simplify}
\end{plListEq}
Translating the context into meta terms gives us
\begin{plListEq}
&\proofsep i. & (\lambda x.\,(\lambda y.\,\boxed{x + 0}))\, y \simeq
(\lambda y.\,\boxed{y}) & \ruleType{sum_simplify}
\end{plListEq}
Applying $\beta$-reduction gives us
\begin{plListEq}
&\proofsep i. & (\lambda y.\,\boxed{y + 0}) \simeq
(\lambda y.\,\boxed{y}) & \ruleType{sum_simplify}
\end{plListEq}
Finally, using $\reify()$ gives us
\begin{plListEq}
&\proofsep i. & \forall y.\,(y + 0 \simeq y) & \ruleType{sum_simplify}
\end{plListEq}
This obviously holds in the theory of linear arithmetic.
Contexts are used to express proofs about the preprocessing of terms. The
conclusions of proof rules that use contexts always have the form
\begin{AletheS}
i. & $\Gamma$ & \ctxsep & $t ≈ u$ & ($\ruleType{rule}$, …) \\
\end{AletheS}
where the term $t$\, is the original term, and $u$ is the term after
preprocessing. Tautologies with contexts correspond to judgments
$\vDash_T \subst(\Gamma)(t) ≈ u$. Note that, some proof rules require
an empty context. In the list of proof rules
in Section~\ref{apx:rules}
this is indicated by omitting
the $\Gamma$.
The substitution induced by $\Gamma$ is capture-avoiding.
Hence, some bound variables could be renamed in
$\subst(\Gamma)(t)$ with respect to the original term $t$.
A consequence of this is that steps that use a context must be checked
under α-equivalence. The \proofRule{bind} rule can be used
to express renaming of bound variables explicitly. The \proofRule{refl}
rule, on the other hand, can be exploited to directly rename bound variables
without an explicit proof.
Formally, the context can be translated to \index{abstraction!lambda}λ-abstractions and
applications. This is discussed in Section~\ref{sec:alethe:semantics}.
\begin{example}\label{ex:ti:ctx-abstract}
This example shows a proof that uses a subproof with a context to rename a bound
variable.
\begin{AletheS}
1.& & \ctxsep & $\forall x.\,(P\,x)$ & $\proofRule{assume}$ \\
2.& & \ctxsep & $\neg (\forall y.\,(P\,y))$ & $\proofRule{assume}$ \\
3.& \spctx{$y, x \mapsto y$} & \ctxsep & $x ≈ y$ & $\proofRule{refl}$\\
4.& \spctx{$y, x \mapsto y$} & \ctxsep & $(P\,x) ≈ (P\,y)$
& $(\proofRule{cong}\,3) $\\
\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))$
& $\proofRule{equiv_pos2}$ \\
7.& &\ctxsep & $\bot$ & $(\proofRule{resolution}\,1, 2, 5, 6)$ \\
\end{AletheS}
\end{example}
We now give a version of Lemma~\ref{lem:sound_subproof} with contexts.
\begin{lemma}
\label{lem:sound_subproof_context}
Let $P$ be a proof that contains an admissible subproof where
$s_{\mathit{end}}$ is a step using one of:
\proofRule{bind}, \proofRule{sko_ex}, \proofRule{sko_forall},
\proofRule{onepoint}, \proofRule{let}.
Then $V \vDash \Gamma \vartriangleright \psi$ where $\Gamma$ is the
calculated context of $s_{\mathit{start}}$ and $\psi$ is the conclusion
of $s_{\mathit{end}}$. The set $V$ is empty if $s_{\mathit{end}}$
does not use the \ruleType{let} rule. Otherwies, it contains all
conclusions of the
\ruleType{assume} steps among $[s_{\mathit{start}'}, \dots,
s_{\mathit{start}}]$ where $\mathit{start}'$ is either the largest index
${\mathit{start}'} < {\mathit{start}}$ such that $s_{\mathit{start}'}$ is an
anchor, or $1$ if no such index exist.
\end{lemma}
\begin{proof}
The step $s_{\mathit{start}}$ is an anchor due to the definition
of admissible proof.
Let $c_1, \dots, c_n$ is the context introduce by the anchor
$s_{\mathit{start}}$ and let $\Gamma' = \Gamma, c_1, \dots, c_n$.
$\Gamma'$ is the calculated context of the steps in the subproof after
$s_{\mathit{start}}$.
The step $s_{\mathit{end}}$ is a step
\begin{plContainer}
\begin{plSubList}
\plLine\\
\Gamma'
\proofsep& i.& \psi' &(\dots)\\
\end{plSubList}
\begin{plList}
\Gamma \proofsep& \mathit{end}.& \psi &(\ruleType{rule}\;i_1 \dots i_n)\\
\end{plList}
\end{plContainer}
Since we assume the step $s_{\mathit{end}}$ is correctly employed,
$\vDash \Gamma \vartriangleright \psi$ holds, as long as
$\vDash \Gamma' \vartriangleright \psi'$ holds.
We perform the same induction as for
Lemma~\ref{lem:sound_subproof} over the steps in
$[s_{\mathit{start}}, \dots, s_{\mathit{end}}]$. Here, the sets
$V_i$ stay empty since there are no assumptions in the subproof.
The induction ends once $s_i$ is reached. At this step we
get $\vDash \Gamma' \vartriangleright \psi'$.
Only the \ruleType{let} rule uses additional premises
$s_{i_1}, \dots, s_{i_n}$. Hence, for all other rules the conclusion
cannot depend on any steps outside the subproof and $V$ is empty.
% TODO: this is ugly, let is ugly
Due to the definition of admissible subproof, all steps $s_{i_1},
\dots, s_{i_n}$ are in the same subproof that starts at $s_{\mathit{start}'}$.
Furthermore, they are all valid steps that do not conclude a subproof.
If this is the outermost proof, or a subproof that concludes with
an \ruleType{subproof} step, then $s_{i_1}, \dots, s_{i_n}$ might
depend on some \ruleType{assume} steps that appear before them
in their subproof. In this case we can, as we saw in the proof of
Lemma~\ref{lem:sound_subproof}, weaken their judgments to include
all assumptions in $[s_{\mathit{start}'}, \dots, s_{\mathit{start}}]$.
If the subproof that starts at $s_{\mathit{start}'}$ concludes with
any other rule, then ther cannot be any assumptions and $V$ is empty.
\end{proof}
\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 sole exception is the topmost equality in the conclusion of steps
with non-empty context. The order of the arguments of this equality can
never change.
As described above, all rules that accept a non-empty context have
a conclusion of the form $t ≈ u$. Since the context
represents a substitution applied to the left-hand side,
this equality symbol is not symmetric.
The SMT solver {\verit} currently applies this freedom in a restricted
form: equalities are reordered only
when the term below the equality changes 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 Alethe must consider the possible
implicit reordering of equalities everywhere.
\subsubsection{Soundess of Valid Alethe Proofs}
By using Lemma~\ref{lem:sound_subproof} and
Lemma~\ref{lem:sound_subproof_context} we can no show that a valid Alethe proof
is sound. That is, we can show Theorem~\ref{thm:sound}.
\subsection{The Syntax}\label{sec:alethe:syntax}
\begin{proof}
By induction on the number of anchors in $P = [s_1, \dots, s_n]$.
If there is no anchor in $P$ then there is a step $s_i$ that has the
empty clause as its conclusion. We can perform the same induction as
in the proof of Lemma~\ref{lem:sound_subproof} with $\mathit{start} = 1$
and $\mathit{end} = i$. This shows that $V \vDash \bot$, where $V$ is the
conclusion of the \proofRule{assume} steps in $[s_1, \dots, s_i]$. We can weaken
this by adding the conclusions of the \proofRule{assume} steps in
$[s_i, \dots, s_n]$ to get $\varphi_1, \dots, \varphi_m \vDash \bot$.
If there are $n$ anchors in $P$ then there is an admissible subproof with
indices $\mathit{start}$, $\mathit{end}$.
Depending on the rule used by $s_{\mathit{end}}$ either
Lemma~\ref{lem:sound_subproof} and Lemma~\ref{lem:sound_subproof_context}
applies. Hence, it is safe to replace the subproof $[s_{\mathit{start}}, \dots
s_{\mathit{end}}$ with the new step $s'$ as we do in
Definition~\ref{def:valid_proof}. The newly constructed proof $P'$ has
$n-1$ anchors and hence is sound due to the induction hypothesis.
\end{proof}
The concrete text representation of the Alethe proofs
is based on the {\smtlib} standard. Figure~\ref{fig:proof_ex} shows an
example proof as printed by {\verit} with light edits for readability.
%
The format follows the {\smtlib} standard when possible.
%
Input problems in the {\smtlib} format are scripts. An {\smtlib} script
is a list of commands that manipulate the SMT solver. For example,
\inlineAlethe{assert} introduces an assertion, \inlineAlethe{check-sat} starts
solving, and \inlineAlethe{get-proof} instructs the SMT solver to print the
proof.
%
Alethe mirrors this structure. Therefore, beside the {\smtlib}
logic and term language, it also uses commands to structure the proof.
An Alethe proof is a list of commands.
\begin{figure}[t]
\begin{minted}[linenos]{smtlib2.py -x}
\begin{AletheVerb}
(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))))
(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)))
(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
instantiation and resolution steps (line 10--15)}\label{fig:proof_ex}
\end{AletheVerb}
\caption{Example proof output. Assumptions are
introduced; a subproof renames bound variables; the proof finishes with
instantiation and resolution steps.}
\label{fig:proof_ex}
\end{figure}
\subsection{The Syntax}
\label{sec:syntax}
\begin{figure}[t]
{\centering
{ % TODO typesetting hack: align adds an empty line break
\setlength{\belowdisplayskip}{0pt}
\setlength{\belowdisplayshortskip}{0pt}
\[\begin{array}{rcl}
\grNT{proof} &\grRule& \grNT{proof\_command}^{*}\\
\grNT{proof\_command} &\grRule& \grT{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\; \grT{)}\\
&\grOr & \grT{(step}\; \grNT{symbol}\; \grNT{clause}
\; \grT{:rule}\; \grNT{symbol}\\
& & \quad \grNT{premises\_annotation}^{?}\\
& & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\; \grT{)}\\
& \grOr & \grT{(anchor}\; \grT{:step}\; \grNT{symbol}\;\grNT{attribute}^{*}\; \grT{)}\\
& \grOr & \grT{(anchor}\; \grT{:step}\; \grNT{symbol}\;
\grNT{args\_annotation}^{?}\;\\
& & \quad \grNT{attribute}^{*}\; \grT{)}\\
& \grOr & \grT{(define-fun}\; \grNT{function\_def}\; \grT{)}\\
\grNT{clause} &\grRule& \grT{(cl}\; \grNT{proof\_term}^{*}\; \grT{)}\\
\grNT{proof\_term} &\grRule& \grNT{term}\text{ extended with }\\
& & \grT{(choice (}\; \grNT{sorted\_var}\;\grT{)}\; \grNT{proof\_term}\; \grT{)} \\
\grNT{premises\_annotation} &\grRule& \grT{:premises (}\; \grNT{symbol}^{+}\grT{)}\\
\grNT{args\_annotation} &\grRule& \grT{:args}\;\grT{(}\; \grNT{step\_arg}^{+}\; \grT{)} \\
\grNT{step\_arg} &\grRule& \grNT{symbol} \grOr
\grT{(}\; \grNT{symbol}\; \grNT{proof\_term}\; \grT{)}\\
\grNT{context\_annotation} &\grRule& \grT{:args}\;\grT{(}\;\grNT{context\_assignment}^{+}\;\grT{)} \\
\grNT{context\_assignment} &\grRule& \grT{(}\; \grNT{sorted_var}\; \grT{)} \\
& \grOr & \grT{(:=}\; \grNT{symbol}\;\grNT{proof_term}\;\grT{)}\\
\end{array}\]
}\par}
\caption{The proof grammar.}\label{fig:grammar}
\[
\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}
\; \textAlethe{:rule}\; \grNT{symbol} \\
& & \quad \grNT{premises\_annotation}^{?} \\
& & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
& \grOr & \textAlethe{(anchor :step}\; \grNT{symbol}\;
\\
& & \quad \grNT{args\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
& \grOr & \textAlethe{(define-fun}\; \grNT{function\_def}\,\textAlethe{)} \\
\grNT{clause} &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
\grNT{proof\_term} &\grRule & \grNT{term}\text{ extended with } \\
& & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)} \\
\grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
\grNT{args\_annotation} &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)} \\
\grNT{step\_arg} &\grRule & \grNT{symbol} \grOr
\textAlethe{(}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
\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{figure}
The concrete text representation of the Alethe proofs
is based on the SMT-LIB standard. Figure~\ref{fig:proof_ex} shows an
exemplary proof as printed by veriT with light edits for readability.
The format follows the SMT-LIB standard when possible. Hence, beside
the SMT-LIB logic and term language, it also uses commands to structure
the proof. An Alethe proof is a list of commands.
Usually an Alethe proof is associated with a concrete SMT-LIB problem
Every Alethe proof is associated with an {\smtlib} problem
that is proved by the Alethe proof. This can either be a concrete
problem file or, if the incremental solving features of SMT-LIB
problem file or, if the incremental solving commands of {\smtlib}
are used, the implicit problem constructed at the invocation of a
$\grT{get-proof}$ command.
In this document we will call this SMT-LIB problem the \emph{input problem}.
\inlineAlethe{get-proof} command.
In this document, we will call this {\smtlib} problem the {\em input problem}.
An Alethe proof inherits the namespace of its {\smtlib} problem.
All symbols declared or defined in the input problem remain declared or
defined, respectively. Furthermore, the symbolic names introduced
by the $\grT{:named}$ annotation also stay valid and can be used
defined, respectively.
Furthermore, the symbolic names introduced
by the \inlineAlethe{:named} annotation also stay valid and can be used
in the script. For the purpose of the proof rules, terms are treated
as if proxy names introduced by $\grT{:named}$ annotations have been
as if proxy names introduced by \inlineAlethe{:named} annotations have been
expanded and annotations have been removed. For example, the term
\smtinline{(or (! (P a) :named baz) (! baz :foo))} and
\smtinline{(or (P a) (P a))} are considered to be syntactically equal.
\inlineAlethe{(or (! (P a) :named baz) (! baz :foo))} and
\inlineAlethe{(or (P a) (P a))} are considered to be syntactically equal.
Here \inlineAlethe{:foo} is an arbitrary {\smtlib} annotation.
Figure~\ref{fig:grammar} shows the grammar of the proof text. It
is based on the SMT-LIB grammar, as defined in the SMT-LIB
standard version 2.6 Appendix~B\footnote{Available online at:
\url{http://smtlib.cs.uiowa.edu/language.shtml}}. The nonterminals
$\grNT{attribute}$
is based on the {\smtlib} grammar, as defined in the {\smtlib}
standard~\cite[Appendix~B]{SMTLIB}. The non-terminals
$\grNT{attribute}$,
$\grNT{function\_def}$,
$\grNT{sorted\_var}$,
$\grNT{symbol}$, and
$\grNT{term}$
are as defined in the standard. The $\grNT{proof_term}$
is the recursive $\grNT{term}$ nonterminal redefined with the additional
production for the $\grT{choice}$ binder.
Input problems in the SMT-LIB standard contain a list of \emph{commands}
that modify the internal state of the solver. Following
this approach Alethe proofs are also formed by a list of commands.
The $\grT{assume}$ command introduces a new assumption. While this
command could also be expressed using the $\grT{step}$ command with
a special rule, the special semantic of an assumption justifies the
are as defined in the standard. The non-terminal $\grNT{proof\_term}$
corresponds to the $\grNT{term}$ non-terminal of {\smtlib}, but is
extended with the additional production for the \inlineAlethe{choice}\index{choice} binder.
Alethe proofs are a list of commands.
The \inlineAlethe{assume} command introduces a new assumption. While this
command could also be expressed using the \inlineAlethe{step} command with
a special rule, the special semantics of an assumption justifies the
presence of a dedicated command: assumptions are neither tautological nor
derived from premises. The $\grT{step}$ command, on the other hand,
introduces a derived or tautological formula. Both commands $\grT{assume}$
and $\grT{step}$ require an index as the first argument to later
refer back to it. This index is an arbitrary SMT-LIB symbol.
It must be unique for each $\grT{assume}$ and $\grT{step}$ command.
A special restriction applies to the $\grT{assume}$ of the main proof.
Those reference assertions in the input SMT-LIB problem. To simplify
proof checking, the $\grT{assume}$ command must use the name assigned
derived from premises. The \inlineAlethe{step} command, on the other hand,
introduces a derived or tautological clause. Both commands \inlineAlethe{assume}
and \inlineAlethe{step} require an index as the first argument to later
refer back to it. This index is an arbitrary {\smtlib} symbol.
It must be unique for each \inlineAlethe{assume} and \inlineAlethe{step} command.
A special restriction applies to the \inlineAlethe{assume} commands
not within a subproof, which reference assertions in the input {\smtlib} problem. To simplify
proof checking, the \inlineAlethe{assume} command must use the name assigned
to the asserted formula if there is any. For example, if the input
problem contains \smtinline{(assert (! (P c) :named foo))} then
the proof must refer to this assert (if it is needed) as
\smtinline{(assume foo (P c))}. Note that SMT-LIB problem can
assign a name to terms at any point, not only at their first assert.
problem contains \inlineAlethe{(assert (! (P c) :named foo))}, then
the proof must refer to this assertion (if it is needed in the proof) as
\inlineAlethe{(assume foo (P c))}. Note that an {\smtlib} problem can
assign a name to a term at any point, not only at its first occurrence.
If a term has more than one name, any can be picked.
The second argument of $\grT{step}$ and $\grT{assume}$
is the term introduced by the command.
For a $\grT{step}$, this term is always a clause.
To express disjunctions in SMT-LIB the $\grT{or}$ operator is used.
The second argument of \inlineAlethe{step} and \inlineAlethe{assume}
is the conclusion of the command.
For a \inlineAlethe{step}, this term is always a clause.
To express disjunctions in {\smtlib} the \inlineAlethe{or} operator is used.
This operator, however, needs at least two arguments and cannot
represent unary or empty clauses. To circumvent this we introduce a new
$\grT{cl}$ operator. It corresponds the standard $\grT{or}$ function
represent unary or empty clauses. To circumvent this, we introduce a new
\inlineAlethe{cl} operator. It corresponds to the standard \inlineAlethe{or}
function
extended to one argument, where it is equal to the identity, and zero
arguments, where it is equal to $\grT{false}$.
The $\grT{anchor}$ and $\grT{define-fun}$ commands are used for
subproofs and sharing, respectively. The $\grT{define-fun}$ command
corresponds exactly to the $\grT{define-fun}$ command of the
SMT-LIB language.
Furthermore, the syntax uses annotations as used by SMT-LIB. The
original SMT-LIB syntax uses the non-terminal $\grNT{attribute}$.
The Alethe syntax uses some standard annotation. To simplify parsing
arguments, where it is equal to \inlineAlethe{false}.
Every step must use the \inlineAlethe{cl} operator, even if its conclusion
is a unit clause.
The \inlineAlethe{anchor} and \inlineAlethe{define-fun} commands are used for
subproofs and sharing, respectively. The \inlineAlethe{define-fun} command
corresponds exactly to the \inlineAlethe{define-fun} command of the
{\smtlib} language.
Furthermore, the syntax uses annotations as used by {\smtlib}. The
original {\smtlib} syntax uses the non-terminal $\grNT{attribute}$.
The Alethe syntax uses some predefined annotation. To simplify parsing,
the order in which those must be printed is strict.
The $\grT{:premises}$ annotation denotes the premises and is skipped
if they are none. If the rule carries arguments, the
$\grT{:args}$ annotation is used to denote them.
Anchors have two annotations: $\grT{:step}$ provides the name of the
step that concludes the subproof and $\grT{:args}$ provides the context
as sorted variables and assignments. Note that in this annotation
the $\grT{symbol}$ non-terminal is intended to be a variable.
The \inlineAlethe{:premises} annotation denotes the premises and is skipped
if the rule does not require premises. If the rule carries arguments, the
\inlineAlethe{:args} annotation is used to denote them.
Anchors have two annotations: \inlineAlethe{:step} provides the name of the
step that concludes the subproof and \inlineAlethe{:args} provides the context
as sorted variables and assignments. Note that in this annotation,
the $\grNT{symbol}$ non-terminal is intended to be a variable.
After those pre-defined annotations, the solver can use additional
annotation. This can be used for debugging, or other purposes.
A consumer of Alethe proofs \emph{must} be able to parse proofs
that contain such annotations.
annotations. This can be used for debugging, or other purposes.
A consumer of Alethe proofs {\em must} be able to parse proofs
that contain such annotations.
\paragraph{Subproofs}
The abstract notation denotes subproofs by marking them with a vertical
line. To map this notation to a list of commands, Alethe \index{anchor}uses the
\inlineAlethe{anchor} command. This command indicates the start of a subproof.
A subproof is concluded by a matching \inlineAlethe{step} command. This step must use
a \index{rule!concluding}{\em concluding rule}
(such as \proofRule{subproof}, \proofRule{bind}, and so forth).
After the \inlineAlethe{anchor} command, the proof uses \inlineAlethe{assume} commands to list
the assumptions of the subproof. Subsequently, the subproof is a list of
\inlineAlethe{step} commands that can use prior steps in the subproofs as premises.
In the abstract notation, every step is associated with a context. The
concrete syntax uses anchors to optimize this.
The \index{context}context is manipulated in a nested way: if a step
pops $c_1,\dots, c_n$ from a context $\Gamma$, there is an earlier step which
pushes precisely $c_1,\dots, c_n$ onto the context.
%
Since contexts can only be manipulated by push and pop, context manipulations
are nested. The \inlineAlethe{anchor} commands push onto the context and the
corresponding \inlineAlethe{step} commands pop from the context.
To indicate these changes to the context, every anchor is associated with a list
of fixed variables and mappings.
This list can be empty.
Note that, when an \inlineAlethe{anchor} command extends a context $\Gamma$ with
some mappings $x_1 \mapsto t_1, \dots, x_n \mapsto t_n$,
then the terms $t_i$ are normalized by applying
the substitution $\subst(\Gamma)$ to $t_i$. This is because the definition
on page~\pageref{page:ctxdef} extends the context by composing the substitutions.
The \inlineAlethe{:step} annotation of the anchor command is used to indicate
the \inlineAlethe{step} command that will end the subproof. The clause of
this \inlineAlethe{step} command is the conclusion of the subproof.
While it is possible to infer the
step that concludes a subproof from the structure of the proof, the explicit
annotation simplifies proof checking and makes the proof easier to read.
If the subproof uses a
context, the \inlineAlethe{:args} annotation of the \inlineAlethe{anchor} command
indicates the arguments added to the context for this subproof. The
annotation provides the sort of fixed variables.
In the example proof (Figure~\ref{fig:proof_ex}) a
subproof starts at the \inlineAlethe{anchor} command.
It ends with the \proofRule{bind} steps that finishes the
proof for the renaming of the bound variable \inlineAlethe{z2}
to \inlineAlethe{vr4}.
A further restriction applies: only the conclusion of a subproof can be used
as a premise outside the subproof. Hence, a proof checking tool can
remove the steps of the subproof from memory after checking it.
\begin{example}
\label{ex:ti:ctx-concrete}
This example shows the proof from Example~\ref{ex:ti:ctx-abstract}
expressed as a concrete proof.
\begin{AletheVerb}
(assume h1 (forall ((x S)) (P x)))
(assume h2 (not (forall ((y S)) (P y))))
(anchor :step t5 :args ((:= x y)))
(step t3 (cl (= x y)) :rule refl)
(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
:rule bind)
(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
(not (forall ((x S)) (P x)))
(forall ((y S)) (P y)))) :rule equiv_pos2)
(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
\end{AletheVerb}
\end{example}
\tikzset{
solver/.style={draw, thin},
system/.style={draw, thin, rounded corners},
}
\begin{figure}[t]
\centering
\scalebox{0.8}{
\begin{figure}[h]
\center
\begin{tikzpicture}[node distance=2cm, auto,>=latex', thick,scale=0.8]
\node[solver] (unsat) {Unsat mode};
\node[system, right=of unsat] (assume) {Assumptions};
\path[->] (unsat) edge[bend left] node {\texttt{get-proof}} (assume);
\path[->] (assume) edge[loop above] node[align=center] {$\grT{assume}$,\\ $\grT{define-fun}$,\\ $\grT{anchor}$} (assume);
\node[system, right=of assume] (step) {Steps};
\path[->] (assume) edge[bend left] node {$\grT{step}$} (step);
\path[->] (step) edge[loop above] node[align=center] {$\grT{step}$,\\ $\grT{define-fun}$} (step);
\path[->] (step) edge[above, bend left] node {$\grT{anchor}$} (assume);
\path[->] (step) edge[above, bend left] node {Last step} (unsat);
\end{tikzpicture}}
\caption{Abstract view of the transitions in an Alethe proof}\label{fig:proof-states}
\node[solver] (unsat) {\textsf{Unsat mode}};
\node[system, right=of unsat] (assume) {\textsf{Assumptions}};
\path[->] (unsat) edge[bend left] node[font=\scriptsize] {\texttt{get-proof}} (assume);
\path[->] (assume) edge[loop above] node[align=center,font=\scriptsize] {\inlineAlethe{assume},\\\inlineAlethe{define-fun},\\\inlineAlethe{anchor}} (assume);
\node[system, right=of assume] (step) {\textsf{Steps}};
\path[->] (assume) edge[bend left] node[font=\scriptsize] {\inlineAlethe{step}} (step);
\path[->] (step) edge[loop above] node[align=center,font=\scriptsize] {\inlineAlethe{step},\\ \inlineAlethe{define-fun}} (step);
\path[->] (step) edge[above, bend left] node[font=\scriptsize] {\inlineAlethe{anchor}} (assume);
\path[->] (step) edge[above, bend left] node[font=\scriptsize] {\textsf{Last step}} (unsat);
\end{tikzpicture}
\label{fig:proof-states}\caption{Abstract view of the transitions in an Alethe proof.}
\end{figure}
\paragraph{Alethe Proof Printing States}
Figure~\ref{fig:proof-states} shows the states of an Alethe proof
abstractly. To generate a proof, the SMT solver must be in the
\emph{Unsat mode}, i.e., the solver determined that the problem
is unsatisfiable. The user of the solver then requests the proof by
invoking the $\grT{get-proof}$ command. It is possible that this command
fails. For example, proof production was not activated upfront.
If there is no error, the proof is printed and printing starts by printing
{\em Unsat mode}, i.e., the solver determined that the problem
is unsatisfiable. The {\smtlib} problem script then requests the proof by
invoking the \inlineAlethe{get-proof} command. It is possible that this command
fails. For example, if proof production was not activated up front.
If there is no error, the proof is printed and printing starts with
the assumptions. The solver prints the proof as a list of commands
according to the state. The states ensure one constraint is maintained:
assumptions can only appear at either the beginning of a proof or right
after a subproof is started by the $\grT{anchor}$ command. They can not
after a subproof is started by the \inlineAlethe{anchor} command. They cannot
be mixed with ordinary proof steps. This simplifies
reconstruction. Each assumption printed at the beginning of the proof
corresponds to assertions in the input problem, up to symmetry of equality.
Proof printing concludes after the last step is printed and the solver
returns to the Unsat mode and the user can issue further commands.
Usually the last step is a step the main proof
Usually the last step is an outermost step
(i.e., not within a subproof) that concludes the proof by deriving
the empty clause, but this is not necessary.
The solver is allowed to print some additional, useless,
steps after the proof is concluded.
\subsection*{Subproofs}
As the name suggests, the \grT{anchor} command together with proof
rules such as the \proofRule{subproof} rule expresses subproofs. This
is possible because its application is restricted: the assumption used
as premise
for the \proofRule{subproof} step must be the assumption introduced
last. Hence, the \grT{assume}, \proofRule{subproof} pairs are
nested. The context is manipulated in the same way: if a step
pops $c_1,\dots, c_n$ from a context $\Gamma$, there is an earlier step which
pushes precisely $c_1,\dots, c_n$ onto the context. Since
contexts can only be manipulated by push and pop, context manipulations
are also nested.
Because of this nesting, a subproof
is started right before an \grT{assume} command or a command which
pushes onto the context. We call this point the {\em anchor} and an Alethe
contains the \grT{anchor} command at this point.
After the \grT{Anchor} command the proof uses \grT{assume} commands to list
the assumptions of the subproof. Subsequently the subproof is a list of
\grT{step} commands that can use the assumptions of and any parent subproof
as premises.
The subproof ends with a \grT{step} command using the \proofRule{subproof} rule or
another rule that pops from the context, respectively. The $\grT{:step}$
annotation of the anchor command is used to indicate the $\grT{step}$
command which will end the subproof. The term of this $\grT{step}$
command is the conclusion of the subproof. While it is possible to infer the
step that concludes a subproof from structure of the proof, the explicit
annotation simplifies reconstruction and makes the proof easier to read.
If the subproof uses a
context, the $\grT{:args}$ annotation of the $\grT{anchor}$ command
indicates the arguments added to the context for this subproof. The
annotation provides the sort of fixed variables.
In the example proof (Figure~\ref{fig:proof_ex}) a subproof starts on line four.
It ends on line seven with the \proofRule{bind} steps which finished the
proof for the renaming of the bound variable \smtinline{z2}
to \smtinline{vr4}.
A further restriction applies: only the conclusion of a subproof can be used
as a premise outside of the subproof. Hence, a proof checking tool can
remove the steps of the subproof from memory after checking it.
\begin{comment}{Hans-Jörg Schurr}
There is an open question with regard to the best way to print
subproofs:
There is an implicit relation between the last step of the subproof
and the step concluding the subproof.
{\textrightarrow} what if we would, for some reason, have some crap after the last step
of the subproof? We cannot accommodate this yet.
There are multiple solutions to solve this implicit dependency.
steps after the proof is concluded.
{\textbullet} One is to
give the final step of the subproof as a premise to the step concluding
the subproof.
{\textrightarrow} downside: normally it's forbidden to use steps from within a deeper proof
{\textbullet} We could have the conclusion of the subproof already in the anchor.
or we could turn the current structure upside down
{\textrightarrow} downside: a solver that just dumps out steps can not no always know
the conclusion when opening a subproof. For example, when simplifications are applied.
\end{comment}
\subsection*{Sharing and Skolem Terms}
Alethe proofs are generally large. One reason for this is that SMT
solvers can store terms internally much more efficiently. A term data
\paragraph{Sharing and Skolem Terms}
Usually, SMT solvers store terms internally in an efficient manner. A term data
structure with perfect sharing ensures that every term is stored in memory
precisely once. When printing the proof this compact storage is unfolded.
precisely once. When printing the proof, this compact storage is unfolded.
This leads to a blowup of the proof size.
Alethe can optionally use sharing\footnote{For veriT this can be activated
by the command-line option \texttt{--proof-with-sharing}.} to print common
Alethe can optionally use sharing\footnote{For {\verit} this can be activated
by the command-line option \Verb{--proof-with-sharing}.} to print common
subterms only once. This is realized using the standard naming mechanism
of SMT-LIB. In the language of SMT-LIB it is possible to annotate any
term $t$ with a name $n$ by writing $\grT{(! }t\grT{ :named }n\grT{ )}$
of {\smtlib}. A term $t$ is annotated with a name $n$ by writing
\inlineAlethe{(!}\,$t$\,\inlineAlethe{:named}\;$n$\,\inlineAlethe{)}
where $n$ is a symbol. After a term is annotated with a name, the name can
be used in place of the term. This is a purely syntactical replacement.
Alethe continues to use the names already used in the input problem.
@@ -1269,95 +938,690 @@ Hence, terms that already have a name in the input problem can be replaced
by that name and new names introduced in the proof must not use names
already used in the input problem.
To limit the number of names introduced, an SMT solver can use the following
simple approach used by veriT.
Before printing the proof it iterates over all terms of the proof and
To limit the number of names, an SMT solver can use the following
simple approach used by {\verit}.
Before printing the proof, it iterates over all terms of the proof and
recursively descend into the terms. It marks every unmarked subterm it
visits. If a visited term is already marked, the solver assigns a new name
to this term. If a term already has a name, it does not descend further
into the term.
%
By doing so, it ensures that only terms that appear as
child of two different parent terms get a name. Since a name term is replaced
with its name after it first appearance, a term that only appears
as a child of one single term not need a distinct name.
child of two different parent terms get a name. Since a named term
is replaced with its name after it first appearance, a term that only
appears as a child of one single term does not need a distinct name.
%
Thanks to the perfect
sharing representation testing if a term is marked takes constant time
sharing representation, testing if a term is marked takes constant time
and the overall traversal takes linear time in the proof size.
To simplify reconstruction Alethe can optionally\footnote{For veriT by
using the command-line option \texttt{--proof-define-skolems}.} define
Skolem constants as functions. In this case the proof contains a list
of $\grT{define-fun}$ commands that define shorthand 0-ary functions for
the $\grT{(choice }\dots\grT{)}$ terms needed. Without this option,
no $\grT{define-fun}$ commands are issued and the constants are expanded.
To simplify reconstruction, Alethe can optionally\footnote{For {\verit} by
using the command-line option \Verb{--proof-define-skolems}.} define
Skolem constants as functions. In this case, the proof contains a list
of \inlineAlethe{define-fun} commands that define shorthand 0-ary functions for
the \inlineAlethe{(choice }\dots\inlineAlethe{)} terms needed. Without this option,
no \inlineAlethe{define-fun} commands are issued, and the constants are expanded.
\section{The Alethe Rules}
\label{sec:rules-generic}
\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{)} in the
original {\smtlib} problem or in the proof.
\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
as renaming of bound variables, and the application of substitutions.
\section{Checking Alethe Proofs}
\label{sec:alethe:semantics}
In this section we present an abstract procedure to check if an Alethe
proof is \index{well-formed}well-formed and valid. An Alethe proof is
well-formed only if its anchors and steps are balanced. To check that
this is the case, we replace innermost subproofs by holes until there is
no subproof left. If the resulting reduced proof is free of anchors and steps
that use concluding rules, then the overall proof is well-formed.
To check if a proof is valid we have to check if all steps of a subproof
adhere to the conditions of
their rules before replacing the subproof by a hole.
If all subproofs are valid and all steps in the reduced
proof adhere to the conditions of their rule,
then the entire proof is valid.
Formally, an Alethe proof $P$ is a list $[C_1, \dots, C_n]$ of steps
and anchors.
Since every step uses an unique index, we assume that each step
$C_i$ in $P$ uses $i$ as its index.
The context
only changes at anchors and subproof-concluding steps.
Therefore, the elements of $C_1, \dots, C_n$ that are steps
are not associated with a context.
Instead, the context can be computed
from the prior anchors.
The anchors only ever extend the context.
To check an Alethe proof we can iteratively eliminate the first-innermost
subproof, i.e., the innermost subproof that does not come after a
complete subproof. The restriction to the first subproofs simplifies
the calculation of the context of the steps in the subproof.
\begin{definition}[First-Innermost Subproof]
Let $P$\, be the proof $[C_1, \dots, C_n]$ and $1 \leq \mathit{start}
< \mathit{end} \leq n$ be two indices such that
\begin{itemize}
\item $C_{\mathit{start}}$ is an anchor,
\item $C_{\mathit{end}}$ is a step that uses a concluding rule,
\item no $C_k$ with $k < \mathit{start}$ uses a concluding rule,
\item no $C_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
a step that uses a concluding rule.
\end{itemize}
Then $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$ is the
\index{subproof!first-innermost}first-innermost subproof of $P$.
\end{definition}
\begin{example}
The proof in Example~\ref{ex:ti:ctx-concrete} has only one subproof
and this subproof is also a first-innermost subproof. It is the subproof
\begin{AletheVerb}
(anchor :step t5 :args ((:= x y)))
(step t3 (cl (= x y)) :rule refl)
(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
:rule bind)
\end{AletheVerb}
\end{example}
\noindent
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$.
Let $A_1, \dots, A_m$ be the anchors among $C_1, \dots, C_{\mathit{start}-1}$.
The \index{context!calculated}calculated context of $C_i$ is the context
\[
c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}
\]
where $c_{k,1}, \dots, c_{k, n_k}$ is the list of fixed variables
and mappings associated with $A_k$.
\end{definition}
Note that if $C_i$ is an anchor, its calculated context does not
contain the elements associated with $C_i$.
Therefore, the context of $C_{\mathit{start}}$
is the context of the steps before the subproof.
Furthermore, the step $C_{\mathit{end}}$ is the concluding
step of the subproof and must have the same context as the steps surrounding
the subproof.
Hence, the context of $C_{\mathit{end}}$ is the calculated
context of $C_{\mathit{start}}$.
\begin{example}
The calculated context of the steps \texttt{\color{SmtStepId}t3} and \texttt{\color{SmtStepId}t5} in
Example~\ref{ex:ti:ctx-concrete} is the context $x \mapsto y$.
The calculated context of the concluding step \texttt{\color{SmtStepId}t5} and the anchor is empty.
\end{example}
\noindent
A first-innermost subproof is valid if all its steps adhere to
the conditions of their rule and only use premises that occur before them
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
\begin{itemize}
\item all steps $C_i$ with $\mathit{start} < i <
\mathit{end}$ only use premises $C_j$ with $\mathit{start} <
j < i$,
\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
rule under the calculated context of $C_{\mathit{start}}$.
\end{itemize}
\end{definition}
The only rule that can discharge assumptions in a subproof is the
\proofRule{subproof} rule. Therefore, an admissible subproof can only
contain \proofRule{assume} step if $C_{\mathit{end}}$
is the \proofRule{subproof} rule.
To eliminate a subproof we can replace the subproof with a hole that has
at its conclusion the conclusion of the subproof. This is safe as long
as the subproof that is eliminated is valid (see Section~\ref{sec:alethe:soundness-eh}).
\begin{definition}
The function $E$ eliminates the first-innermost subproof from a proof
if there is one.
Let $P$ be a proof $[C_1, \dots C_n]$.
Then $E(P) = P$ if $P$ has no first-innermost subproof.
Otherwise, $P$ has the first-innermost subproof
$[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$, and
$E(P) = [C_1, \dots, C_{\mathit{start}-1}, C', C_{\mathit{end}+1},
\dots, C_n]$ where $C'$ is a new step that uses the \proofRule{hole} rule
and has the index, conclusion, and premises of $C_{\mathit{end}}$.
\end{definition}
It is important to add the premises of $C_{\mathit{end}}$
to $C'$. The \proofRule{let} rule can use additional premises
and omitting those premises results in an unsound step.
We can apply $E$ iteratively to a proof $P$ until we reach the least fixed point.
Since $P$ is finite we will always reach a fixed point in finitely many steps.
The result is a list $[P_0, P_1, P_2, \dots, P_{\mathit{last}}]$ where $P_0 = P$,
$P_1 = E(P)$, $P_2 = E(E(P))$ and $P_{\mathit{last}} = E(P_{\mathit{last}})$.
\begin{example}
Applying $E$\, to the proof in
Example~\ref{ex:ti:ctx-concrete} gives us the proof
\begin{AletheVerb}
(assume h1 (forall ((x S)) (P x)))
(assume h2 (not (forall ((y S)) (P y))))
(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
:rule hole)
(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
(not (forall ((x S)) (P x)))
(forall ((y S)) (P y)))) :rule equiv_pos2)
(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
\end{AletheVerb}
Since this proof contains no subproof, it is also $P_{\mathit{last}}$.
\end{example}
\begin{definition}[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
\begin{itemize}
\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 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
rule under the empty context.
\end{itemize}
\end{definition}
The condition that $P$ contains no hole ensures that the original
proof is complete and holes are only introduced by eliminating valid
subproofs.
\begin{example}
The proof in Example~\ref{ex:ti:ctx-concrete} is valid. The only
subproof is valid, the proof contains no hole, and $P_{\mathit{last}}$
contains the step \textsf{\color{SmtStepId} t7} that concludes with the empty clause.
\end{example}
It is sometimes useful to speak about the steps that are not within a
subproof. We call such a step an \index{step!outermost}{\em outermost
step}. In a well-formed proof those are the steps
of $P_{\mathit{last}}$.
\subsection{Contexts and Metaterms}
We now direct our attention to subproofs with \index{context}contexts.
It is useful to give precise semantics
to contexts to have the tools to check that rules that use contexts
are sound.
Contexts are local in the sense that they affect only the
proof step they are applied to.
For the full details on contexts see~\cite{barbosa-2019}.
The presentation here is adapted from this publication, but omits some
details.
To handle subproofs with contexts, we translate the contexts into
λ-terms.
%
This allows us to
leverage the \index{lambda calculus}λ-calculus as an existing well-understood theory of \index{binder}binders.
%
These λ-terms\index{term!lambda} are called \index{term!meta}\index{metaterms}{\em metaterms}.
\begin{definition}[Metaterm]
Metaterms are expressions constructed by the grammar
\[
M \,::=\, \groundbox{$t$}\,\mid\, \lambda x.\,M\,\mid\,(\lambda \bar{x}_n.\,
M)\,\bar{t}_n
\]
where $t$ is an ordinary term and $t_i$ and $x_i$ have matching sorts for
all $0 \leq i \leq 1$.
\end{definition}
According to this definition, a metaterm is either a boxed term, a
\index{abstraction!lambda}λ-abstraction, or an application to an uncurried λ-term.
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.}
We use $=_{\alpha\beta}$ to denote syntactic equivalence modulo
α-equivalence and β-reduction.
Proof steps with contexts can be encoded into proof steps with empty
contexts, but with metaterms. A proof step
\begin{AletheS}
i. & $\Gamma$ & \ctxsep & $t ≈ u$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]$ \\
\end{AletheS}
Together with the language, the Alethe format also comes with a set
of proof rule. Section~\ref{sec:rules} gives a full list of all
proof rules. Currently, the proof rules correspond to the rules used
by the veriT solver. For the rest of this section, we will discuss some
\noindent
is encoded into
\begin{AletheS}
i. & & \ctxsep & $L(\Gamma)[t] ≈ R(\Gamma)[u]$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]$ \\
\end{AletheS}
\noindent
where
\begin{align*}
L(\emptyset)[t] &= \groundbox{t} & R(\emptyset)[u] &= \groundbox{u} \\
L(x, \bar{c}_m)[t] &= \lambda x.\,L(\bar{c}_m)[t] & R(x, \bar{c}_m)[u] &= \lambda x.\,R(\bar{c}_m)[u] \\
L(\bar{x}_n\mapsto\bar{s}_n, \bar{c}_m)[t] &= (\lambda \bar{x}_n.\,L(\bar{c}_m)[t]) \bar{s}_n
& R(\bar{x}_n\mapsto\bar{s}_n, \bar{c}_m)[u] &= R(\bar{c}_m)[u] \\
\end{align*}
To achieve the same effect as using the $\subst()$ function described above, we
can translate the terms into metaterms, perform β-reduction, and rename
bound variables if necessary~\cite[Lemma~11]{barbosa-2019}.
\begin{example}
The example on page~\pageref{ex:alethe:substctx} becomes
\begin{flalign*}
\quad & L(x\mapsto 7, x \mapsto g(x))[x] = (\lambda x.\,(\lambda x.\,\groundbox{x})\,(g(x)))\, 7
=_{\alpha\beta} \groundbox{g(7)} &\\
& L(x\mapsto 7, x, x \mapsto g(x))[x] = (\lambda x.\,\lambda x.\,(\lambda x.\,\groundbox{x})\,(g(x)))\, 7
=_{\alpha\beta} \lambda x.\,\groundbox{g(x)}
\end{flalign*}
\end{example}
Most proof rules that operate with contexts can easily be translated into
proof rules using metaterms. The exception are the tautologous rules,
such as \proofRule{refl} and the $\cdots{}${\ruleType{_simplify}} rules.
Steps that use such rules always encode a judgment
$\vDash \Gamma\,\vartriangleright\,t ≈ u$. With the encoding described above
we get $L(\Gamma)[t] ≈ R(\Gamma)[u]
=_{\alpha\beta} \lambda \bar{x}_n.\,\groundbox{t'} ≈
\lambda \bar{x}_n.\,\groundbox{u'}$ with some terms $t'$, $u'$.
To handle those terms, we use the $\reify()$ function.
This function is defined as
\[
\reify(\lambda \bar{x}_n.\,\groundbox{t} ≈
\lambda \bar{x}_n.\,\groundbox{u}) = \forall \bar{x}_n.\,(t ≈ u).
\]
Therefore,
all tautological rules with contexts represent a judgment\\
$\vDash \reify(T ≈ U)$
where $T =_{\alpha\beta} L(\Gamma)[t]$ and $U =_{\alpha\beta} R(\Gamma)[u]$.
\begin{example}
Consider the step
\begin{AletheS}
i. & $y, x \mapsto y$ & \ctxsep
& $x + 0 ≈ y$ & $\proofRule{sum_simplify}$ \\
\end{AletheS}
\noindent
Translating the context into metaterms leads to
\begin{AletheS}
i. & \phantom{$y, x \mapsto y$} & \ctxsep
& $(\lambda y.\,(\lambda x.\,\groundbox{$x + 0$})\, y) ≈
(\lambda y.\,\groundbox{$y$})$ & $\proofRule{sum_simplify}$ \\
\end{AletheS}
\noindent
Applying β-reduction leads to
\begin{AletheS}
i. & \phantom{$y, x \mapsto y$} & \ctxsep
& $(\lambda y.\,\groundbox{$y + 0$}) ≈
(\lambda y.\,\groundbox{$y$}) $ & $\proofRule{sum_simplify}$ \\
\end{AletheS}
\noindent
Finally, using $\reify()$ leads to
\begin{AletheS}
i. & \phantom{$y, x \mapsto y$} & \ctxsep
& $\forall y.\,(y + 0 ≈ y)$ & $\proofRule{sum_simplify}$ \\
\end{AletheS}
\noindent
This obviously holds in the theory of linear arithmetic.
\end{example}
\subsection{Soundness}
\label{sec:alethe:soundness-eh}
Any proof calculus should be sound. In the case of Alethe, most proof
rules are
standard rules, or simple tautologies. The rules that use context
are unusual, but those proof rules were previously shown to be
sound~\cite{barbosa-2019}.
Alethe does not use any rules that are merely satisfiability preserving.
The skolemization rules replace the bound variables with choice terms
instead of fresh symbols.\footnote{The \inlineAlethe{define-fun} function
can introduce fresh symbols, but we will assume here that those
commands have been eliminated by unfolding the definition.}
All Alethe rules express semantic implications.
Overall, we assume in this document that the proof rules and proofs
written in the abstract notation are sound.
Nevertheless, a modest gap remains. The concrete, command-based
syntax does not precisely correspond to the abstract notation.
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.
\]
\end{theorem}
Here, $\vDash$ represents
semantic consequence in the many-sorted first order logic of {\smtlib}
with the theories of uninterpreted functions and linear arithmetic extended
with the choice operator and clauses.
To show the soundness of a valid Alethe proof $P = [C_1, \dots, C_n]$,
we can use the same approach as for the definition of validity: consider
first-innermost subproof first and then replace them by holes.
%
Since valid proofs do not contain holes, we have to generalize the induction
to allow holes that were introduced by the elimination of subproofs.
%
We start with simple subproofs with empty contexts and without
nested subproofs.
\begin{lemma}
\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}}$.
Then $\vDash \psi$ holds.
\end{lemma}
\begin{proof}
First, we use induction on the number of steps $n$ after
$C_{\mathit{start}}$. Let $\psi_n$ be the conclusion
of $C_{\mathit{start}+n}$ and $V_n$ the conclusions of
the \proofRule{assume} steps in $[C_{\mathit{start}}, \dots,
C_{\mathit{start}+n}]$.
Assumptions always introduce unit clauses. We will identify
unit clauses with their single literal.
We will
show $V_n \vDash \psi_n$ if $\mathit{start}+n < \mathit{end}$.
If $n = 1$, then $C_{\mathit{start}+n} = C_{\mathit{start}+1}$ must
either be a tautology, or an \proofRule{assume} step. In the first case,
$\vDash \psi_{\mathit{start}+1}$ holds, and in the second case
$\psi_{\mathit{start}+1} \vDash \psi_{\mathit{start}+1}$ holds.
For subsequent $n$, $C_{\mathit{start}+n}$ is
either an ordinary step, or an \proofRule{assume} step. In the second case,
$\psi_{\mathit{start}+n} \vDash \psi_{\mathit{start}+n}$ which can
be weakened to $V_n \vDash \psi_{\mathit{start}+n}$.
In the first case, the step $C_{\mathit{start}+n}$ has a set of
premises $S$.
For each step $C_{\mathit{start}+i} \in S$ we have $i < n$ and
$V_i \vDash \psi_{\mathit{start}+i}$ due to the induction
hypothesis. Since $i < n$, the premises $V_i$ are a subset of $V_n$ and
we can weaken $V_i \vDash \psi_{\mathit{start}+i}$
to $V_n \vDash \psi_{\mathit{start}+i}$. Since all premises of
$C_{\mathit{start}+n}$ are the consequence of $V_n$ we get
$V_n \vDash \psi_n$.
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.
\end{proof}
\noindent
We can do the same reasoning as for Lemma~\ref{lem:sound_subproof} for
subproofs with contexts. This is slightly complicated by the
\proofRule{let} rule that can use extra premises.
\begin{lemma}\label{lem:sound_subproof_context}
Let $P$ be a proof that contains a
valid first-innermost subproof where
$C_{\mathit{end}}$ is a step using one of:
\proofRule{bind}, \proofRule{sko_ex}, \proofRule{sko_forall},
\proofRule{onepoint}, \proofRule{let}.
Then $V \vDash \Gamma \vartriangleright \psi$ where $\Gamma$ is the
calculated context of $C_{\mathit{start}}$ and $\psi$ is the conclusion
of $C_{\mathit{end}}$. The set $V$\, is empty if $C_{\mathit{end}}$
does not use the \proofRule{let} rule. Otherwise, it contains all
conclusions of the
\proofRule{assume} steps among $[C_{δ}, \dots,
C_{\mathit{start}}]$ where $δ$ is either the largest index
$δ < {\mathit{start}}$ such
that $s_{δ}$ is an anchor, or $1$ if no such index exist.
Hence, there is no anchor between $C_{δ}$ and $C_{\mathit{start}}$.
\end{lemma}
\begin{proof}
The step $C_{\mathit{start}}$ is an anchor due to the definition
of innermost-first subproof.
Let $c_1, \dots, c_n$ be the context introduced by the anchor
$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
$C_{\mathit{start}}$.
The step $C_{\mathit{end}}$ is a step
\begin{AletheS}
& \spctx{} & & $\cdots$ & \\
$\mathit{end}-1$. & \spctx{$\Gamma'$} & \ctxsep & $\,\psi'$ & $(\dots)$ \\
\spsep
$\mathit{end}$. & $\Gamma$ & \ctxsep & $\psi$ & $(\ruleType{rule}\;i_1, \dots, i_n)$ \\
\end{AletheS}
Since we assume the step $C_{\mathit{end}}$ is correctly employed,
$\vDash \Gamma \vartriangleright \psi$ holds, as long as
$\vDash \Gamma' \vartriangleright \psi'$ holds.
We perform the same induction as for
Lemma~\ref{lem:sound_subproof} over the steps in
$[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$.
%
Since $C_{\mathit{end}}$ does not use the \proofRule{subproof} rule,
the subproof does not contain any assumptions and
$V_i$ stays empty.
%
Again, we are interested in the step $C_{\mathit{end}-1}$. At this step we
get $\vDash \Gamma' \vartriangleright \psi'$.
Only the \proofRule{let} rule uses additional premises
$C_{i_1}, \dots, C_{i_n}$. Hence, for all other rules, the conclusion
cannot depend on any step outside the subproof and $V$\, is empty.
% TODO: this is ugly, let is ugly
Due to the definition of first-innermost subproof, all steps $C_{i_1},
\dots, C_{i_n}$ are in the same subproof that starts at $C_{δ}$.
The steps $C_{i_1}, \dots, C_{i_n}$ might
depend on some \proofRule{assume} steps that appear before them
in their subproof. This is the case if the steps are outermost steps, or
if the subproof that starts at $C_{δ}$ concludes with
a \proofRule{subproof} step.
%
In this case we can, as we saw in the proof of
Lemma~\ref{lem:sound_subproof}, weaken their judgments to include
all assumptions in $[C_{δ}, \dots, C_{\mathit{start}}]$.
If the subproof that starts at $C_{δ}$ concludes with
any other rule, then there cannot be any assumptions and $V$\, is empty.
\end{proof}
By using Lemma~\ref{lem:sound_subproof} and
Lemma~\ref{lem:sound_subproof_context} we can now show that
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:semantics}.
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}
\section{Core Concepts of the Alethe Rules}
\label{sec:alethe:rules-generic}
Together with the language, the Alethe format also includes a set
of proof rule.
Section~\ref{apx:rules}
gives a full list of all
proof rules. Currently, the proof rules correspond to the rules
that the solver {\verit} can emit. For the rest of this section, we will discuss some
general concepts related to the rules.
\paragraph{Tautologous Rules and Simple Deduction.}
\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
\dots \land \varphi_n), \varphi_i$.
%
Other rules derive their conclusion from a single 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$.
rule eliminates an implication: From $\varphi_1 → \varphi_2$,
it deduces $\neg \varphi_1, \varphi_2$.
\paragraph{Resolution.}
CDCL($T$)-based SMT solvers, and especially their SAT solvers,
{\cdclt}-based SMT solvers, and especially their SAT solvers,
are fundamentally based on resolution of clauses.
Hence, Alethe also has dedicated clauses and a resolution proof
rule. However, since SMT solvers do not enforce a strict
clausal normal-form, ordinary disjunction is also used.
clausal normal form, ordinary disjunction is also used.
Keeping clauses and disjunctions distinct simplifies rule checking.
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}
the sole literal starts with a disjunction and non-unit clauses. The
syntax for clauses uses the \inlineAlethe{cl} operator, while disjunctions
use the standard {\smtlib} \inlineAlethe{or} operator. The \proofRule{or}
\emph{rule} is responsible for converting disjunctions into clauses.
The Alethe 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 Alethe proofs use a generalized propositional resolution
rule with the 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 no notion of a unifier. The resolution
rules also implicitly simplifies repeated negations at the head
of literals.
The premises of a resolution step are clauses and the conclusion
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.}
\paragraph{Quantifier Instantiation}
To express quantifier instantiation, the rule \proofRule{forall_inst}
is used. It produces a formula of the form $(\neg \forall \bar
x_n.\,\varphi)\lor \varphi[\bar t_n]$, where $\varphi$ is
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$.
ground term $t_i$ is a new term with the same sort as $x_i$.\footnote{
For historical reasons, \proofRule{forall_inst} 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),
\dots, (x_n, t_n)\). While this information can be recovered from the term,
The arguments of a \proofRule{forall_inst} step are the list $(x_1 , t_1),
\dots, (x_n, t_n)$. While this information can be recovered from the term,
providing it explicitly helps reconstruction because the implicit reordering of
equalities (see below) obscures which terms have been used as instances.
Existential quantifiers are handled by Skolemization.
equalities obscures which terms have been used as instances.
Existential quantifiers are handled by skolemization.
\paragraph{Linear Arithmetic.}
\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$
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.}
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
(in)equalities. Checking the validity of this clause 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.
@@ -1366,328 +1630,79 @@ the coefficients is a trivial inequality between constants.
\begin{example}
The following example is the proof 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.& (3 < x), (x + y < 1) &(\proofRule{or}\;1)\\
\proofsep& 5.& \neg (3<x), \neg (x\simeq 2) &\proofRule{la_generic}\; [1.0, 1.0]\\
\proofsep& 6.& \neg (3<x) &(\proofRule{resolution}\; 2, 5)\\
\proofsep& 7.& x + y < 1 &(\proofRule{resolution}\; 4, 6)\\
\proofsep& 8.& \neg (x + y < 1), \neg (x\simeq 2) \lor \neg (0 \simeq y)
&\proofRule{la_generic}\;[1.0, -1.0, 1.0]\\
\proofsep& 9.& \bot &(\proofRule{resolution}\; 8, 7, 2, 3)
\end{plListEq}
of $(x+y<1) \lor$ $(3<x)$, $x≈ 2$, and $0≈ y$.
\begin{Alethe}
1.& \ctxsep & $(3 < x) \lor (x + y < 1) $ & $ \proofRule{assume}$ \\
2.& \ctxsep & $x≈ 2 $ & $ \proofRule{assume}$ \\
3.& \ctxsep & $0≈ y $ & $ \proofRule{assume}$ \\
4.& \ctxsep & $(3 < x), (x + y < 1) $ & $ (\proofRule{or}\,1)$ \\
5.& \ctxsep & $\neg (3<x), \neg (x≈ 2) $ & $ \proofRule{la_generic}\, [1.0, 1.0]$ \\
6.& \ctxsep & $\neg (3<x) $ & $ (\proofRule{resolution}\, 2, 5)$ \\
7.& \ctxsep & $x + y < 1 $ & $ (\proofRule{resolution}\, 4, 6)$ \\
8.& \ctxsep & $\neg (x + y < 1), \neg (x≈ 2) \lor \neg (0 ≈ y)$ & $\proofRule{la_generic}\,[1.0, -1.0, 1.0]$ \\
9.& \ctxsep & $\bot $ & $ (\proofRule{resolution}\, 8, 7, 2, 3)$ \\
\end{Alethe}
\end{example}
\paragraph{Skolemization and Other Preprocessing Steps.}
\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 (\varepsilon x.\varphi) &\proofsep n.&\varphi \simeq \psi &(\ruleType{\dots})\\
\Gamma &\proofsep m.& (\exists x.\varphi) \simeq \psi &(\proofRule{sko_ex}\; n)
\end{plListEq}
rule that is used to express skolemization of an existentially
quantified variable.
%
The conclusion of a step that uses this rules is an equality.
The left-hand side is a formula starting with an existential quantifier
over some variable $x$. In the formula on the right-hand side, the
variable is replaced by the appropriate Skolem term.
To provide a proof for the replacement, the \proofRule{sko_ex} step
uses one premise.
The premise
has a context that maps the existentially quantified variable
to the appropriate Skolem term.
\begin{AletheS}
i. & \spctx{$\Gamma, x\mapsto (\varepsilon x.\,\varphi)$} & \ctxsep
& $\varphi ≈ \psi$ & $(\dots)$ \\
\spsep
j. & $\Gamma$ & \ctxsep & $(\exists x.\,\varphi) ≈ \psi$ & $(\proofRule{sko_ex})$ \\
\end{AletheS}
\begin{example}
To illustrate how such a rule is applied, consider the following example
taken from~\cite{barbosa-2019}. Here the term $\neg p(\varepsilon x.\neg
p(x))$ is Skolemized. The \proofRule{refl} rule expresses
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 $\varepsilon x.\neg\varphi$.
\begin{plListEqAlgn}
x\mapsto (\varepsilon x.\neg p(x)) \proofsep& 1.& x &\simeq \varepsilon x.\neg p(x) &\proofRule{refl}\\
x\mapsto (\varepsilon x.\neg p(x)) \proofsep& 2.& p(x) &\simeq p(\varepsilon x.\neg p(x)) &(\proofRule{cong}\; 1)\\
\proofsep& 3.&( \forall x.p(x))&\simeq p(\varepsilon x.\neg p(x)) &(\proofRule{sko_forall}\; 2)\\
\proofsep& 4.&(\neg\forall x.p(x))&\simeq \neg p(\varepsilon x.\neg p(x)) &(\proofRule{cong}\; 3)
\end{plListEqAlgn}
\end{example}
\begin{AletheS}
1. & \spctx{$x\mapsto (\varepsilon x.\,\neg (p\,x))$}
& \ctxsep
& $x ≈ \varepsilon x.\,\neg (p\,x) $ &
$\proofRule{refl}$ \\
2. & \spctx{$x\mapsto (\varepsilon x.\,\neg (p\,x))$} & \ctxsep & $ (p\,x) ≈ p(\varepsilon x.\,\neg (p\,x))$ & $(\proofRule{cong}\, 1)$ \\
\spsep
3. & & \ctxsep & $( \forall x.\,(p\,x))≈ (p\,(\varepsilon x.\,\neg (p\,x)))$ & $(\proofRule{sko_forall}\, 2)$ \\
4. & & \ctxsep & $(\neg\forall x.\,(p\,x))≈ \neg (p\,(\varepsilon x.\,\neg (p\,x)))$ & $(\proofRule{cong}\, 3)$ \\
\end{AletheS}
\end{example}
\section{The Alethe Rules}
\label{apx:rules}
\input{rule_list}
\subsection{Classifications of the Rules}
\label{sec:rules-overview}
Section~\ref{sec:rules} provides a list of all proof rules supported by
Alethe. To make this long list more accessible, this section
first lists multiple classes of proof rules. The classes are not
mutually exclusive: for example, the \proofRule{la_generic} rule is
both a linear arithmetic rule and introduces a tautology.
Table~\ref{rule-tab:special} lists rules that serve a special purpose.
Table~\ref{rule-tab:tautologies} lists all rules that introduce
tautologies. That is, regular rules that do not use premises.
Within the tables, the number in brackets corresponds to the number
of the rule in Section~\ref{sec:rules}.
\begin{table}[ht]\label{rule-tab:special}
\caption{Special Rules}
\centering
\begin{tabular}{l l}
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{tabular}
\end{table}
\begin{table}[h!]
\caption{Resolution and Related Rules}
\centering
\begin{tabular}{l l}
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{tabular}
\end{table}
%\begin{table}[h!]
%\centering
\begin{longtable}{l l}
\caption{Rules Introducing Tautologies}\label{rule-tab:tautologies}\\
Rule & Conclusion \\
\hline
\ruleref{true} & \(\top\) \\
\ruleref{false} & \(\neg\bot\) \\
\ruleref{not_not} & \(\neg(\neg\neg\varphi), \varphi\) \\
\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
\ruleref{la_disequality} & \(t_1 \simeq t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)\) \\
\ruleref{la_totality} & \(t_1 \leq t_2 \lor t_2 \leq t_1\) \\
\ruleref{la_tautology} & A trivial linear tautology. \\
\ruleref{forall_inst} & Quantifier instantiation. \\
\ruleref{refl} & Reflexivity after applying the context. \\
\ruleref{eq_reflexive} & \(t \simeq t\) without context. \\
\ruleref{eq_transitive} & \(\neg (t_1 \simeq t_2) , \dots , \neg (t_{n-1} \simeq t_n) ,
t_1 \simeq t_n\) \\
\ruleref{eq_congruent} & \(\neg (t_1 \simeq u_1) , \dots , \neg (t_n \simeq u_n) ,
f(t_1, \dots, t_n) \simeq f(u_1, \dots, u_n)\) \\
\ruleref{eq_congruent_pred} & \(\neg (t_1 \simeq u_1) , \dots , \neg (t_n \simeq u_n) ,
P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n)\) \\
\ruleref{qnt_cnf} & Clausification of a quantified formula. \\
\ruleref{and_pos} & \(\neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k \) \\
\ruleref{and_neg} & \( (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1 , \dots , \neg\varphi_n \) \\
\ruleref{or_pos} & \( \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots , \varphi_n \) \\
\ruleref{or_neg} & \( (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k \) \\
\ruleref{xor_pos1} & \( \neg (\varphi_1 \operatorname{xor} \varphi_2) , \varphi_1 , \varphi_2 \) \\
\ruleref{xor_pos2} & \( \neg (\varphi_1 \operatorname{xor} \varphi_2), \neg \varphi_1, \neg \varphi_2 \) \\
\ruleref{xor_neg1} & \( \varphi_1 \operatorname{xor} \varphi_2, \varphi_1 , \neg \varphi_2 \) \\
\ruleref{xor_neg2} & \( \varphi_1 \operatorname{xor} \varphi_2, \neg \varphi_1 , \varphi_2 \) \\
\ruleref{implies_pos} & \( \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 \) \\
\ruleref{implies_neg1} & \( \varphi_1 \rightarrow \varphi_2, \varphi_1 \) \\
\ruleref{implies_neg2} & \( \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 \) \\
\ruleref{equiv_pos1} & \(\neg (\varphi_1 \leftrightarrow \varphi_2) , \varphi_1 , \neg \varphi_2\) \\
\ruleref{equiv_pos2} & \(\neg (\varphi_1 \leftrightarrow \varphi_2) , \neg \varphi_1 , \varphi_2\) \\
\ruleref{equiv_neg1} & \(\varphi_1 \leftrightarrow \varphi_2 , \neg \varphi_1 , \neg \varphi_2\) \\
\ruleref{equiv_neg2} & \(\varphi_1 \leftrightarrow \varphi_2 , \varphi_1 , \varphi_2\) \\
\ruleref{ite_pos1} & \(\neg (\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3) , \varphi_1 , \varphi_3\) \\
\ruleref{ite_pos2} & \(\neg (\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3) , \neg \varphi_1 , \varphi_2\) \\
\ruleref{ite_neg1} & \(\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3 , \varphi_1 , \neg \varphi_3\) \\
\ruleref{ite_neg2} & \(\operatorname{ite} \varphi_1\;\varphi_2\;\varphi_3 , \neg \varphi_1 , \neg \varphi_2\) \\
\ruleref{connective_def} & Definition of the boolean connectives. \\
\ruleref{and_simplify} & Simplification of a conjunction. \\
\ruleref{or_simplify} & Simplification of a disjunction. \\
\ruleref{not_simplify} & Simplification of a boolean negation. \\
\ruleref{implies_simplify} & Simplification of an implication. \\
\ruleref{equiv_simplify} & Simplification of an equivalence. \\
\ruleref{bool_simplify} & Simplification of combined boolean connectives. \\
\ruleref{ac_simp} & Flattening of nested \(\lor\) or \(\land\). \\
\ruleref{ite_simplify} & Simplification of if-then-else. \\
\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
\ruleref{eq_simplify} & Simplification of equality. \\
\ruleref{div_simplify} & Simplification of division. \\
\ruleref{prod_simplify} & Simplification of products. \\
\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
\ruleref{minus_simplify} & Simplification of subtractions. \\
\ruleref{sum_simplify} & Simplification of sums. \\
\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
\ruleref{distinct_elim} & Elimination of the distinction predicate. \\
\ruleref{la_rw_eq} & \((t \simeq u) \simeq (t \leq u \land u \leq t)\) \\
\ruleref{nary_elim} & Replace $n$-ary operators with binary application. \\
\end{longtable}
%\end{table}
\begin{table}[h!]
\caption{Linear Arithmetic Rules}
\centering
\begin{tabular}{l l}
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 \simeq t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)\) \\
\ruleref{la_totality} & \(t_1 \leq t_2 \lor t_2 \leq t_1\) \\
\ruleref{la_tautology} & A trivial linear tautology. \\
\ruleref{la_rw_eq} & \((t \simeq u) \simeq (t \leq u \land u \leq t)\) \\
\ruleref{div_simplify} & Simplification of division. \\
\ruleref{prod_simplify} & Simplification of products. \\
\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
\ruleref{minus_simplify} & Simplification of subtractions. \\
\ruleref{sum_simplify} & Simplification of sums. \\
\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
\end{tabular}
\end{table}
\begin{table}[h!]
\caption{Quantifier Handling}
\centering
\begin{tabular}{l l}
Rule & Description \\
\hline
\ruleref{forall_inst} & Instantiation of an universal variable. \\
\ruleref{bind} & Renaming of bound variables. \\
\ruleref{sko_ex} & Skolemization of existential variables. \\
\ruleref{sko_forall} & Skolemization of universal variables. \\
\ruleref{qnt_cnf} & Clausification of quantified formulas. \\
\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
\ruleref{onepoint} & The one-point rule. \\
\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
\end{tabular}
\end{table}
\begin{table}[h!]
\caption{Skolemization Rules}
\centering
\begin{tabular}{l l}
Rule & Description \\
\hline
\ruleref{sko_ex} & Skolemization of existential variables. \\
\ruleref{sko_forall} & Skolemization of universal variables. \\
\end{tabular}
\end{table}
\begin{table}[h!]
\caption{Clausification Rules. These rules can be used to perform propositional
clausification.}
\centering
\begin{tabular}{l l}
Rule & Description \\
\hline
\ruleref{and} & And elimination. \\
\ruleref{not_or} & Elimination of a negated disjunction. \\
\ruleref{or} & Disjunction to clause. \\
\ruleref{not_and} & Distribution of negation over a conjunction. \\
\ruleref{xor1} & From \(\operatorname{xor} \varphi_1 \varphi_2\) to \(\varphi_1, \varphi_2\). \\
\ruleref{xor2} & From \(\operatorname{xor} \varphi_1 \varphi_2\) to \(\neg\varphi_1, \neg\varphi_2\). \\
\ruleref{not_xor1} & From \(\neg(\operatorname{xor} \varphi_1 \varphi_2)\) to \(\varphi_1, \neg\varphi_2\). \\
\ruleref{not_xor2} & From \(\neg(\operatorname{xor} \varphi_1 \varphi_2)\) to \(\neg\varphi_1, \varphi_2\). \\
\ruleref{implies} & From \( \varphi_1\rightarrow\varphi_2 \) to \(\neg\varphi_1 , \varphi_2 \). \\
\ruleref{not_implies1} & From \(\neg (\varphi_1\rightarrow\varphi_2)\) to \(\varphi_1\). \\
\ruleref{not_implies2} & From \(\neg (\varphi_1\rightarrow\varphi_2)\) to \(\neg\varphi_2\). \\
\ruleref{equiv1} & From \( \varphi_1\leftrightarrow\varphi_2\) to \(\neg\varphi_1 , \varphi_2\). \\
\ruleref{equiv2} & From \( \varphi_1\leftrightarrow\varphi_2\) to \(\varphi_1 , \neg\varphi_2\). \\
\ruleref{not_equiv1} & From \(\neg(\varphi_1\leftrightarrow\varphi_2)\) to \(\varphi_1 , \varphi_2\). \\
\ruleref{not_equiv2} & From \(\neg(\varphi_1\leftrightarrow\varphi_2)\) to \(\neg\varphi_1 , \neg\varphi_2\). \\
\ruleref{and_pos} & \(\neg (\varphi_1 \land \dots \land \varphi_n), \varphi_k\)\\
\ruleref{and_neg} & \((\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n \) \\
\ruleref{or_pos} & \(\neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
, \varphi_n \) \\
\ruleref{or_neg} &
\( (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k \)\\
\ruleref{xor_pos1} &
\( \neg (\varphi_1 \operatorname{xor} \varphi_2) , \varphi_1 , \varphi_2 \) \\
\ruleref{xor_pos2} &
\( \neg (\varphi_1 \operatorname{xor} \varphi_2)
, \neg \varphi_1, \neg \varphi_2 \) \\
\ruleref{xor_neg1} &
\( \varphi_1 \operatorname{xor} \varphi_2, \varphi_1 , \neg \varphi_2 \) \\
\ruleref{xor_neg2} &
\( \varphi_1 \operatorname{xor} \varphi_2, \neg \varphi_1 , \varphi_2 \) \\
\ruleref{implies_pos} &
\( \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 \) \\
\ruleref{implies_neg1} &
\( \varphi_1 \rightarrow \varphi_2, \varphi_1 \) \\
\ruleref{implies_neg2} &
\( \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 \) \\
\ruleref{equiv_pos1} &
\(\neg (\varphi_1 \leftrightarrow \varphi_2) , \varphi_1 , \neg \varphi_2\) \\
\ruleref{equiv_pos2} &
\(\neg (\varphi_1 \leftrightarrow \varphi_2) , \neg \varphi_1 , \varphi_2\) \\
\ruleref{equiv_neg1} &
\(\varphi_1 \leftrightarrow \varphi_2 , \neg \varphi_1 , \neg \varphi_2\) \\
\ruleref{equiv_neg2} &
\(\varphi_1 \leftrightarrow \varphi_2 , \varphi_1 , \varphi_2\) \\
\ruleref{let} & Elimination of the 'let' operator. \\
\ruleref{distinct_elim} & Elimination of the 'distinct' operator. \\
\ruleref{nary_elim} & Elimination of n-ary application of operators. \\
\end{tabular}
\end{table}
\begin{table}[h!]
\caption{Simplification Rules. These rules represent typical operator-level
simplifications.}
\centering
\begin{tabular}{l l}
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. \\
\ruleref{not_simplify} & Simplification of a boolean negation. \\
\ruleref{implies_simplify} & Simplification of an implication. \\
\ruleref{equiv_simplify} & Simplification of an equivalence. \\
\ruleref{bool_simplify} & Simplification of combined boolean connectives. \\
\ruleref{ac_simp} & Simplification of nested disjunctions and conjunctions. \\
\ruleref{ite_simplify} & Simplification of if-then-else. \\
\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
\ruleref{onepoint} & The one-point rule. \\
\ruleref{qnt_join} & Joining of consecutive quantifiers. \\
\ruleref{qnt_rm_unused} & Removal of unused quantified variables. \\
\ruleref{eq_simplify} & Simplification of equalities. \\
\ruleref{div_simplify} & Simplification of division. \\
\ruleref{prod_simplify} & Simplification of products. \\
\ruleref{unary_minus_simplify} & Simplification of the unary minus. \\
\ruleref{minus_simplify} & Simplification of subtractions. \\
\ruleref{sum_simplify} & Simplification of sums. \\
\ruleref{comp_simplify} & Simplification of arithmetic comparisons. \\
\ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
\end{tabular}
\end{table}
%TODO: Implement this
%\begin{table}[h!]
%\caption{Recommended Rules. Some rules are very similar. This table lists
%which rule should be used in this case.}
%\centering
%\begin{tabular}{l l}
%Rule & Description \\
%\hline
%1 & 6 \\
%\end{tabular}
%\end{table}
%TODO: Add proof-relevante options
\clearpage
\section{List of Proof Rules}
\section*{Changelog}
\label{sec:rules}
The following lists all rules of Alethe.
\input{rule\string_list}
\section{Changelog}
\label{sec:changelog}
\addcontentsline{toc}{section}{Changelog}
\input{changelog}
\bibliographystyle{plain}
\bibliography{bib}
\clearpage
\section*{Index}
\addcontentsline{toc}{section}{Index}
\printindex
\bibliographystyle{plain}
\bibliography{publications}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: