diff --git a/.gitignore b/.gitignore
index 194387bce4623f21a38485d2643f49d60b20921d..3ffcffd18ca31756386647b80ee43fdd53340476 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,4 +8,5 @@ _minted-comments/
*.log
*.out
*.pdf
+*.pag
*.toc
diff --git a/publications/pxtp21/_minted-extended_abstract/default-pyg-prefix.pygstyle b/publications/pxtp21/_minted-extended_abstract/default-pyg-prefix.pygstyle
new file mode 100644
index 0000000000000000000000000000000000000000..cd0f51ac14bc0245adbc1b7a69a2d395b97b924d
--- /dev/null
+++ b/publications/pxtp21/_minted-extended_abstract/default-pyg-prefix.pygstyle
@@ -0,0 +1,101 @@
+
+\makeatletter
+\def\PYG@reset{\let\PYG@it=\relax \let\PYG@bf=\relax%
+ \let\PYG@ul=\relax \let\PYG@tc=\relax%
+ \let\PYG@bc=\relax \let\PYG@ff=\relax}
+\def\PYG@tok#1{\csname PYG@tok@#1\endcsname}
+\def\PYG@toks#1+{\ifx\relax#1\empty\else%
+ \PYG@tok{#1}\expandafter\PYG@toks\fi}
+\def\PYG@do#1{\PYG@bc{\PYG@tc{\PYG@ul{%
+ \PYG@it{\PYG@bf{\PYG@ff{#1}}}}}}}
+\def\PYG#1#2{\PYG@reset\PYG@toks#1+\relax+\PYG@do{#2}}
+
+\expandafter\def\csname PYG@tok@w\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.73,0.73}{##1}}}
+\expandafter\def\csname PYG@tok@c\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@cp\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.74,0.48,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@k\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@kp\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@kt\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.69,0.00,0.25}{##1}}}
+\expandafter\def\csname PYG@tok@o\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@ow\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
+\expandafter\def\csname PYG@tok@nb\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@nf\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PYG@tok@nc\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PYG@tok@nn\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PYG@tok@ne\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.82,0.25,0.23}{##1}}}
+\expandafter\def\csname PYG@tok@nv\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PYG@tok@no\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.53,0.00,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@nl\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.63,0.63,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@ni\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PYG@tok@na\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.49,0.56,0.16}{##1}}}
+\expandafter\def\csname PYG@tok@nt\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@nd\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
+\expandafter\def\csname PYG@tok@s\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@sd\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@si\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.73,0.40,0.53}{##1}}}
+\expandafter\def\csname PYG@tok@se\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.73,0.40,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@sr\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.40,0.53}{##1}}}
+\expandafter\def\csname PYG@tok@ss\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PYG@tok@sx\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@m\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@gh\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@gu\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.50,0.00,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@gd\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.63,0.00,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@gi\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.63,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@gr\endcsname{\def\PYG@tc##1{\textcolor[rgb]{1.00,0.00,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@ge\endcsname{\let\PYG@it=\textit}
+\expandafter\def\csname PYG@tok@gs\endcsname{\let\PYG@bf=\textbf}
+\expandafter\def\csname PYG@tok@gp\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@go\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.53,0.53,0.53}{##1}}}
+\expandafter\def\csname PYG@tok@gt\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.27,0.87}{##1}}}
+\expandafter\def\csname PYG@tok@err\endcsname{\def\PYG@bc##1{\setlength{\fboxsep}{0pt}\fcolorbox[rgb]{1.00,0.00,0.00}{1,1,1}{\strut ##1}}}
+\expandafter\def\csname PYG@tok@kc\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@kd\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@kn\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@kr\endcsname{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@bp\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PYG@tok@fm\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PYG@tok@vc\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PYG@tok@vg\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PYG@tok@vi\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PYG@tok@vm\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PYG@tok@sa\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@sb\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@sc\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@dl\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@s2\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@sh\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@s1\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PYG@tok@mb\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@mf\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@mh\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@mi\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@il\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@mo\endcsname{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PYG@tok@ch\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@cm\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@cpf\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@c1\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PYG@tok@cs\endcsname{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+
+\def\PYGZbs{\char`\\}
+\def\PYGZus{\char`\_}
+\def\PYGZob{\char`\{}
+\def\PYGZcb{\char`\}}
+\def\PYGZca{\char`\^}
+\def\PYGZam{\char`\&}
+\def\PYGZlt{\char`\<}
+\def\PYGZgt{\char`\>}
+\def\PYGZsh{\char`\#}
+\def\PYGZpc{\char`\%}
+\def\PYGZdl{\char`\$}
+\def\PYGZhy{\char`\-}
+\def\PYGZsq{\char`\'}
+\def\PYGZdq{\char`\"}
+\def\PYGZti{\char`\~}
+% for compatibility with earlier versions
+\def\PYGZat{@}
+\def\PYGZlb{[}
+\def\PYGZrb{]}
+\makeatother
+
diff --git a/publications/pxtp21/_minted-extended_abstract/listing1.pygtex b/publications/pxtp21/_minted-extended_abstract/listing1.pygtex
new file mode 100644
index 0000000000000000000000000000000000000000..f1a40c39fb1610a11879a889da21ae17050b92dd
--- /dev/null
+++ b/publications/pxtp21/_minted-extended_abstract/listing1.pygtex
@@ -0,0 +1,19 @@
+\begin{Verbatim}[commandchars=\\\{\}]
+ \PYG{p}{(}\PYG{k+kr}{assume} \PYG{n+nv}{a0} \PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{x} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{x}\PYG{p}{)))}
+ \PYG{p}{(}\PYG{k+kr}{anchor} \PYG{n+nf}{:step} \PYG{n+nv}{t1} \PYG{n+nf}{:args} \PYG{p}{(}\PYG{n+nb}{:= }\PYG{n+nv}{x} \PYG{n+nv}{vr}\PYG{p}{))}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t1.t1} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{= }\PYG{n+nv}{x} \PYG{n+nv}{vr}\PYG{p}{))} \PYG{n+nf}{:rule} \PYG{n+nv}{cong}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t1.t2} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{= }\PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{x}\PYG{p}{)} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{)))} \PYG{n+nf}{:rule} \PYG{n+nv}{cong}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t1} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{= }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{x} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{x}\PYG{p}{))}
+ \PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{))))} \PYG{n+nf}{:rule} \PYG{n+nv}{bind}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t2} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{not }\PYG{p}{(}\PYG{n+nb}{= }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{x}\PYG{p}{))}
+ \PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{))))}
+ \PYG{p}{(}\PYG{n+nb}{not }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{x}\PYG{p}{)))}
+ \PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{)))} \PYG{n+nf}{:rule} \PYG{n+nv}{equiv\PYGZus{}pos1}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t3} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{)))} \PYG{n+nf}{:premises} \PYG{p}{(}\PYG{n+nv}{a0} \PYG{n+nv}{t1} \PYG{n+nv}{t2}\PYG{p}{)} \PYG{n+nf}{:rule} \PYG{n+nv}{resolution}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{define\PYGZhy{}fun} \PYG{n+nv}{X} \PYG{p}{()} \PYG{n+nv}{A} \PYG{p}{(}\PYG{n+nv}{choice} \PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{)))}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t4} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{= }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{X}\PYG{p}{)))} \PYG{n+nf}{:rule} \PYG{n+nv}{sko\PYGZus{}ex}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t5} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nb}{not }\PYG{p}{(}\PYG{n+nb}{= }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{X}\PYG{p}{)))}
+ \PYG{p}{(}\PYG{n+nb}{not }\PYG{p}{(}\PYG{n+nb}{exists }\PYG{p}{((}\PYG{n+nv}{vr} \PYG{n+nv}{A}\PYG{p}{))} \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{vr}\PYG{p}{)))}
+ \PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{X}\PYG{p}{))} \PYG{n+nf}{:rule} \PYG{n+nv}{equiv\PYGZus{}pos1}\PYG{p}{)}
+ \PYG{p}{(}\PYG{k+kr}{step} \PYG{n+nv}{t6} \PYG{p}{(}\PYG{n+nb}{cl }\PYG{p}{(}\PYG{n+nv}{f} \PYG{n+nv}{X}\PYG{p}{))} \PYG{n+nf}{:premises} \PYG{p}{(}\PYG{n+nv}{t3} \PYG{n+nv}{t4} \PYG{n+nv}{t5}\PYG{p}{)} \PYG{n+nf}{:rule} \PYG{n+nv}{resolution}\PYG{p}{)}
+\end{Verbatim}
diff --git a/publications/pxtp21/_minted-extended_abstract/trac.pygstyle b/publications/pxtp21/_minted-extended_abstract/trac.pygstyle
new file mode 100644
index 0000000000000000000000000000000000000000..85929ff13f12724880889cf52f61700fb9facd0a
--- /dev/null
+++ b/publications/pxtp21/_minted-extended_abstract/trac.pygstyle
@@ -0,0 +1,99 @@
+
+\makeatletter
+\def\PYGtrac@reset{\let\PYGtrac@it=\relax \let\PYGtrac@bf=\relax%
+ \let\PYGtrac@ul=\relax \let\PYGtrac@tc=\relax%
+ \let\PYGtrac@bc=\relax \let\PYGtrac@ff=\relax}
+\def\PYGtrac@tok#1{\csname PYGtrac@tok@#1\endcsname}
+\def\PYGtrac@toks#1+{\ifx\relax#1\empty\else%
+ \PYGtrac@tok{#1}\expandafter\PYGtrac@toks\fi}
+\def\PYGtrac@do#1{\PYGtrac@bc{\PYGtrac@tc{\PYGtrac@ul{%
+ \PYGtrac@it{\PYGtrac@bf{\PYGtrac@ff{#1}}}}}}}
+\def\PYGtrac#1#2{\PYGtrac@reset\PYGtrac@toks#1+\relax+\PYGtrac@do{#2}}
+
+\expandafter\def\csname PYGtrac@tok@w\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.73,0.73}{##1}}}
+\expandafter\def\csname PYGtrac@tok@c\endcsname{\let\PYGtrac@it=\textit\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@cp\endcsname{\let\PYGtrac@bf=\textbf\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@cs\endcsname{\let\PYGtrac@bf=\textbf\let\PYGtrac@it=\textit\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@o\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@s\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sr\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.50,0.50,0.00}{##1}}}
+\expandafter\def\csname PYGtrac@tok@m\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@k\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@kt\endcsname{\let\PYGtrac@bf=\textbf\def\PYGtrac@tc##1{\textcolor[rgb]{0.27,0.33,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@nb\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@nf\endcsname{\let\PYGtrac@bf=\textbf\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.00,0.00}{##1}}}
+\expandafter\def\csname PYGtrac@tok@nc\endcsname{\let\PYGtrac@bf=\textbf\def\PYGtrac@tc##1{\textcolor[rgb]{0.27,0.33,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@ne\endcsname{\let\PYGtrac@bf=\textbf\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.00,0.00}{##1}}}
+\expandafter\def\csname PYGtrac@tok@nn\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.33,0.33,0.33}{##1}}}
+\expandafter\def\csname PYGtrac@tok@nv\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@no\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@nt\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@na\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@ni\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.50,0.00,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@gh\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@gu\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.67,0.67,0.67}{##1}}}
+\expandafter\def\csname PYGtrac@tok@gd\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.00,0.00}{##1}}\def\PYGtrac@bc##1{\setlength{\fboxsep}{0pt}\colorbox[rgb]{1.00,0.87,0.87}{\strut ##1}}}
+\expandafter\def\csname PYGtrac@tok@gi\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.00,0.00}{##1}}\def\PYGtrac@bc##1{\setlength{\fboxsep}{0pt}\colorbox[rgb]{0.87,1.00,0.87}{\strut ##1}}}
+\expandafter\def\csname PYGtrac@tok@gr\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.67,0.00,0.00}{##1}}}
+\expandafter\def\csname PYGtrac@tok@ge\endcsname{\let\PYGtrac@it=\textit}
+\expandafter\def\csname PYGtrac@tok@gs\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@gp\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.33,0.33,0.33}{##1}}}
+\expandafter\def\csname PYGtrac@tok@go\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.53,0.53,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@gt\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.67,0.00,0.00}{##1}}}
+\expandafter\def\csname PYGtrac@tok@err\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.65,0.09,0.09}{##1}}\def\PYGtrac@bc##1{\setlength{\fboxsep}{0pt}\colorbox[rgb]{0.89,0.82,0.82}{\strut ##1}}}
+\expandafter\def\csname PYGtrac@tok@kc\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@kd\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@kn\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@kp\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@kr\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@bp\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@fm\endcsname{\let\PYGtrac@bf=\textbf\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.00,0.00}{##1}}}
+\expandafter\def\csname PYGtrac@tok@vc\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@vg\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@vi\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@vm\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.50,0.50}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sa\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sb\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sc\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@dl\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sd\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@s2\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@se\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sh\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@si\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@sx\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@s1\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@ss\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.73,0.53,0.27}{##1}}}
+\expandafter\def\csname PYGtrac@tok@mb\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@mf\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@mh\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@mi\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@il\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@mo\endcsname{\def\PYGtrac@tc##1{\textcolor[rgb]{0.00,0.60,0.60}{##1}}}
+\expandafter\def\csname PYGtrac@tok@ow\endcsname{\let\PYGtrac@bf=\textbf}
+\expandafter\def\csname PYGtrac@tok@ch\endcsname{\let\PYGtrac@it=\textit\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@cm\endcsname{\let\PYGtrac@it=\textit\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@cpf\endcsname{\let\PYGtrac@it=\textit\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.53}{##1}}}
+\expandafter\def\csname PYGtrac@tok@c1\endcsname{\let\PYGtrac@it=\textit\def\PYGtrac@tc##1{\textcolor[rgb]{0.60,0.60,0.53}{##1}}}
+
+\def\PYGtracZbs{\char`\\}
+\def\PYGtracZus{\char`\_}
+\def\PYGtracZob{\char`\{}
+\def\PYGtracZcb{\char`\}}
+\def\PYGtracZca{\char`\^}
+\def\PYGtracZam{\char`\&}
+\def\PYGtracZlt{\char`\<}
+\def\PYGtracZgt{\char`\>}
+\def\PYGtracZsh{\char`\#}
+\def\PYGtracZpc{\char`\%}
+\def\PYGtracZdl{\char`\$}
+\def\PYGtracZhy{\char`\-}
+\def\PYGtracZsq{\char`\'}
+\def\PYGtracZdq{\char`\"}
+\def\PYGtracZti{\char`\~}
+% for compatibility with earlier versions
+\def\PYGtracZat{@}
+\def\PYGtracZlb{[}
+\def\PYGtracZrb{]}
+\makeatother
+
diff --git a/publications/pxtp21/abstract b/publications/pxtp21/abstract
new file mode 100644
index 0000000000000000000000000000000000000000..db7a43200470027feab57d682e78d5673bf9df43
--- /dev/null
+++ b/publications/pxtp21/abstract
@@ -0,0 +1,13 @@
+PxTP-7
+
+Beyond veriT: Towards a Generic SMT Proof Format (Extended Abstract)
+
+The first iteration of the proof format used by veriT was presented ten
+years ago at the first PxTP workshop in 2011. Since then the format
+has matured, and proofs generated by veriT are used withing multiple
+applications. Indeed, it is quickly growing beyond the confinements
+of one singular prover. We review the challenges we encountered with
+using the format in practice, and also discuss the likely problems that
+will arise when another solver will use the format. We also present
+our work on a specification for the format.
+
diff --git a/publications/pxtp21/breakurl.sty b/publications/pxtp21/breakurl.sty
new file mode 100644
index 0000000000000000000000000000000000000000..0bf5b06e8fe39fb3f1e2a8179bb69c9281aaf38d
--- /dev/null
+++ b/publications/pxtp21/breakurl.sty
@@ -0,0 +1,309 @@
+%%
+%% This is file `breakurl.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% breakurl.dtx (with options: `package')
+%%
+%% This is a generated file.
+%%
+%% Copyright (C) 2005 by Vilar Camara Neto.
+%%
+%% This file may be distributed and/or modified under the
+%% conditions of the LaTeX Project Public License, either
+%% version 1.2 of this license or (at your option) any later
+%% version. The latest version of this license is in:
+%%
+%% http://www.latex-project.org/lppl.txt
+%%
+%% and version 1.2 or later is part of all distributions of
+%% LaTeX version 1999/12/01 or later.
+%%
+%% Currently this work has the LPPL maintenance status "maintained".
+%%
+%% The Current Maintainer of this work is Vilar Camara Neto.
+%%
+%% This work consists of the files breakurl.dtx and
+%% breakurl.ins and the derived file breakurl.sty.
+%%
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{breakurl}
+ [2009/01/24 v1.30 Breakable hyperref URLs]
+
+
+\RequirePackage{xkeyval}
+\RequirePackage{ifpdf}
+
+\ifpdf
+ % Dummy package options
+ \DeclareOptionX{preserveurlmacro}{}
+ \DeclareOptionX{hyphenbreaks}{}
+ \DeclareOptionX{vertfit}{}
+ \ProcessOptionsX\relax
+
+ \PackageWarning{breakurl}{%
+ You are using breakurl while processing via pdflatex.\MessageBreak
+ \string\burl\space will be just a synonym of \string\url.\MessageBreak}
+ \DeclareRobustCommand{\burl}{\url}
+ \DeclareRobustCommand*{\burlalt}{\hyper@normalise\burl@alt}
+ \def\burl@alt#1#2{\hyper@linkurl{\Hurl{#1}}{#2}}
+ \expandafter\endinput
+\fi
+
+\@ifpackageloaded{hyperref}{}{%
+ \PackageError{breakurl}{The breakurl depends on hyperref package}%
+ {I can't do anything. Please type X <return>, edit the source file%
+ \MessageBreak
+ and add \string\usepackage\string{hyperref\string} before
+ \string\usepackage\string{breakurl\string}.}
+ \endinput
+}
+
+\newif\if@preserveurlmacro\@preserveurlmacrofalse
+\newif\if@burl@fitstrut\@burl@fitstrutfalse
+\newif\if@burl@fitglobal\@burl@fitglobalfalse
+
+\newtoks\burl@toks
+
+\let\burl@charlistbefore\empty
+\let\burl@charlistafter\empty
+
+\def\burl@addtocharlistbefore{\g@addto@macro\burl@charlistbefore}
+\def\burl@addtocharlistafter{\g@addto@macro\burl@charlistafter}
+
+\bgroup
+ \catcode`\&=12\relax
+ \hyper@normalise\burl@addtocharlistbefore{%}
+ \hyper@normalise\burl@addtocharlistafter{:/.?#&_,;!}
+\egroup
+
+\def\burl@growmif#1#2{%
+ \g@addto@macro\burl@mif{\def\burl@ttt{#1}\ifx\burl@ttt\@nextchar#2\else}%
+}
+\def\burl@growmfi{%
+ \g@addto@macro\burl@mfi{\fi}%
+}
+\def\burl@defifstructure{%
+ \let\burl@mif\empty
+ \let\burl@mfi\empty
+ \expandafter\@tfor\expandafter\@nextchar\expandafter:\expandafter=%
+ \burl@charlistbefore\do{%
+ \expandafter\burl@growmif\@nextchar\@burl@breakbeforetrue
+ \burl@growmfi
+ }%
+ \expandafter\@tfor\expandafter\@nextchar\expandafter:\expandafter=%
+ \burl@charlistafter\do{%
+ \expandafter\burl@growmif\@nextchar\@burl@breakaftertrue
+ \burl@growmfi
+ }%
+}
+
+\AtEndOfPackage{\burl@defifstructure}
+
+\def\burl@setvertfit#1{%
+ \lowercase{\def\burl@temp{#1}}%
+ \def\burl@opt{local}\ifx\burl@temp\burl@opt
+ \@burl@fitstrutfalse\@burl@fitglobalfalse
+ \else\def\burl@opt{strut}\ifx\burl@temp\burl@opt
+ \@burl@fitstruttrue\@burl@fitglobalfalse
+ \else\def\burl@opt{global}\ifx\burl@temp\burl@opt
+ \@burl@fitstrutfalse\@burl@fitglobaltrue
+ \else
+ \PackageWarning{breakurl}{Unrecognized vertfit option `\burl@temp'.%
+ \MessageBreak
+ Adopting default `local'}
+ \@burl@fitstrutfalse\@burl@fitglobalfalse
+ \fi\fi\fi
+}
+
+\DeclareOptionX{preserveurlmacro}{\@preserveurlmacrotrue}
+\DeclareOptionX{hyphenbreaks}{%
+ \bgroup
+ \catcode`\&=12\relax
+ \hyper@normalise\burl@addtocharlistafter{-}%
+ \egroup
+}
+\DeclareOptionX{vertfit}[local]{\burl@setvertfit{#1}}
+
+\ProcessOptionsX\relax
+
+\def\burl@hyper@linkurl#1#2{%
+ \begingroup
+ \hyper@chars
+ \burl@condpdflink{#1}%
+ \endgroup
+}
+
+\def\burl@condpdflink#1{%
+ \literalps@out{
+ /burl@bordercolor {\@urlbordercolor} def
+ /burl@border {\@pdfborder} def
+ }%
+ \if@burl@fitstrut
+ \sbox\pdf@box{#1\strut}%
+ \else\if@burl@fitglobal
+ \sbox\pdf@box{\burl@url}%
+ \else
+ \sbox\pdf@box{#1}%
+ \fi\fi
+ \dimen@\ht\pdf@box\dimen@ii\dp\pdf@box
+ \sbox\pdf@box{#1}%
+ \ifdim\dimen@ii=\z@
+ \literalps@out{BU.SS}%
+ \else
+ \lower\dimen@ii\hbox{\literalps@out{BU.SS}}%
+ \fi
+ \ifHy@breaklinks\unhbox\else\box\fi\pdf@box
+ \ifdim\dimen@=\z@
+ \literalps@out{BU.SE}%
+ \else
+ \raise\dimen@\hbox{\literalps@out{BU.SE}}%
+ \fi
+ \pdf@addtoksx{H.B}%
+}
+
+\DeclareRobustCommand*{\burl}{%
+ \leavevmode
+ \begingroup
+ \let\hyper@linkurl=\burl@hyper@linkurl
+ \catcode`\&=12\relax
+ \hyper@normalise\burl@
+}
+
+\DeclareRobustCommand*{\burlalt}{%
+ \begingroup
+ \let\hyper@linkurl=\burl@hyper@linkurl
+ \catcode`\&=12\relax
+ \hyper@normalise\burl@alt
+}
+
+\newif\if@burl@breakbefore
+\newif\if@burl@breakafter
+\newif\if@burl@prevbreakafter
+
+\bgroup
+\catcode`\&=12\relax
+\gdef\burl@#1{%
+ \def\burl@url{#1}%
+ \def\burl@urltext{#1}%
+ \burl@doit
+}
+
+\gdef\burl@alt#1{%
+ \def\burl@url{#1}%
+ \hyper@normalise\burl@@alt
+}
+\gdef\burl@@alt#1{%
+ \def\burl@urltext{#1}%
+ \burl@doit
+}
+
+\gdef\burl@doit{%
+ \burl@toks{}%
+ \let\burl@UrlRight\UrlRight
+ \let\UrlRight\empty
+ \@burl@prevbreakafterfalse
+ \@ifundefined{@urlcolor}{\Hy@colorlink\@linkcolor}{\Hy@colorlink\@urlcolor}%
+ \expandafter\@tfor\expandafter\@nextchar\expandafter:\expandafter=%
+ \burl@urltext\do{%
+ \if@burl@breakafter\@burl@prevbreakaftertrue
+ \else\@burl@prevbreakafterfalse\fi
+ \@burl@breakbeforefalse
+ \@burl@breakafterfalse
+ \expandafter\burl@mif\burl@mfi
+ \if@burl@breakbefore
+ % Breakable if the current char is in the `can break before' list
+ \burl@flush\linebreak[0]%
+ \else
+ \if@burl@prevbreakafter
+ \if@burl@breakafter\else
+ % Breakable if the current char is not in any of the `can break'
+ % lists, but the previous is in the `can break after' list.
+ % This mechanism accounts for sequences of `break after' characters,
+ % where a break is allowed only after the last one
+ \burl@flush\linebreak[0]%
+ \fi
+ \fi
+ \fi
+ \expandafter\expandafter\expandafter\burl@toks
+ \expandafter\expandafter\expandafter{%
+ \expandafter\the\expandafter\burl@toks\@nextchar}%
+ }%
+ \let\UrlRight\burl@UrlRight
+ \burl@flush
+ \literalps@out{BU.E}%
+ \Hy@endcolorlink
+ \endgroup
+}
+\egroup
+
+\def\the@burl@toks{\the\burl@toks}
+
+\def\burl@flush{%
+ \expandafter\def\expandafter\burl@toks@def\expandafter{\the\burl@toks}%
+ \literalps@out{/BU.L (\burl@url) def}%
+ \hyper@linkurl{\expandafter\Hurl\expandafter{\burl@toks@def}}{\burl@url}%
+ \global\burl@toks{}%
+ \let\UrlLeft\empty
+}%
+
+\if@preserveurlmacro\else\let\url\burl\let\urlalt\burlalt\fi
+
+\AtBeginDvi{%
+ \headerps@out{%
+ /burl@stx null def
+ /BU.S {
+ /burl@stx null def
+ } def
+ /BU.SS {
+ currentpoint
+ /burl@lly exch def
+ /burl@llx exch def
+ burl@stx null ne {burl@endx burl@llx ne {BU.FL BU.S} if} if
+ burl@stx null eq {
+ burl@llx dup /burl@stx exch def /burl@endx exch def
+ burl@lly dup /burl@boty exch def /burl@topy exch def
+ } if
+ burl@lly burl@boty gt {/burl@boty burl@lly def} if
+ } def
+ /BU.SE {
+ currentpoint
+ /burl@ury exch def
+ dup /burl@urx exch def /burl@endx exch def
+ burl@ury burl@topy lt {/burl@topy burl@ury def} if
+ } def
+ /BU.E {
+ BU.FL
+ } def
+ /BU.FL {
+ burl@stx null ne {BU.DF} if
+ } def
+ /BU.DF {
+ BU.BB
+ [ /H /I /Border [burl@border] /Color [burl@bordercolor]
+ /Action << /Subtype /URI /URI BU.L >> /Subtype /Link BU.B /ANN pdfmark
+ /burl@stx null def
+ } def
+ /BU.BB {
+ burl@stx HyperBorder sub /burl@stx exch def
+ burl@endx HyperBorder add /burl@endx exch def
+ burl@boty HyperBorder add /burl@boty exch def
+ burl@topy HyperBorder sub /burl@topy exch def
+ } def
+ /BU.B {
+ /Rect[burl@stx burl@boty burl@endx burl@topy]
+ } def
+ /eop where {
+ begin
+ /@ldeopburl /eop load def
+ /eop { SDict begin BU.FL end @ldeopburl } def
+ end
+ } {
+ /eop { SDict begin BU.FL end } def
+ } ifelse
+ }%
+}
+\endinput
+%%
+%% End of file `breakurl.sty'.
diff --git a/publications/pxtp21/eptcs.bst b/publications/pxtp21/eptcs.bst
new file mode 100644
index 0000000000000000000000000000000000000000..86e0e1be13e3e1880db785d3f563b0a34ec45e04
--- /dev/null
+++ b/publications/pxtp21/eptcs.bst
@@ -0,0 +1,1425 @@
+%%
+%% This is file `eptcs.bst',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% merlin.mbs (with options: `vonx,ed-au,dt-beg,yr-par,xmth,yrp-col,tit-it,atit-u,volp-com,jwdpg,pp-last,num-xser,ser-vol,jnm-x,pre-edn,doi,blknt,pp,xedn,amper,and-xcom,etal-xc,url,url-blk,bibinfo,nfss,')
+%% ----------------------------------------
+%% *** Stylefile for EPTCS ***
+%%
+%% Copyright 1994-2004 Patrick W Daly
+ % ===============================================================
+ % NOTICE:
+ % This bibliographic style (bst) file has been generated from one or
+ % more master bibliographic style (mbs) files, listed above.
+ % Subsequently it has been edited by hand by Rob van Glabbeek
+ %
+ % This file can be redistributed and/or modified under the terms
+ % of the LaTeX Project Public License Distributed from CTAN
+ % archives in directory macros/latex/base/lppl.txt; either
+ % version 1 of the License, or any later version.
+ % ===============================================================
+ % Name and version information of the main mbs file:
+ % \ProvidesFile{merlin.mbs}[2004/02/09 4.13 (PWD, AO, DPC)]
+ % For use with BibTeX version 0.99a or later
+ %-------------------------------------------------------------------
+ % This bibliography style file is intended for texts in ENGLISH
+ % This is a numerical citation style, and as such is standard LaTeX.
+ % It requires no extra package to interface to the main text.
+ % The form of the \bibitem entries is
+ % \bibitem{key}...
+ % Usage of \cite is as follows:
+ % \cite{key} ==>> [#]
+ % \cite[chap. 2]{key} ==>> [#, chap. 2]
+ % where # is a number determined by the ordering in the reference list.
+ % The order in the reference list is alphabetical by authors.
+ %---------------------------------------------------------------------
+
+ENTRY
+ { address
+ author
+ booktitle
+ chapter
+ doi
+ edition
+ editor
+ eid
+ howpublished
+ institution
+ journal
+ key
+ note
+ number
+ organization
+ pages
+ publisher
+ school
+ series
+ title
+ type
+ url
+ ee
+ volume
+ year
+ }
+ {}
+ { label }
+INTEGERS { output.state before.all mid.sentence after.sentence after.block }
+FUNCTION {init.state.consts}
+{ #0 'before.all :=
+ #1 'mid.sentence :=
+ #2 'after.sentence :=
+ #3 'after.block :=
+}
+STRINGS { s t}
+FUNCTION {output.nonnull}
+{ 's :=
+ output.state mid.sentence =
+ { ", " * write$ }
+ { output.state after.block =
+ { add.period$ write$
+ newline$
+ "\newblock " write$
+ }
+ { output.state before.all =
+ 'write$
+ { add.period$ " " * write$ }
+ if$
+ }
+ if$
+ mid.sentence 'output.state :=
+ }
+ if$
+ s
+}
+FUNCTION {output}
+{ duplicate$ empty$
+ 'pop$
+ 'output.nonnull
+ if$
+}
+FUNCTION {output.check}
+{ 't :=
+ duplicate$ empty$
+ { pop$ "empty " t * " in " * cite$ * warning$ }
+ 'output.nonnull
+ if$
+}
+FUNCTION {fin.entry}
+{ add.period$
+ write$
+ newline$
+}
+
+FUNCTION {new.block}
+{ output.state before.all =
+ 'skip$
+ { after.block 'output.state := }
+ if$
+}
+FUNCTION {new.sentence}
+{ output.state after.block =
+ 'skip$
+ { output.state before.all =
+ 'skip$
+ { after.sentence 'output.state := }
+ if$
+ }
+ if$
+}
+FUNCTION {add.blank}
+{ " " * before.all 'output.state :=
+}
+
+FUNCTION {date.block}
+{
+ ":" *
+ add.blank
+}
+
+FUNCTION {not}
+{ { #0 }
+ { #1 }
+ if$
+}
+FUNCTION {and}
+{ 'skip$
+ { pop$ #0 }
+ if$
+}
+FUNCTION {or}
+{ { pop$ #1 }
+ 'skip$
+ if$
+}
+FUNCTION {new.block.checka}
+{ empty$
+ 'skip$
+ 'new.block
+ if$
+}
+FUNCTION {new.block.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.block
+ if$
+}
+FUNCTION {new.sentence.checka}
+{ empty$
+ 'skip$
+ 'new.sentence
+ if$
+}
+FUNCTION {new.sentence.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.sentence
+ if$
+}
+FUNCTION {field.or.null}
+{ duplicate$ empty$
+ { pop$ "" }
+ 'skip$
+ if$
+}
+FUNCTION {emphasize}
+{ duplicate$ empty$
+ { pop$ "" }
+ { "\emph{" swap$ * "}" * }
+ if$
+}
+FUNCTION {slant}
+{ duplicate$ empty$
+ { pop$ "" }
+ { "{\sl " swap$ * "}" * }
+ if$
+}
+FUNCTION {tie.or.space.prefix}
+{ duplicate$ text.length$ #3 <
+ { "~" }
+ { " " }
+ if$
+ swap$
+}
+
+FUNCTION {capitalize}
+{ "u" change.case$ "t" change.case$ }
+
+FUNCTION {space.word}
+{ " " swap$ * " " * }
+ % Here are the language-specific definitions for explicit words.
+ % Each function has a name bbl.xxx where xxx is the English word.
+ % The language selected here is ENGLISH
+FUNCTION {bbl.and}
+{ "and"}
+
+FUNCTION {bbl.etal}
+{ "et~al." }
+
+FUNCTION {bbl.editors}
+{ "editors" }
+
+FUNCTION {bbl.editor}
+{ "editor" }
+
+FUNCTION {bbl.edby}
+{ "edited by" }
+
+FUNCTION {bbl.edition}
+{ "edition" }
+
+FUNCTION {bbl.volume}
+{ "" }
+
+FUNCTION {bbl.of}
+{ "of" }
+
+FUNCTION {bbl.nr}
+{ "no." }
+
+FUNCTION {bbl.in}
+{ "in" }
+
+FUNCTION {bbl.pages}
+{ "pp." }
+
+FUNCTION {bbl.page}
+{ "p." }
+
+FUNCTION {bbl.chapter}
+{ "chapter" }
+
+FUNCTION {bbl.techrep}
+{ "Technical Report" }
+
+FUNCTION {bbl.mthesis}
+{ "Master's thesis" }
+
+FUNCTION {bbl.phdthesis}
+{ "Ph.D. thesis" }
+
+MACRO {jan} {"January"}
+
+MACRO {feb} {"February"}
+
+MACRO {mar} {"March"}
+
+MACRO {apr} {"April"}
+
+MACRO {may} {"May"}
+
+MACRO {jun} {"June"}
+
+MACRO {jul} {"July"}
+
+MACRO {aug} {"August"}
+
+MACRO {sep} {"September"}
+
+MACRO {oct} {"October"}
+
+MACRO {nov} {"November"}
+
+MACRO {dec} {"December"}
+
+MACRO {acmcs} {"ACM Computing Surveys"}
+
+MACRO {acta} {"Acta Informatica"}
+
+MACRO {cacm} {"Communications of the ACM"}
+
+MACRO {eptcs} {"Electronic Proceedings in Computer Science"}
+
+MACRO {ibmjrd} {"IBM Journal of Research and Development"}
+
+MACRO {ibmsj} {"IBM Systems Journal"}
+
+MACRO {ieeese} {"IEEE Transactions on Software Engineering"}
+
+MACRO {ieeetc} {"IEEE Transactions on Computers"}
+
+MACRO {ieeetcad}
+ {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}
+
+MACRO {ipl} {"Information Processing Letters"}
+
+MACRO {jacm} {"Journal of the ACM"}
+
+MACRO {jcss} {"Journal of Computer and System Sciences"}
+
+MACRO {scp} {"Science of Computer Programming"}
+
+MACRO {sicomp} {"SIAM Journal on Computing"}
+
+MACRO {tocs} {"ACM Transactions on Computer Systems"}
+
+MACRO {tods} {"ACM Transactions on Database Systems"}
+
+MACRO {tog} {"ACM Transactions on Graphics"}
+
+MACRO {toms} {"ACM Transactions on Mathematical Software"}
+
+MACRO {toois} {"ACM Transactions on Office Information Systems"}
+
+MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"}
+
+MACRO {tcs} {"Theoretical Computer Science"}
+FUNCTION {bibinfo.check}
+{ swap$
+ duplicate$ missing$
+ {
+ pop$ pop$
+ ""
+ }
+ { duplicate$ empty$
+ {
+ swap$ pop$
+ }
+ { swap$
+ "\bibinfo{" swap$ * "}{" * swap$ * "}" *
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {bibinfo.warn}
+{ swap$
+ duplicate$ missing$
+ {
+ swap$ "missing " swap$ * " in " * cite$ * warning$ pop$
+ ""
+ }
+ { duplicate$ empty$
+ {
+ swap$ "empty " swap$ * " in " * cite$ * warning$
+ }
+ { swap$
+ "\bibinfo{" swap$ * "}{" * swap$ * "}" *
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {either.or.check}
+{ empty$
+ 'pop$
+ { "can't use both " swap$ * " fields in " * cite$ * warning$ }
+ if$
+}
+FUNCTION {format.ee}
+{ ee empty$
+ { "" }
+ { "\urlprefix\url{" ee * "}" * }
+ if$
+}
+FUNCTION {format.url}
+{ url empty$
+ { format.ee }
+ { "\urlprefix\url{" url * "}" *
+ "ee and url" ee either.or.check
+ }
+ if$
+}
+
+STRINGS { bibinfo}
+INTEGERS { nameptr namesleft numnames }
+
+FUNCTION {format.names}
+{ 'bibinfo :=
+ duplicate$ empty$ 'skip$ {
+ 's :=
+ "" 't :=
+ #1 'nameptr :=
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { s nameptr
+ "{ff~}\surnamestart {vv~}{ll}\surnameend{, jj}"
+ format.name$
+ bibinfo bibinfo.check
+ 't :=
+ nameptr #1 >
+ {
+ namesleft #1 >
+ { ", " * t * }
+ {
+ s nameptr "{ll}" format.name$ duplicate$ "others" =
+ { 't := }
+ { pop$ }
+ if$
+ t "others" =
+ {
+ " " * bbl.etal *
+ }
+ {
+ "\&"
+ space.word * t *
+ }
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+ } if$
+}
+FUNCTION {format.names.ed}
+{
+ format.names
+}
+FUNCTION {format.authors}
+{ author "author" format.names
+}
+FUNCTION {get.bbl.editor}
+{ editor num.names$ #1 > 'bbl.editors 'bbl.editor if$ }
+
+FUNCTION {format.editors}
+{ editor "editor" format.names duplicate$ empty$ 'skip$
+ {
+ "," *
+ " " *
+ get.bbl.editor
+ *
+ }
+ if$
+}
+FUNCTION {format.doi}
+{ doi
+ duplicate$ empty$ 'skip$
+ {
+ "\doi{" swap$ * "}" *
+ }
+ if$
+}
+FUNCTION {format.note}
+{
+ note empty$
+ { "" }
+ { note #1 #1 substring$
+ duplicate$ "{" =
+ 'skip$
+ { output.state mid.sentence =
+ { "l" }
+ { "u" }
+ if$
+ change.case$
+ }
+ if$
+ note #2 global.max$ substring$ * "note" bibinfo.check
+ }
+ if$
+}
+
+FUNCTION {format.title}
+{ title
+ "title" bibinfo.check
+ duplicate$ empty$ 'skip$
+ {
+ emphasize
+ }
+ if$
+}
+FUNCTION {output.bibitem}
+{ newline$
+ "\bibitemdeclare{" type$ "}{" cite$ "}" * * * * write$ newline$
+ "\bibitem{" write$
+ cite$ write$
+ "}" write$
+ newline$
+ ""
+ before.all 'output.state :=
+}
+
+FUNCTION {n.dashify}
+{
+ 't :=
+ ""
+ { t empty$ not }
+ { t #1 #1 substring$ "-" =
+ { t #1 #2 substring$ "--" = not
+ { "--" *
+ t #2 global.max$ substring$ 't :=
+ }
+ { { t #1 #1 substring$ "-" = }
+ { "-" *
+ t #2 global.max$ substring$ 't :=
+ }
+ while$
+ }
+ if$
+ }
+ { t #1 #1 substring$ *
+ t #2 global.max$ substring$ 't :=
+ }
+ if$
+ }
+ while$
+}
+
+FUNCTION {word.in}
+{ bbl.in capitalize
+ " " * }
+
+FUNCTION {format.date}
+{
+ ""
+ duplicate$ empty$
+ year "year" bibinfo.check duplicate$ empty$
+ { swap$ 'skip$
+ { "there's a month but no year in " cite$ * warning$ }
+ if$
+ *
+ }
+ { swap$ 'skip$
+ {
+ swap$
+ " " * swap$
+ }
+ if$
+ *
+ }
+ if$
+ duplicate$ empty$
+ 'skip$
+ {
+ before.all 'output.state :=
+ " (" swap$ * ")" *
+ }
+ if$
+}
+FUNCTION {format.btitle}
+{ title "title" bibinfo.check
+ duplicate$ empty$ 'skip$
+ {
+ emphasize
+ }
+ if$
+}
+FUNCTION {volume.or.number}
+{ volume missing$
+ { number }
+ { volume }
+ if$
+}
+FUNCTION {format.volume.number.series}
+{ volume.or.number missing$
+ { series "series" bibinfo.check field.or.null }
+ { series empty$
+ { volume.or.number "volume" bibinfo.check }
+ { volume.or.number tie.or.space.prefix "volume" bibinfo.check *
+ series "series" bibinfo.check
+ duplicate$ empty$ 'pop$
+ { slant swap$ * }
+ if$
+ }
+ if$
+ volume missing$
+ 'skip$
+ { "volume and number" number either.or.check }
+ if$
+ }
+ if$
+}
+FUNCTION {format.edition}
+{ edition duplicate$ empty$ 'skip$
+ {
+ output.state mid.sentence =
+ { "l" }
+ { "t" }
+ if$ change.case$
+ "edition" bibinfo.check
+ " " * bbl.edition *
+ }
+ if$
+}
+INTEGERS { multiresult }
+FUNCTION {multi.page.check}
+{ 't :=
+ #0 'multiresult :=
+ { multiresult not
+ t empty$ not
+ and
+ }
+ { t #1 #1 substring$
+ duplicate$ "-" =
+ swap$ duplicate$ "," =
+ swap$ "+" =
+ or or
+ { #1 'multiresult := }
+ { t #2 global.max$ substring$ 't := }
+ if$
+ }
+ while$
+ multiresult
+}
+FUNCTION {format.pages}
+{ pages duplicate$ empty$ 'skip$
+ { duplicate$ multi.page.check
+ {
+ bbl.pages swap$
+ n.dashify
+ }
+ {
+ bbl.page swap$
+ }
+ if$
+ tie.or.space.prefix
+ "pages" bibinfo.check
+ * *
+ }
+ if$
+}
+FUNCTION {format.journal.pages}
+{ pages duplicate$ empty$ 'pop$
+ { swap$ duplicate$ empty$
+ { pop$ pop$ format.pages }
+ {
+ ", " *
+ swap$
+ n.dashify
+ pages multi.page.check
+ 'bbl.pages
+ 'bbl.page
+ if$
+ swap$ tie.or.space.prefix
+ "pages" bibinfo.check
+ * *
+ *
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.journal.eid}
+{ eid "eid" bibinfo.check
+ duplicate$ empty$ 'pop$
+ { swap$ duplicate$ empty$ 'skip$
+ {
+ ":" *
+ }
+ if$
+ swap$ *
+ "eid and pages" pages either.or.check
+ }
+ if$
+}
+FUNCTION {format.vol.num}
+{ volume field.or.null
+ duplicate$ empty$ 'skip$
+ {
+ "volume" bibinfo.check
+ }
+ if$
+ number "number" bibinfo.check duplicate$ empty$ 'skip$
+ {
+ swap$ duplicate$ empty$
+ { "there's a number but no volume in " cite$ * warning$ }
+ 'skip$
+ if$
+ swap$
+ "(" swap$ * ")" *
+ }
+ if$ *
+ duplicate$ empty$ 'skip$
+ {
+ swap$ duplicate$ empty$ 'skip$
+ {
+ " " *
+ }
+ if$ swap$
+ }
+ if$ *
+}
+
+FUNCTION {format.chapter}
+{ chapter empty$
+ { "" }
+ { type empty$
+ { bbl.chapter }
+ { type "l" change.case$
+ "type" bibinfo.check
+ }
+ if$
+ chapter tie.or.space.prefix
+ "chapter" bibinfo.check
+ * *
+ }
+ if$
+}
+
+FUNCTION {format.booktitle}
+{
+ booktitle "booktitle" bibinfo.check
+ slant
+}
+FUNCTION {format.in.ed.booktitle}
+{ format.booktitle duplicate$ empty$ 'skip$
+ { bbl.in capitalize
+ editor "editor" format.names.ed duplicate$ empty$ 'pop$
+ {
+ " " swap$ *
+ ", " *
+ get.bbl.editor *
+ * }
+ if$
+ ": " *
+ swap$ *
+ }
+ if$
+}
+FUNCTION {empty.misc.check}
+{ author empty$ title empty$ howpublished empty$
+ year empty$ note empty$
+ and and and and
+ key empty$ not and
+ { "all relevant fields are empty in " cite$ * warning$ }
+ 'skip$
+ if$
+}
+FUNCTION {format.thesis.type}
+{ type duplicate$ empty$
+ 'pop$
+ { swap$ pop$
+ "t" change.case$ "type" bibinfo.check
+ }
+ if$
+}
+FUNCTION {format.tr.number}
+{ number "number" bibinfo.check
+ type duplicate$ empty$
+ { pop$ bbl.techrep }
+ 'skip$
+ if$
+ "type" bibinfo.check
+ swap$ duplicate$ empty$
+ { pop$ "t" change.case$ }
+ { tie.or.space.prefix * * }
+ if$
+}
+FUNCTION {format.article.crossref}
+{
+ key duplicate$ empty$
+ { pop$
+ journal duplicate$ empty$
+ { "need key or journal for " cite$ * " to crossref " * crossref * warning$ }
+ { "journal" bibinfo.check slant word.in swap$ * }
+ if$
+ }
+ { word.in swap$ * " " *}
+ if$
+ " \cite{" * crossref * "}" *
+}
+FUNCTION {format.crossref.editor}
+{ editor #1 "{vv~}{ll}" format.name$
+ "editor" bibinfo.check
+ editor num.names$ duplicate$
+ #2 >
+ { pop$
+ " " * bbl.etal
+ *
+ }
+ { #2 <
+ 'skip$
+ { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
+ {
+ " " * bbl.etal
+ *
+ }
+ {
+ " \& "
+ * editor #2 "{vv~}{ll}" format.name$
+ "editor" bibinfo.check
+ *
+ }
+ if$
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.book.crossref}
+{ volume duplicate$ empty$
+ { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
+ pop$ word.in
+ }
+ { bbl.volume
+ capitalize
+ swap$ tie.or.space.prefix "volume" bibinfo.check * * bbl.of space.word *
+ }
+ if$
+ editor empty$
+ editor field.or.null author field.or.null =
+ or
+ { key empty$
+ { series empty$
+ { "need editor, key, or series for " cite$ * " to crossref " *
+ crossref * warning$
+ "" *
+ }
+ { series slant * }
+ if$
+ }
+ { key * }
+ if$
+ }
+ { format.crossref.editor * }
+ if$
+ " \cite{" * crossref * "}" *
+}
+FUNCTION {format.incoll.inproc.crossref}
+{
+ editor empty$
+ editor field.or.null author field.or.null =
+ or
+ { key empty$
+ { format.booktitle duplicate$ empty$
+ { "need editor, key, or booktitle for " cite$ * " to crossref " *
+ crossref * warning$
+ }
+ { word.in swap$ * }
+ if$
+ }
+ { word.in key * " " *}
+ if$
+ }
+ { word.in format.crossref.editor * " " *}
+ if$
+ " \cite{" * crossref * "}" *
+}
+FUNCTION {format.org.or.pub}
+{ 't :=
+ ""
+ address empty$ t empty$ and
+ 'skip$
+ {
+ t empty$
+ { address "address" bibinfo.check *
+ }
+ { t *
+ address empty$
+ 'skip$
+ { ", " * address "address" bibinfo.check * }
+ if$
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.publisher.address}
+{ publisher "publisher" bibinfo.warn format.org.or.pub
+}
+
+FUNCTION {format.organization.address}
+{ organization "organization" bibinfo.check format.org.or.pub
+}
+
+FUNCTION {article}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date "year" output.check
+ date.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ {
+ journal
+ "journal" bibinfo.check
+ slant
+ "journal" output.check
+ format.vol.num
+ }
+ { format.article.crossref output.nonnull
+ }
+ if$
+ eid empty$
+ { format.journal.pages }
+ { format.journal.eid }
+ if$
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {book}
+{ output.bibitem
+ author empty$
+ { format.editors "author and editor" output.check
+ }
+ { format.authors output.nonnull
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ format.date "year" output.check
+ date.block
+ format.btitle "title" output.check
+ crossref missing$
+ { format.edition output
+ new.block
+ format.volume.number.series output
+ format.publisher.address output
+ }
+ {
+ new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {booklet}
+{ output.bibitem
+ format.authors output
+ format.date output
+ date.block
+ format.title "title" output.check
+ new.block
+ howpublished "howpublished" bibinfo.check output
+ address "address" bibinfo.check output
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {inbook}
+{ output.bibitem
+ author empty$
+ { format.editors "author and editor" output.check
+ }
+ { format.authors output.nonnull
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ format.date "year" output.check
+ date.block
+ format.btitle "title" output.check
+ crossref missing$
+ {
+ format.edition output
+ format.chapter output
+ format.pages output
+ new.block
+ format.volume.number.series output
+ format.publisher.address output
+ }
+ {
+ format.chapter output
+ format.pages output
+ new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {incollection}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date "year" output.check
+ date.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle "booktitle" output.check
+ format.edition output
+ format.chapter output
+ format.volume.number.series output
+ format.publisher.address output
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ format.chapter output
+ }
+ if$
+ format.pages "pages" output.check
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {inproceedings}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date "year" output.check
+ date.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle "booktitle" output.check
+ format.volume.number.series output
+ publisher empty$
+ { format.organization.address output }
+ { organization "organization" bibinfo.check output
+ format.publisher.address output
+ }
+ if$
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ }
+ if$
+ format.pages "pages" output.check
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {conference} { inproceedings }
+FUNCTION {manual}
+{ output.bibitem
+ author empty$
+ { organization "organization" bibinfo.check
+ duplicate$ empty$ 'pop$
+ { output
+ address "address" bibinfo.check output
+ }
+ if$
+ }
+ { format.authors output.nonnull }
+ if$
+ format.date output
+ date.block
+ format.btitle "title" output.check
+ format.edition output
+ author empty$
+ { organization empty$
+ {
+ address new.block.checka
+ address "address" bibinfo.check output
+ }
+ 'skip$
+ if$
+ }
+ {
+ organization address new.block.checkb
+ organization "organization" bibinfo.check output
+ address "address" bibinfo.check output
+ }
+ if$
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {mastersthesis}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date "year" output.check
+ date.block
+ format.btitle
+ "title" output.check
+ new.block
+ bbl.mthesis format.thesis.type output.nonnull
+ school "school" bibinfo.warn output
+ address "address" bibinfo.check output
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {misc}
+{ output.bibitem
+ format.authors output
+ format.date output
+ output.state before.all =
+ 'skip$
+ {date.block}
+ if$
+ title howpublished new.block.checkb
+ format.title output
+ howpublished new.block.checka
+ howpublished "howpublished" bibinfo.check output
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+ empty.misc.check
+}
+FUNCTION {phdthesis}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date "year" output.check
+ date.block
+ format.btitle
+ "title" output.check
+ new.block
+ bbl.phdthesis format.thesis.type output.nonnull
+ school "school" bibinfo.warn output
+ address "address" bibinfo.check output
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {proceedings}
+{ output.bibitem
+ editor empty$
+ { organization "organization" bibinfo.check output
+ }
+ { format.editors output.nonnull }
+ if$
+ format.date "year" output.check
+ date.block
+ format.btitle "title" output.check
+ editor empty$
+ { publisher empty$
+ { new.sentence format.volume.number.series output }
+ {
+ new.sentence
+ format.volume.number.series output
+ format.publisher.address output
+ }
+ if$
+ }
+ { publisher empty$
+ {
+ new.sentence
+ format.volume.number.series output
+ format.organization.address output }
+ {
+ new.sentence
+ format.volume.number.series output
+ organization "organization" bibinfo.check output
+ format.publisher.address output
+ }
+ if$
+ }
+ if$
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {techreport}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date "year" output.check
+ date.block
+ format.title
+ "title" output.check
+ new.block
+ format.tr.number output.nonnull
+ institution "institution" bibinfo.warn output
+ address "address" bibinfo.check output
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {unpublished}
+{ output.bibitem
+ format.authors "author" output.check
+ format.date output
+ date.block
+ format.title "title" output.check
+ format.doi output
+ new.block
+ format.url output
+ new.block
+ format.note "note" output.check
+ fin.entry
+}
+
+FUNCTION {default.type} { misc }
+READ
+FUNCTION {sortify}
+{ purify$
+ "l" change.case$
+}
+INTEGERS { len }
+FUNCTION {chop.word}
+{ 's :=
+ 'len :=
+ s #1 len substring$ =
+ { s len #1 + global.max$ substring$ }
+ 's
+ if$
+}
+FUNCTION {sort.format.names}
+{ 's :=
+ #1 'nameptr :=
+ ""
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { s nameptr
+ "{ll{ }}{ ff{ }}{ jj{ }}"
+ format.name$ 't :=
+ nameptr #1 >
+ {
+ " " *
+ namesleft #1 = t "others" = and
+ { "zzzzz" * }
+ { t sortify * }
+ if$
+ }
+ { t sortify * }
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+}
+
+FUNCTION {sort.format.title}
+{ 't :=
+ "A " #2
+ "An " #3
+ "The " #4 t chop.word
+ chop.word
+ chop.word
+ sortify
+ #1 global.max$ substring$
+}
+FUNCTION {author.sort}
+{ author empty$
+ { key empty$
+ { "to sort, need author or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+FUNCTION {author.editor.sort}
+{ author empty$
+ { editor empty$
+ { key empty$
+ { "to sort, need author, editor, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+FUNCTION {author.organization.sort}
+{ author empty$
+ { organization empty$
+ { key empty$
+ { "to sort, need author, organization, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { "The " #4 organization chop.word sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+FUNCTION {editor.organization.sort}
+{ editor empty$
+ { organization empty$
+ { key empty$
+ { "to sort, need editor, organization, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { "The " #4 organization chop.word sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+}
+FUNCTION {presort}
+{ type$ "book" =
+ type$ "inbook" =
+ or
+ 'author.editor.sort
+ { type$ "proceedings" =
+ 'editor.organization.sort
+ { type$ "manual" =
+ 'author.organization.sort
+ 'author.sort
+ if$
+ }
+ if$
+ }
+ if$
+ " "
+ *
+ year field.or.null sortify
+ *
+ " "
+ *
+ title field.or.null
+ sort.format.title
+ *
+ #1 entry.max$ substring$
+ 'sort.key$ :=
+}
+ITERATE {presort}
+SORT
+STRINGS { longest.label }
+INTEGERS { number.label longest.label.width }
+FUNCTION {initialize.longest.label}
+{ "" 'longest.label :=
+ #1 'number.label :=
+ #0 'longest.label.width :=
+}
+FUNCTION {longest.label.pass}
+{ number.label int.to.str$ 'label :=
+ number.label #1 + 'number.label :=
+ label width$ longest.label.width >
+ { label 'longest.label :=
+ label width$ 'longest.label.width :=
+ }
+ 'skip$
+ if$
+}
+EXECUTE {initialize.longest.label}
+ITERATE {longest.label.pass}
+FUNCTION {begin.bib}
+{ preamble$ empty$
+ 'skip$
+ { preamble$ write$ newline$ }
+ if$
+ "\begin{thebibliography}{" longest.label * "}" *
+ write$ newline$
+ "\providecommand{\bibitemdeclare}[2]{}"
+ write$ newline$
+ "\providecommand{\surnamestart}{}"
+ write$ newline$
+ "\providecommand{\surnameend}{}"
+ write$ newline$
+ "\providecommand{\urlprefix}{Available at }"
+ write$ newline$
+ "\providecommand{\url}[1]{\texttt{#1}}"
+ write$ newline$
+ "\providecommand{\href}[2]{\texttt{#2}}"
+ write$ newline$
+ "\providecommand{\urlalt}[2]{\href{#1}{#2}}"
+ write$ newline$
+ "\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}"
+ write$ newline$
+ "\providecommand{\bibinfo}[2]{#2}"
+ write$ newline$
+}
+EXECUTE {begin.bib}
+EXECUTE {init.state.consts}
+ITERATE {call.type$}
+FUNCTION {end.bib}
+{ newline$
+ "\end{thebibliography}" write$ newline$
+}
+EXECUTE {end.bib}
+%% End of customized bst file
+%%
+%% End of file `eptcs.bst'.
diff --git a/publications/pxtp21/eptcs.cls b/publications/pxtp21/eptcs.cls
new file mode 100644
index 0000000000000000000000000000000000000000..3a5f6b1652136afdbd6941b44295d01cbc5df38e
--- /dev/null
+++ b/publications/pxtp21/eptcs.cls
@@ -0,0 +1,263 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{eptcs}[2020/12/20 v1.6]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% options %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newif\ifadraft
+\newif\ifsubmission
+\newif\ifpreliminary
+\newif\ifcopyright
+\newif\ifpublicdomain
+\newif\ifcreativecommons
+\newif\ifnoderivs
+\newif\ifsharealike
+\newif\ifnoncommercial
+\adraftfalse
+\submissionfalse
+\preliminaryfalse
+\copyrightfalse
+\publicdomainfalse
+\creativecommonsfalse
+\noderivsfalse
+\sharealikefalse
+\noncommercialfalse
+\DeclareOption{adraft}{\adrafttrue}
+\DeclareOption{submission}{\submissiontrue}
+\DeclareOption{preliminary}{\preliminarytrue}
+\DeclareOption{copyright}{\copyrighttrue}
+\DeclareOption{publicdomain}{\publicdomaintrue}
+\DeclareOption{creativecommons}{\creativecommonstrue}
+\DeclareOption{noderivs}{\noderivstrue}
+\DeclareOption{noncommercial}{\noncommercialtrue}
+\DeclareOption{sharealike}{\sharealiketrue}
+\ProcessOptions\relax
+
+\LoadClass[letterpaper,11pt,twoside]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% On US letter paper the margins (left-top-right-bottom) are %%
+%% 2.795cm - 1.23cm - 2.795cm - 3.46cm %%
+%% Note: When \topmargin would be 0, the real top margin would be %%
+%% (72-25-12=35pt) + 1pt (unused portion of head) = .5in = 1.27cm. %%
+%% The bottom margin is 11in - 1in + 0.04cm - 623/72in = 3.46cm. %%
+%% On the first page the bottom margin contains various footers. %%
+%% When translating from US letter to A4 paper, without scaling, by %%
+%% leaving the centre of the paper invariant (as is possible when %%
+%% printing the paper with acroread), the resulting A4 margins are %%
+%% 2.5cm - 2.11cm - 2.5cm - 4.34cm %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\textwidth 16cm % A4 width is 21cm %
+\textheight 623.01pt % 46 lines exactly = 21.98cm %
+\oddsidemargin -0.04cm % +1 inch = 2.5cm %
+\evensidemargin -0.04cm % +1 inch = 2.5cm %
+\topmargin -0.04cm % +1 inch = 2.5cm %
+\advance\topmargin-\headheight % 12pt %
+\advance\topmargin-\headsep % 25pt %
+\marginparwidth 45pt % leaves 15pt from A4 edge %
+\advance\evensidemargin .295cm % centre w.r.t. letter paper %
+\advance\oddsidemargin .295cm % centre w.r.t. letter paper %
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% load eptcsdata when available %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\IfFileExists{eptcsdata.tex}{\input{eptcsdata}}{}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Pagestyle and titlepage %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\pagestyle{myheadings}
+\renewcommand\pagestyle[1]{} % ignore further \pagestyles
+
+\renewcommand\maketitle{\par
+ \begingroup
+ \providecommand{\event}{}
+ \ifadraft
+ \providecommand{\publicationstatus}{\Large DRAFT\quad\today}
+ \else\ifsubmission
+ \providecommand{\publicationstatus}{Submitted to:\\
+ \event}
+ \else\ifpreliminary
+ \providecommand{\publicationstatus}{Preliminary Report. Final version to appear in:\\
+ \event}
+ \else
+ \providecommand{\publicationstatus}{To appear in EPTCS.}
+ \fi\fi\fi
+ \providecommand{\titlerunning}{Please define {\tt $\backslash$titlerunning}}
+ \providecommand{\authorrunning}{Please define {\tt $\backslash$authorrunning}}
+ \providecommand{\copyrightholders}{\authorrunning}
+ \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+ \def\@makefnmark{\rlap{\@textsuperscript{\normalfont\@thefnmark}}}%
+ \long\def\@makefntext##1{\parindent 1em\noindent
+ \hb@xt@1.8em{%
+ \hss\@textsuperscript{\normalfont\@thefnmark}}##1}%
+ \newpage
+ \global\@topnum\z@ % Prevents figures from going at top of page.
+ \@maketitle
+ \thispagestyle{empty}\@thanks
+ \endgroup
+ \setcounter{footnote}{0}%
+ \label{FirstPage}
+ \global\let\thanks\relax
+ \global\let\maketitle\relax
+ \global\let\@maketitle\relax
+ \global\let\@thanks\@empty
+ \global\let\@author\@empty
+ \global\let\@date\@empty
+ \global\let\@title\@empty
+ \global\let\title\relax
+ \global\let\author\relax
+ \global\let\date\relax
+ \global\let\and\relax
+}
+\def\@maketitle{% adapted from article.cls
+ \newpage
+\noindent
+\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
+\begin{tabular}{@{}l}
+\publicationstatus
+\end{tabular}}
+\hfill\vspace{-1em}
+\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
+\makebox[0pt][r]{
+\begin{tabular}{l@{}}
+\ifpublicdomain
+ This work is \href{https://creativecommons.org/publicdomain/zero/1.0/}
+ {dedicated to the public domain}.
+\else
+ \ifcopyright
+ \copyright~\copyrightholders\\
+ \fi
+ \ifcreativecommons
+ This work is licensed under the
+ \ifnoncommercial
+ \href{https://creativecommons.org}{Creative Commons}\\
+ \ifnoderivs
+ \href{https://creativecommons.org/licenses/by-nc-nd/4.0/}
+ {Attribution-Noncommercial-No Derivative Works} License.
+ \else\ifsharealike
+ \href{https://creativecommons.org/licenses/by-nc-sa/4.0/}
+ {Attribution-Noncommercial-Share Alike} License.
+ \else
+ \href{https://creativecommons.org/licenses/by-nc/4.0/}
+ {Attribution-Noncommercial} License.
+ \fi\fi
+ \else
+ \ifnoderivs
+ \href{https://creativecommons.org}{Creative Commons}\\
+ \href{https://creativecommons.org/licenses/by-nd/4.0/}
+ {Attribution-No Derivative Works} License.
+ \else\ifsharealike
+ \href{https://creativecommons.org}{Creative Commons}\\
+ \href{https://creativecommons.org/licenses/by-sa/4.0/}
+ {Attribution-Share Alike} License.
+ \else
+ \\\href{https://creativecommons.org}{Creative Commons}
+ \href{https://creativecommons.org/licenses/by/4.0/}
+ {Attribution} License.
+ \fi\fi
+ \fi
+ \fi
+\fi
+\end{tabular}}}
+ \null
+ %\vskip 2em% a bit of space removed (< 2em)
+ \begin{center}%
+ \let \footnote \thanks
+ {\LARGE\bf \@title \par}% \bf added
+ \vskip 2em% was: 1.5em
+ {\large
+ \lineskip .5em%
+ \begin{tabular}[t]{c}%
+ \@author
+ \end{tabular}\par}%
+ \vskip 1em% \date and extra space removed
+ \end{center}%
+ \par
+ \markboth{\hfill\titlerunning}{\authorrunning\hfill}
+ \vskip .5em}
+
+\AtBeginDocument{
+ \providecommand{\firstpage}{1}
+ \setcounter{firstpage}{\firstpage}
+ \setcounter{page}{\firstpage}
+ \@ifpackageloaded{array}% Contributed by Wolfgang Jeltsch
+ {\newcommand{\IfArrayPackageLoaded}[2]{#1}}
+ {\newcommand{\IfArrayPackageLoaded}[2]{#2}}}
+\newcommand{\institute}[1]{\IfArrayPackageLoaded
+ {\\{\scriptsize\begin{tabular}[t]{@{}>{\footnotesize}c@{}}#1\end{tabular}}}
+ {\\{\scriptsize\begin{tabular}[t]{@{\footnotesize}c@{}}#1\end{tabular}}}}
+\newcommand{\email}[1]{\\{\footnotesize\tt #1}}
+
+\renewenvironment{abstract}{\begin{list}{}% header removed and noindent
+ {\rightmargin\leftmargin
+ \listparindent 1.5em
+ \parsep 0pt plus 1pt}
+ \small\item}{\end{list}
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\RequirePackage{hyperref} % add hyperlinks
+\RequirePackage{mathptmx} % Pick Times Roman as a base font
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Remember page numbers %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcounter{firstpage}
+\setcounter{firstpage}{1}
+\AtEndDocument{\clearpage
+ \addtocounter{page}{-1}
+ \immediate\write\@auxout{\string
+ \newlabel{LastPage}{{}{\thepage}{}{page.\thepage}{}}}%
+ \newwrite\pages
+ \immediate\openout\pages=\jobname.pag
+ \immediate\write\pages{\arabic{firstpage}-\arabic{page}}
+ \addtocounter{page}{1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Less space in lists %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\@listi{\leftmargin\leftmargini
+ \parsep 2.5\p@ \@plus1.5\p@ \@minus\p@
+ \topsep 5\p@ \@plus2\p@ \@minus5\p@
+ \itemsep2.5\p@ \@plus1.5\p@ \@minus\p@}
+\let\@listI\@listi
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+ \labelwidth\leftmarginii
+ \advance\labelwidth-\labelsep
+ \topsep 1\p@ \@plus\p@ \@minus\p@
+ \parsep 1\p@ \@plus\p@ \@minus\p@
+ \itemsep \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+ \labelwidth\leftmarginiii
+ \advance\labelwidth-\labelsep
+ \topsep \z@
+ \parsep \z@
+ \itemsep \topsep}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% References small and with less space between items %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewenvironment{thebibliography}[1]
+ {\section*{\refname}\small% small added
+ \list{\@biblabel{\@arabic\c@enumiv}}%
+ {\settowidth\labelwidth{\@biblabel{#1}}%
+ \leftmargin\labelwidth
+ \advance\leftmargin\labelsep
+ \@openbib@code
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+ \sloppy
+ \clubpenalty4000
+ \@clubpenalty \clubpenalty
+ \widowpenalty4000%
+ \sfcode`\.\@m
+ \setlength{\parskip}{0pt}%
+ \setlength{\itemsep}{3pt plus 2pt}% less space between items
+ }
+ {\def\@noitemerr
+ {\@latex@warning{Empty `thebibliography' environment}}%
+ \endlist}
diff --git a/publications/pxtp21/extended_abstract.tex b/publications/pxtp21/extended_abstract.tex
new file mode 100644
index 0000000000000000000000000000000000000000..a2afec2a7e6f6ff101386b031e7ee787498ce1a3
--- /dev/null
+++ b/publications/pxtp21/extended_abstract.tex
@@ -0,0 +1,426 @@
+\documentclass[submission,copyright,creativecommons]{eptcs}
+
+\providecommand{\event}{PxTP 2021} % Name of the event you are submitting to
+\usepackage{breakurl} % Not needed if you use pdflatex only.
+\usepackage{underscore} % Only needed if you use pdflatex.
+\usepackage{todonotes}
+
+\usepackage[frozencache=true]{minted}
+\usemintedstyle{trac}
+
+\usepackage{microtype}
+\microtypesetup{final,tracking=true,kerning=true,spacing=true,stretch=10,shrink=10,letterspace=25}
+\microtypecontext{spacing=nonfrench}
+
+\def\orcid#1{\smash{\href{http://orcid.org/#1}{\protect\raisebox{-1.25pt}{\protect\includegraphics{orcid.pdf}}}}}
+
+\title{Alethe: Towards a Generic SMT Proof Format\\ (extended abstract)}
+\author{%
+Hans-Jörg Schurr
+\orcid{0000-0002-0829-5056}
+\institute{University of Lorraine, CNRS, Inria, and LORIA, Nancy, France}
+\email{hans-jorg.schurr@inria.fr}
+\and
+Mathias Fleury
+\orcid{0000-0002-1705-3083}
+\institute{Johannes Kepler University Linz, Austria}
+\email{mathias.fleury@jku.at}
+\and
+Haniel Barbosa
+\orcid{0000-0003-0188-2300}
+\institute{Universidade Federal de Minas Gerais, Belo Horizonte, Brazil}
+\email{hbarbosa@dcc.ufmg.br}
+\and
+Pascal Fontaine
+\orcid{0000-0003-4700-6031}
+\institute{University of Liège, Belgium}
+\email{pascal.fontaine@uliege.be}
+}
+
+\def\titlerunning{Towards a Generic SMT Proof Format}
+\def\authorrunning{Schurr, Fleury, Barbosa, and Fontaine}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+ The first iteration of the proof format used by the SMT solver veriT was
+ presented ten years ago at the first PxTP workshop.
+ %
+ Since then the format has matured. veriT proofs are used
+ within multiple applications, and other solvers generate proofs in the
+ same format.
+ %
+ We would now like to gather feedback from the community to guide future
+ developments.
+ %
+ Towards this, we review the history of the format, present
+ our pragmatic approach to develop the format, and
+ also discuss problems that might arise when other solvers use the format.
+\end{abstract}
+
+\noindent
+Over the years the production of machine-consumable formal proofs of
+unsatisfiability from SMT solvers~\cite{Barrett2018} has attracted significant
+attention~\cite{barrett-2015}.
+%
+Such proofs enable users to certify unsatisfiability results similarly to how
+satisfiable results may be certified via models.
+%
+However, a major difficulty that SMT proof formats
+must address is the complex and
+heterogeneous nature of SMT solvers: a SAT solver drives
+multiple, often very
+%
+different, theory solvers; instantiation procedures
+generate ground instances; and heavily theory-dependent simplification techniques
+ensure that the solvers are fast in practice.
+%
+Moreover, how each of these components works internally can also differ from
+solver to solver.
+%
+As a testament to these challenges proof formats for SMT solvers have been
+mostly restricted to individual solvers and no standard has emerged.
+%
+To be adopted by several solvers, an SMT proof format must be carefully designed
+to accommodate needs of specific
+solvers. This will require repeated refinement and generalization.
+
+The basis for our efforts in this field is the proof format implemented by the
+SMT solver veriT~\cite{verit} that is now mature and used by multiple systems.
+To further improve the format, as well as to accommodate not only the reasoning
+of the SMT solver veriT but also of other solvers, we are currently extending
+the format and developing better tooling, such as an independent proof checker.
+To facilitate this effort and overall usage, we are also writing a full
+specification.
+To emphasize the independence of the format we are baptizing it
+\emph{Alethe}.\footnote{Alethe is a genus of small birds and the name resembles \emph{aletheia},
+the Greek word for truth.}
+%
+We do not presume to propose a standard format a priori. Instead we believe that
+Alethe, together with its tooling, can provide a basis for further discussions
+on how to achieve a format to be used by multiple solvers.
+
+\section{The State of Alethe}
+
+Alethe combines two major ideas
+whose roots reach back ten years to the first PxTP workshop in
+2011~\cite{besson-2011,deharbe-2011}.
+It was proposed as
+an easy-to-produce format with a term language very close to
+SMT-LIB~\cite{SMTLIB}, the standard input language of SMT solvers, and rules
+with a varying level of granularity, allowing implicit proof steps in the proof
+and thus relying on powerful proof checkers capable of filling the gaps.
+%
+Since then the format has been refined and extended~\cite{barbosa-2019}. It is now
+mature, supports coarse- and fine-grained proof steps capturing
+SMT solving for the SMT-LIB logic UFLIRA\footnote{That is the logic for
+ problems containing a mix of any of quantifiers,
+ uninterpreted
+ functions, and linear arithmetic.} and can be reconstructed by the proof
+assistants Coq~\cite{Armand2011,SMTCoq} and
+Isabelle~\cite{fleury-2019,schurr-2021}.
+%
+In particular, the integration with Coq was also used as a bridge for the
+reconstruction of proofs from the SMT solver CVC4~\cite{Barrett2011} in
+Coq, where its proofs in the LFSC format~\cite{Stump2013} were
+first translated into the veriT format before reconstruction.
+%
+Finally, the format will also be natively supported in the upcoming cvc5.
+solver\footnote{\url{https://cvc4.github.io/2021/04/02/cvc5-announcement.html}}
+
+On the one hand, Alethe uses a
+natural-deduction style calculus driven mostly by resolution~\cite{besson-2011}.
+To handle
+first-order reasoning, dedicated quantifier instantiation rules are used~\cite{deharbe-2011}.
+On the other hand, it
+implements novel ideas to express reasoning typically used for processing,
+such as Skolemization, renaming of variables, and other manipulations
+of bound variables~\cite{barbosa-2019}.
+While the format was always inspired by the SMT-LIB language,
+we recently~\cite{fleury-2019} changed
+the syntax of Alethe to closely resemble the command structure
+used within SMT-LIB. When possible Alethe uses existing SMT-LIB features,
+such as the \texttt{define-fun} command to define constants and the \texttt{:named}
+annotation to implement term sharing.
+
+The following proof fragment gives a taste of the format. The
+fragment first renames the bound variable in the term $\exists x.\,f(x)$ from
+$x$ to $\mathit{vr}$ and then skolemizes the quantifier. A proof is a
+list of commands. The \emph{assume} command introduces an assumption, \emph{anchor}
+starts a subproof, and \emph{step} denotes an ordinary proof step. Steps are
+annotated with an identifier, a rule, and premises. The SMT-LIB command \emph{define-fun}
+defines a function.
+The rule \emph{bind} used by step \texttt{t1} performs the renaming
+of the bound variable. It uses a subproof (Steps \texttt{t1.t1} and
+\texttt{t1.t2}). The subproof uses a context to denote that \texttt{x}
+is equal to \texttt{vr} within the subproof. The \texttt{anchor} command
+starts the subproof and introduces the context.
+The \texttt{bind} rule does not only make it possible to
+rename bound variables, but within the subproof it is possible
+to simplify the formula as done during preprocessing.
+The steps \texttt{t2} and \texttt{t3} use resolution to finish the
+renaming.
+In step
+\texttt{t4} the bound variable is skolemized. Skolemization uses
+the choice binder $\epsilon$ and derives $f(\epsilon\mathit{vr}.\, f(\mathit{vr}))$
+from $\exists \mathit{vr}.\, f(\mathit{vr})$. To simplify the reconstruction
+the choice term is introduced as a defined constant (by \texttt{define-fun}). Finally, resolution
+is used again to finish the proof.
+\begin{minted}{smtlib2.py -x}
+ (assume a0 (exists ((x A)) (f x)))
+ (anchor :step t1 :args (:= x vr))
+ (step t1.t1 (cl (= x vr)) :rule cong)
+ (step t1.t2 (cl (= (f x) (f vr))) :rule cong)
+ (step t1 (cl (= (exists ((x A)) (f x))
+ (exists ((vr A)) (f vr)))) :rule bind)
+ (step t2 (cl (not (= (exists ((vr A)) (f x))
+ (exists ((vr A)) (f vr))))
+ (not (exists ((vr A)) (f x)))
+ (exists ((vr A)) (f vr))) :rule equiv_pos1)
+ (step t3 (cl (exists ((vr A)) (f vr))) :premises (a0 t1 t2) :rule resolution)
+ (define-fun X () A (choice ((vr A)) (f vr)))
+ (step t4 (cl (= (exists ((vr A)) (f vr)) (f X))) :rule sko_ex)
+ (step t5 (cl (not (= (exists ((vr A)) (f vr)) (f X)))
+ (not (exists ((vr A)) (f vr)))
+ (f X)) :rule equiv_pos1)
+ (step t6 (cl (f X)) :premises (t3 t4 t5) :rule resolution)
+\end{minted}
+
+The output of Alethe proofs from veriT has now reached a certain level of maturity.
+The 2021 version of the Isabelle theorem prover was released earlier this year
+and supports the reconstruction of
+Alethe proofs generated by veriT. Users of Isabelle/HOL can invoke the \texttt{smt}
+tactic. This tactic encodes the current proof goal as an SMT-LIB problem and
+calls an SMT solver. Previously only the SMT solver Z3 was supported. Now
+veriT is supported too. If the solver produces a proof, the proof is
+reconstructed within the Isabelle kernel. In practice, users will seldom
+choose the \texttt{smt} tactic themselves. Instead, they call the
+Sledgehammer tool that calls external tools to find relevant facts. Sometimes,
+the external tool finds a proof, but the proof cannot be imported into Isabelle,
+requiring the user to write a proof manually.
+The addition of the veriT-powered \texttt{smt} tactic halves~\cite{schurr-2021} the rate
+of this kind of failures. The improvement is especially pronounced for proofs found by CVC4.
+A key reason for this improvement is the support for the
+conflicting-instance instantiation technique within veriT. Z3, the
+singular SMT solver supported previously, does not implement this
+technique. Nevertheless, it is Alethe that allowed us to connect veriT
+to Isabelle, and we hope that the support for Alethe in other solvers
+will ease this connection between powerful SMT solvers and other tools in the future.
+
+The process of implementing proof reconstruction in Isabelle also
+helped us to improve the proof format. We found both,
+possible improvements in the format (like providing the Farkas' coefficient for
+lemmas of linear arithmetic) and in the implementation (by identifying
+concrete errors).
+One major shortcoming of the proofs were rules that combined several simplification
+steps into one.
+We replaced these steps by
+multiple simple and well-defined rules. In particular every simplification rule
+addresses a specific theory instead of combining them.
+An interesting
+observation of the reconstruction in Isabelle is that some steps can be skipped
+to improve performance. For example, the proofs for the renaming of variables
+are irrelevant for Isabelle since this uses De~Bruijn indices.
+%
+This shows that reconstruction specific
+optimizations can counterbalance the proof length which is increased by fine-grained
+rules.
+%
+We will take this prospect into account as we further refine the format.
+
+\section{A Glance Into the Future}
+The development of the Alethe proof format so far was not a monolithic
+process. Both practical considerations and research progress --- such as
+supporting fine-grained preprocessing rules --- influenced the development process.
+Due to this, the format is not fully homogeneous, but this approach allowed
+us to quickly adapt the format when necessary. We will continue this
+pragmatic approach.
+
+\paragraph{Speculative Specification.}
+
+We are writing a speculative specification.\footnote{The current
+version is available at
+\url{http://www.verit-solver.org/documentation/alethe-spec.pdf}.}
+During the development of the Isabelle reconstruction it became necessary
+to document the proof rules in a coherent and complete manner. When we
+started to develop the reconstruction there was only an automatically
+generated list of rules with a short comment for each rule. While
+this is enough for simple tautological rules, it does not provide a clear
+definition of the more complex rules such as the linear arithmetic rules.
+%
+To rectify this, we studied veriT's source code and wrote an independent
+document with a list of all rules and a clear mathematical definition
+of each rule.
+%
+We chose a
+level of precision for these descriptions that serves the implementer:
+precise enough to clarify the edge case, but without the details that would make it a fully formal specification.
+We are now extending this document to a full specification of the format.
+This specification is speculative in the sense that it will not be cast
+in stone. It will describe the format as it is in use
+at any point in time and will develop in parallel with practical support for the
+format within SMT solvers, proof checkers, and other tools.
+
+\paragraph{Flexible Rules.}
+
+The next solver that will gain support for the Alethe format is the upcoming
+cvc5 solver. Implementing a proof format into another solver reveals where the
+proof format is too tied to the current implementation of veriT. On the one
+hand, new proof rules must be added to the format --- e.g., veriT does not
+support the theory of bitvectors, while cvc5 does.
+%
+When CVC4 was integrated into Coq via a translation of its LFSC proofs into
+Alethe proofs~\cite{SMTCoq}, an ad-hoc extension with bitvector rules was
+made. A revised version of this extension will now be incorporated into the
+upcoming specification of the format so that cvc5 bitvector proofs can be
+represented in Alethe.
+%
+Further extensions to other theories supported by cvc5, like the theory of
+strings, will eventually be made as well.
+
+Besides new theories, cvc5 can also be stricter than veriT in the usage
+of some rules.
+%
+This strictness can simplify the reconstruction, since less search is
+required.
+%
+A good example of this is the \texttt{trans} rule that expresses
+transitivity.
+%
+This rule has a list of equalities as premises and the conclusion is
+an equality derived by transitivity.
+%
+In principle, this rule can have three levels of ``strictness'':
+\begin{enumerate}
+\item The premises are ordered and the equalities are correctly oriented (like in cvc5), e.g.,
+ \(a=b\), \(b=c\), and \(c=d\) implies \(a=d\).
+\item The premises are ordered but the equalities might not be correctly oriented (like in veriT), e.g.,
+ \(b=a\), \(c=b\), and \(d=c\) implies \(d=a\).
+\item Neither are the assumptions ordered, nor are the equalities oriented, e.g., \(c=b\),
+ \(b=a\), and \(d=c\) implies \(d=a\).
+\end{enumerate}
+
+\noindent
+The most strict variant is the easiest to reconstruct: a straightforward linear
+traversal of the premises suffices for checking.
+%
+From the point of view of producing it from the solver, however, this version is
+the hardest to implement. This is due to implementations of the
+congruence closure decision procedure~\cite{Nelson1980,Downey1980} in SMT
+solvers being generally agnostic to the order of equalities, which can lead to
+implicit reorientations that can be difficult to track.
+%
+Anecdotally, for cvc5 to achieve this level of detail several months of work
+were necessary, within the overall effort of redesigning from scratch CVC4's
+proof infrastructure.
+%
+Since we cannot assume every solver developer will, or even should, undertake
+such an effort, all the different levels of granularity must be allowed by the
+format, each requiring different complexity levels of checking.
+
+To keep the proof format flexible and proofs easy to produce, we will
+provide different versions of proof rules, with varying levels of granularity as
+in the transitivity example case above, by \emph{annotating} them.
+%
+This leverages the rule \emph{arguments},
+%
+which are already used by some
+rules.
+%
+For example, the Farkas' coefficient of the linear arithmetic rule are provided
+as arguments.
+%
+This puts pressure on proof checkers and reconstruction in proof assistants to
+support all the variants or at least the most general one (at the cost of
+efficiency). Hence, our design principle here is that the annotation is
+optional: the absence of an annotation denotes the least strict version of the
+rule.
+
+\paragraph{Powerful Tooling.}
+
+We believe that powerful software tools may greatly increase the utility of a
+proof format.
+%
+Towards this end we have started implementing an independent proof checker for
+Alethe.
+%
+In contrast to a proof-assistant-based reconstruction, this checker will not be
+structured around a small, trusted kernel, and correct-by-construction
+extensions. Instead, the user would need to trust the implementation does not
+lead to wrong checking results.
+%
+Instead, its focus is on performance, support for multiple features and greater
+flexibility for integrating extensions and refinements to the format.
+%
+The Isabelle checker is currently not suited
+to this task --- one major issue is that it does not support SMT-LIB input
+files.\footnote{A version capable of doing so was developed for Z3 but it was unfortunately lost.}
+
+This independent checker will also serve as a proof ``elaborator''.
+%
+Rather than checking, it will also allow converting a coarse-grained proof,
+containing implicit steps, to a fine-grained one, with more detailed steps. The
+resulting proof can then be more efficiently checked by the tool itself or
+via proof-assistant reconstructions.
+%
+An example of such elaboration is the transitivity rule.
+%
+If the rule is not in its most detailed version, with premises in the correct
+order and none implicitly reordered, it can be elaborated by greedily reordering
+the premises and adding proof steps using the symmetry of equality.
+%
+Note however that in the limit detailing coarse-grained steps can be as hard as
+solving an SMT problem. Should such cases arise, the checker will rely on internal
+proof-producing procedures capable of producing a detailed proof for the given
+step. At first the veriT and cvc5 solvers, which can produce fine-grained proofs
+for several aspects of SMT solving, could be used in such cases.
+
+A nice side effect of the use of an external checker is that it could prune useless
+steps. Currently SMT solvers keep a full proof trace in memory and print a pruned
+proof after solving finishes. This is in contrast to SAT solvers that dump proofs
+on-the-fly. For SAT proofs, the pruned proof can be obtained from a full trace by using a tool like
+\textsc{Drat-Trim}. There is some ongoing work by Nikolaj Bjørner on Z3 to also generate proofs
+on-the-fly, but it is not clear how to support preprocessing and quantifiers.\footnote{\url{https://github.com/Z3Prover/z3/discussions/4881}}
+
+\section{Conclusion}
+\label{sec:concl}
+
+We have presented on overview of the current state of the Alethe proof format
+and some ideas on how we intend to improve and extend the format, as well as
+supporting tools.
+%
+In designing a new proof format supported across two solvers we hope to provide
+a first step towards a format adopted by more solvers.
+%
+This format allows several levels of detail, and is thus flexible enough to reasonably
+easily produce proofs in various contexts. We intend to define a precise
+semantics at each level though.
+%
+This distinguishes our format from other approaches, such as the TSTP
+format~\cite{Sutcliffe2004}, that are probably easier to adopt but only
+specify the syntax, leading to very different proofs generated by the various
+provers supporting it.
+
+One limit of our approach for proofs is that we cannot express global
+transformations like symmetry breaking. SAT solvers are able to add clauses
+(DRAT clauses) such that the overall problems is equisatisfiable. It is unclear
+however how to add such clauses in the SMT context.
+
+Overall, we hope to get feedback from users and developers to see what special
+needs they have and exchange ideas on the proof format.
+
+\paragraph{Acknowledgment}
+We thank Bruno Andreotti for ongoing work on the proof checker and
+Hanna Lachnitt for ongoing work on the cvc5 support.
+We are grateful for the helpful comments provided to us by the anonymous
+reviewers.
+The first author has received funding from the European Research Council (ERC)
+under the European Union’s Horizon 2020 research and innovation program (grant
+agreement No. 713999, Matryoshka).
+The second author is supported by the LIT AI Lab funded by the State of Upper Austria.
+
+\bibliographystyle{eptcs}
+\bibliography{generic}
+
+\end{document}
diff --git a/publications/pxtp21/generic.bib b/publications/pxtp21/generic.bib
new file mode 100644
index 0000000000000000000000000000000000000000..5a2d13ed3197d7aa60ab47cd80ba3a3af80f2ec5
--- /dev/null
+++ b/publications/pxtp21/generic.bib
@@ -0,0 +1,241 @@
+@string{lncs = "LNCS"}
+@string{cpp = "Certified Programs and Proofs"}
+@string{cav = "Computer Aided Verification (CAV)"}
+
+@inproceedings{besson-2011,
+ title = {A Flexible Proof Format for {SMT}: A Proposal},
+ author = {Besson, Fr{\'e}d{\'e}ric and Fontaine, Pascal and Th{\'e}ry, Laurent},
+ editor = "Pascal Fontaine and Aaron Stump",
+ booktitle = {PxTP 2011},
+ year = {2011},
+ pages = "15--26",
+ MONTH = Aug,
+}
+
+@inproceedings{deharbe-2011,
+ TITLE = {Quantifier Inference Rules for {SMT} Proofs},
+ AUTHOR = {D{\'e}harbe, David and Fontaine, Pascal and Woltzenlogel Paleo, Bruno},
+ editor = "Pascal Fontaine and Aaron Stump",
+ BOOKTITLE = {PxTP 2011},
+ YEAR = {2011},
+ pages = "33--39",
+ MONTH = Aug,
+}
+
+@article{barrett-2015,
+ title={Proofs in satisfiability modulo theories},
+ author={Barrett, Clark and De Moura, Leonardo and Fontaine, Pascal},
+ journal={All about proofs, Proofs for all},
+ volume={55},
+ number={1},
+ pages={23--44},
+ year={2015},
+ publisher={Citeseer}
+}
+
+@article{barbosa-2019,
+ title = "Scalable Fine-Grained Proofs for Formula Processing",
+ journal = "Journal of Automated Reasoning",
+ year = {2019},
+ month = jan,
+ author = "Barbosa, Haniel
+ and Blanchette, Jasmin C.
+ and Fleury, Mathias
+ and Fontaine, Pascal",
+ publisher = "Springer",
+ doi = {10.1007/s10817-018-09502-y}
+}
+
+@TECHREPORT{SMTLIB,
+ author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+ title = {{The SMT-LIB Standard: Version 2.6}},
+ institution = {Department of Computer Science, The University of Iowa},
+ year = 2017,
+ note = {Available at {\tt www.SMT-LIB.org}}
+}
+
+@inproceedings{verit,
+ author = {Thomas Bouton
+ and Diego C. B. de Oliveira
+ and David D{\'{e}}harbe
+ and Pascal Fontaine},
+ title = {{veriT}: An Open, Trustable and Efficient {SMT}-solver},
+ booktitle = "CADE 22",
+ pages = {151--156},
+ year = {2009},
+ editor = {Renate A. Schmidt},
+ series = lncs,
+ volume = {5663},
+ publisher = "Springer Berlin Heidelberg",
+ doi = {10.1007/978-3-642-02959-2\_12}
+}
+
+@InProceedings{SMTCoq,
+ author = "Ekici, Burak
+ and Mebsout, Alain
+ and Tinelli, Cesare
+ and Keller, Chantal
+ and Katz, Guy
+ and Reynolds, Andrew
+ and Barrett, Clark",
+ editor = "Majumdar, Rupak
+ and Kun{\v{c}}ak, Viktor",
+ title = "{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into {C}oq",
+ booktitle = "CAV 2017",
+ series = lncs,
+ volume = {10426},
+ year = "2017",
+ publisher = "Springer",
+ pages = "126--133",
+ isbn = "978-3-319-63390-9",
+ doi = {10.1007/978-3-319-63390-9\_7}
+}
+
+@inproceedings{fleury-2019,
+ author = {Mathias Fleury and
+ Hans{-}J{\"{o}}rg Schurr},
+ editor = {Giselle Reis and
+ Haniel Barbosa},
+ title = {Reconstructing {veriT} Proofs in {Isabelle/HOL}},
+ booktitle = {PxTP 2019},
+ series = {{EPTCS}},
+ volume = {301},
+ pages = {36--50},
+ year = {2019},
+ doi = {10.4204/EPTCS.301.6},
+}
+
+@inproceedings{schurr-2021,
+ author = {
+ Hans-Jörg Schurr and Mathias Fleury and Martin Desharnais
+ },
+ title = {Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant},
+ booktitle = "CADE 28",
+ year = {2021},
+ series = lncs,
+}
+
+@inproceedings{Armand2011,
+ author = {Micha{\"e}l Armand and
+ Germain Faure and
+ Benjamin Gr{\'e}goire and
+ Chantal Keller and
+ Laurent Th{\'e}ry and
+ Benjamin Werner},
+ title = {A~Modular Integration of {SAT}\slash{SMT} Solvers to {Coq} through
+ Proof Witnesses},
+ booktitle = cpp,
+ pages = {135--150},
+ editor = {Jean-Pierre Jouannaud and
+ Zhong Shao},
+ publisher = {Springer},
+ series = lncs,
+ volume = {7086},
+ year = {2011},
+ doi = {10.1007/978-3-642-25379-9_12}
+}
+
+@incollection{Barrett2018,
+ author = {Clark W. Barrett and
+ Cesare Tinelli},
+ title = {Satisfiability Modulo Theories},
+ booktitle = {Handbook of Model Checking.},
+ pages = {305--343},
+ year = {2018},
+ XXurl = {https://doi.org/10.1007/978-3-319-10575-8\_11},
+ doi = {10.1007/978-3-319-10575-8\_11},
+ timestamp = {Mon, 24 Jun 2019 15:54:17 +0200},
+ biburl = {https://dblp.org/rec/bib/reference/mc/BarrettT18},
+ bibsource = {dblp computer science bibliography, https://dblp.org},
+ editor = {Edmund M. Clarke and
+ Thomas A. Henzinger and
+ Helmut Veith and
+ Roderick Bloem},
+ publisher = {Springer},
+}
+
+@inproceedings{Barrett2011,
+author="Barrett, Clark
+and Conway, Christopher L.
+and Deters, Morgan
+and Hadarean, Liana
+and Jovanovi{\'{c}}, Dejan
+and King, Tim
+and Reynolds, Andrew
+and Tinelli, Cesare",
+editor="Gopalakrishnan, Ganesh
+and Qadeer, Shaz",
+title={{CVC4}},
+booktitle=cav,
+year="2011",
+publisher="Springer",
+pages="171--177",
+doi="10.1007/978-3-642-22110-1_14",
+XXurl="http://dx.doi.org/10.1007/978-3-642-22110-1_14"
+}
+
+@article{Stump2013,
+ author = {Aaron Stump and
+ Duckki Oe and
+ Andrew Reynolds and
+ Liana Hadarean and
+ Cesare Tinelli},
+ title = {{SMT} proof checking using a logical framework},
+ journal = {Formal Methods in System Design},
+ volume = {42},
+ number = {1},
+ pages = {91--118},
+ year = {2013},
+ XXurl = {http://dx.doi.org/10.1007/s10703-012-0163-3},
+ doi = {10.1007/s10703-012-0163-3},
+ timestamp = {Fri, 11 Jan 2013 11:14:23 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/fmsd/StumpORHT13},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@inproceedings{Sutcliffe2004,
+ author = {Geoff Sutcliffe and J{\"u}rgen Zimmer and Stephan Schulz},
+ title = "{TSTP} Data-Exchange Formats for Automated Theorem Proving Tools",
+ editor = "Weixiong Zhang and Volker Sorge",
+ booktitle = "Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems",
+ series = "Frontiers in Artificial Intelligence and Applications",
+ volume = 112,
+ pages = "201--215",
+ publisher = "IOS Press",
+ year = 2004}
+
+@article{Downey1980,
+ author = {Downey, Peter J. and Sethi, Ravi and Tarjan, Robert Endre},
+ title = {Variations on the Common Subexpression Problem},
+ journal = {J. ACM},
+ issue_date = {Oct. 1980},
+ volume = {27},
+ number = {4},
+ month = oct,
+ year = {1980},
+ issn = {0004-5411},
+ pages = {758--771},
+ numpages = {14},
+ XXurl = {http://doi.acm.org/10.1145/322217.322228},
+ doi = {10.1145/322217.322228},
+ acmid = {322228},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@article{Nelson1980,
+ author = {Nelson, Greg and Oppen, Derek C.},
+ title = {{Fast Decision Procedures Based on Congruence Closure}},
+ journal = {J. ACM},
+ issue_date = {April 1980},
+ volume = {27},
+ number = {2},
+ year = {1980},
+ issn = {0004-5411},
+ pages = {356--364},
+ numpages = {9},
+ XXurl = {http://doi.acm.org/10.1145/322186.322198},
+ doi = {10.1145/322186.322198},
+ acmid = {322198},
+ publisher = {ACM},
+}
diff --git a/publications/pxtp21/orcid.pdf b/publications/pxtp21/orcid.pdf
new file mode 100755
index 0000000000000000000000000000000000000000..b348975bce5714a33b4a2a464e999297b998d64f
Binary files /dev/null and b/publications/pxtp21/orcid.pdf differ
diff --git a/publications/pxtp21/smtlib2.py b/publications/pxtp21/smtlib2.py
new file mode 100755
index 0000000000000000000000000000000000000000..833869fcaa86542c8109e9dcaa28c5fbd4c6371b
--- /dev/null
+++ b/publications/pxtp21/smtlib2.py
@@ -0,0 +1,119 @@
+# -*- coding: utf-8 -*-
+
+import re
+
+from pygments.lexer import Lexer, RegexLexer, bygroups, do_insertions, \
+ default, include
+from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
+ Number, Punctuation, Generic
+from pygments import unistring as uni
+
+__all__ = ['Smt2Lexer']
+
+
+line_re = re.compile('.*?\n')
+
+class CustomLexer(RegexLexer):
+ """
+ A SMT-Lib 2 parser
+ """
+ name = 'Smt2'
+ aliases = ['smt2']
+ filenames = ['*.smt2']
+ mimetypes = ['text/x-smt2']
+
+ # list of known keywords and builtins taken form vim 6.4 scheme.vim
+ # syntax file.
+ keywords = (
+ 'declare-const', 'declare-fun', 'declare-sort', 'define-fun', 'assert', 'check-sat',
+ 'get-model', 'get-proof', 'get-value', 'echo', 'exit', 'error',
+ 'sat', 'unsat', 'unknown', 'model', 'set-option', 'set-logic',
+ 'anchor', 'step', 'assume', 'input'
+ )
+ sorts = (
+ 'Int', 'Bool'
+ )
+ builtins = (
+ '*', '+', '-', '/', '<', '<=', '=', '>', '>=', 'and', 'or', 'distinct',
+ 'not', ':=', 'forall', 'exists', 'cl'
+ )
+
+ # valid names for identifiers
+ # well, names can only not consist fully of numbers
+ # but this should be good enough for now
+ valid_name = r'[\w\.!$%&*+,/:<=>?@^~|-]+'
+
+ tokens = {
+ 'root': [
+ # the comments
+ # and going to the end of the line
+ (r';.*$', Comment.Single),
+ # multi-line comment
+ (r'#\|', Comment.Multiline, 'multiline-comment'),
+ # commented form (entire sexpr folliwng)
+ (r'#;\s*\(', Comment, 'commented-form'),
+ # signifies that the program text that follows is written with the
+ # lexical and datum syntax described in r6rs
+ (r'#!r6rs', Comment),
+
+ # whitespaces - usually not relevant
+ (r'\s+', Text),
+
+ # numbers
+ (r'-?\d+\.\d+', Number.Float),
+ (r'-?\d+', Number.Integer),
+ # support for uncommon kinds of numbers -
+ # have to figure out what the characters mean
+ # (r'(#e|#i|#b|#o|#d|#x)[\d.]+', Number),
+
+ # strings, symbols and characters
+ (r'"(\\\\|\\"|[^"])*"', String),
+ (r"'" + valid_name, String.Symbol),
+ (r"#\\([()/'\"._!§$%& ?=+-]|[a-zA-Z0-9]+)", String.Char),
+
+ # constants
+ (r'(true|false)', Name.Constant),
+
+ # special operators
+ (r"('|#|`|,@|,)", Operator),
+
+ # highlight the keywords
+ ('(%s)' % '|'.join(re.escape(entry) for entry in keywords),
+ Keyword.Reserved),
+
+ # highlight the sorts
+ ('(%s)' % '|'.join(re.escape(entry) for entry in sorts),
+ Keyword.Type),
+
+ # first variable in a quoted string like
+ # '(this is syntactic sugar)
+ (r"(?<='\()" + valid_name, Name.Variable),
+ (r"(?<=#\()" + valid_name, Name.Variable),
+
+ # highlight the builtins
+ ("(?<=\()(%s)" % '|'.join(re.escape(entry) + '\s+' for entry in builtins),
+ Name.Builtin),
+
+ (r':' + valid_name, Name.Function),
+
+ # the remaining functions
+ #(r'(?<=\()' + valid_name, Name.Function),
+ # find the remaining variables
+ (valid_name, Name.Variable),
+
+ # the famous parentheses!
+ (r'(\(|\))', Punctuation),
+ (r'(\[|\])', Punctuation),
+ ],
+ 'multiline-comment': [
+ (r'#\|', Comment.Multiline, '#push'),
+ (r'\|#', Comment.Multiline, '#pop'),
+ (r'[^|#]+', Comment.Multiline),
+ (r'[|#]', Comment.Multiline),
+ ],
+ 'commented-form': [
+ (r'\(', Comment, '#push'),
+ (r'\)', Comment, '#pop'),
+ (r'[^()]+', Comment),
+ ],
+ }
diff --git a/spec/doc.tex b/spec/doc.tex
index 7f35786f6c087711657b91f2651a2256013ae719..afcd205582aa1ab2a2c51e7a6f1ca4723a745bed 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -269,7 +269,7 @@ break
% ========================================
\title{The {\formatName} Proof Format}
-\subtitle{A Speculative Specification and Reference}
+\subtitle{A Speculative Specification and Reference\\(Work in Progress)}
\author{Haniel Barbosa\textsuperscript{1}
\and Mathias Fleury\textsuperscript{2}
\and Pascal Fontaine\textsuperscript{3}
@@ -610,6 +610,51 @@ of $(x+y<1) \lor (3<x)$, $x\simeq 2$, and $0\simeq y$.
% x < 0 , 1 = x --> 1 1 gives 1 < 0
% this should somehow be fixed
+\paragraph{Subproofs and Lemmas.}
+The proof format uses subproof to prove lemmas and to manipulate the context.
+To prove lemmas, a subproof can
+introduce local assumptions. The subproof \emph{rule} discharges the
+local assumptions by concluding with an implication (written as a clause)
+which has the local assumptions as its antecedents.
+A step can only use steps from the same subproof as its premise. It
+is not possible to have premises from either a subproof at a deeper
+level or from an outer level.%\todo{We could technically allow premises from
+%outside. Do we allow this?}
+
+As the example below shows, our notation for subproofs is a
+frame around the rules within the subproof. Subproofs are also used to
+manipulate the context.
+
+\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{plus\_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}
+
+\end{example}
+
+\paragraph{Contexts.}
+A specialty of the veriT proof
+format is the step context. The context is a possible empty list $[c_1,
+\dots, c_l]$, where $c_i$ is either a variable or a variable-term tuple
+denoted $x_i\mapsto t_i$. Throughout this document $\Gamma$ denotes
+an arbitrary context. The context denotes a substitution.%\todo{Extend}
+
\paragraph{Skolemization and Other Preprocessing Steps.}
One typical example for a rule with context is the \proofRule{sko\_ex}
rule, which is used to express Skolemization of an existentially