diff --git a/thys/Functional_Ordered_Resolution_Prover/document/root.tex b/thys/Functional_Ordered_Resolution_Prover/document/root.tex --- a/thys/Functional_Ordered_Resolution_Prover/document/root.tex +++ b/thys/Functional_Ordered_Resolution_Prover/document/root.tex @@ -1,72 +1,83 @@ \documentclass[10pt,a4paper]{article} \usepackage{amssymb} \usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} \usepackage{graphicx} \usepackage{isabelle} \usepackage{isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{pdfsetup} \urlstyle{tt} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \renewcommand{\isacharunderscore}{\_} \begin{document} \title{A Verified Functional Implementation of \\ Bachmair and Ganzinger's Ordered Resolution Prover} \author{Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel} \maketitle \begin{abstract} \noindent This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section~4.3 of Bachmair and Ganzinger's ``Resolution Theorem Proving'' chapter in the \emph{Handbook of Automated Reasoning}. The result is a functional implementation of a first-order prover. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt \parskip 0.5ex \section{Introduction} Bachmair and Ganzinger's ``Resolution Theorem Proving'' chapter %\cite{bachmair-ganzinger-2001} in the \emph{Handbook of Automated Reasoning} is the standard reference on the topic. It defines a general framework for propositional and first-order resolution-based theorem proving. Resolution forms the basis for superposition, the calculus implemented in many popular automatic theorem provers. \medskip This Isabelle/HOL formalization starts from an existing formalization of Bachmair and Ganzinger's chapter, up to and including Section 4.3. It refines the abstract ordered resolution prover presented in Section~4.3 to obtain an executable, functional implementation of a first-order prover. Figure~\ref{fig:thys} shows the corresponding Isabelle theory structure. +\medskip + +We refer to the following conference paper for details: + +\begin{quote} +Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel: \\ +A verified prover based on ordered resolution. \\ +CPP 2019: 152-165 \\ +\url{http://matryoshka.gforge.inria.fr/pubs/fun_rp_paper.pdf} +\end{quote} + \begin{figure} \begin{center} \includegraphics[width=0.75\textwidth,keepaspectratio]{session_graph} \end{center} \caption{Theory dependency graph} \label{fig:thys} \end{figure} % generated text of all theories \input{session} % optional bibliography % \bibliographystyle{abbrv} % \bibliography{bib} \end{document} diff --git a/thys/Lambda_Free_KBOs/document/root.tex b/thys/Lambda_Free_KBOs/document/root.tex --- a/thys/Lambda_Free_KBOs/document/root.tex +++ b/thys/Lambda_Free_KBOs/document/root.tex @@ -1,62 +1,68 @@ \documentclass[10pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{amssymb} \usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} \usepackage{graphicx} \usepackage{isabelle} \usepackage{isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{pdfsetup} \urlstyle{tt} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \renewcommand{\isacharunderscore}{\_} \begin{document} \title{Formalization of Knuth--Bendix Orders for Lambda-Free Higher-Order Terms} \author{Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand} \maketitle \begin{abstract} \noindent This Isabelle/HOL formalization defines Knuth--Bendix orders for higher-order terms without $\lambda$-ab\-strac\-tion and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on first-order terms. It appears promising as the basis of a higher-order superposition calculus. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt \parskip 0.5ex \section{Introduction} This Isabelle/HOL formalization defines Knuth--Bendix orders for higher-order terms without $\lambda$-abstraction and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on first-order terms. It appears promising as the basis of a higher-order superposition calculus. -We refer to our CADE-26 paper for details.% -\footnote{\url{https://www21.in.tum.de/~blanchet/lambda_free_kbo_conf.pdf}} +We refer to the following conference paper for details: + +\begin{quote} +Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand: \\ +A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. \\ +CADE 2017: 432-453 \\ +\url{https://www21.in.tum.de/~blanchet/lambda_free_kbo_conf.pdf} +\end{quote} % generated text of all theories \input{session} % optional bibliography %\bibliographystyle{abbrv} %\bibliography{root} %\bibliographystyle{abbrv} %\bibliography{bib} \end{document} diff --git a/thys/Lambda_Free_RPOs/document/root.tex b/thys/Lambda_Free_RPOs/document/root.tex --- a/thys/Lambda_Free_RPOs/document/root.tex +++ b/thys/Lambda_Free_RPOs/document/root.tex @@ -1,64 +1,70 @@ \documentclass[10pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{amssymb} \usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} \usepackage{graphicx} \usepackage{isabelle} \usepackage{isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{pdfsetup} \urlstyle{tt} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \renewcommand{\isacharunderscore}{\_} \begin{document} \title{Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms} \author{Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand} \maketitle \begin{abstract} \noindent This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without $\lambda$-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt \parskip 0.5ex \section{Introduction} This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without $\lambda$-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus. -We refer to our FoSSaCS~2017 paper for details.% -\footnote{\url{https://www21.in.tum.de/~blanchet/lambda_free_rpo_conf.pdf}} +We refer to the following conference paper for details: + +\begin{quote} +Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand: \\ +A Lambda-Free Higher-Order Recursive Path Order. \\ +FoSSaCS 2017: 461-479 \\ +\url{https://www.cs.vu.nl/~jbe248/lambda_free_rpo_conf.pdf} +\end{quote} % generated text of all theories \input{session} % optional bibliography %\bibliographystyle{abbrv} %\bibliography{root} %\bibliographystyle{abbrv} %\bibliography{bib} \end{document} diff --git a/thys/Nested_Multisets_Ordinals/document/root.tex b/thys/Nested_Multisets_Ordinals/document/root.tex --- a/thys/Nested_Multisets_Ordinals/document/root.tex +++ b/thys/Nested_Multisets_Ordinals/document/root.tex @@ -1,71 +1,77 @@ \documentclass[10pt,a4paper]{article} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{amssymb} \usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} \usepackage{graphicx} \usepackage{isabelle} \usepackage{isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{pdfsetup} \urlstyle{tt} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \renewcommand{\isacharunderscore}{\_} \begin{document} \title{Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals} \author{Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel} \maketitle \begin{abstract} \noindent This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals---the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt \parskip 0.5ex \section{Introduction} This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals---the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type. In addition, signed (or hybrid) multisets are provided (i.e., multisets with -potentially negative multiplicities), as well as signed hereditary multisets +possibly negative multiplicities), as well as signed hereditary multisets and signed ordinals (e.g., $\omega^2 - 2\omega + 1$). -%We refer to our draft paper for details.% -%\footnote{\url{https://members.loria.fr/JCBlanchette/lambda_free_rpo_conf.pdf}} +We refer to the following conference paper for details: + +\begin{quote} +Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel: \\ +Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. \\ +FSCD 2017: 11:1-11:18 \\ +\url{https://hal.inria.fr/hal-01599176/document} +\end{quote} % generated text of all theories \input{session} % optional bibliography %\bibliographystyle{abbrv} %\bibliography{root} %\bibliographystyle{abbrv} %\bibliography{bib} \end{document} diff --git a/thys/Ordered_Resolution_Prover/document/root.tex b/thys/Ordered_Resolution_Prover/document/root.tex --- a/thys/Ordered_Resolution_Prover/document/root.tex +++ b/thys/Ordered_Resolution_Prover/document/root.tex @@ -1,80 +1,98 @@ \documentclass[10pt,a4paper]{article} \usepackage{amssymb} \usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} \usepackage{graphicx} \usepackage{isabelle} \usepackage{isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{pdfsetup} \urlstyle{tt} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \renewcommand{\isacharunderscore}{\_} \begin{document} \title{Formalization of Bachmair and Ganzinger's \\ Ordered Resolution Prover} \author{Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann} \maketitle \begin{abstract} \noindent This Isabelle/HOL formalization covers Sections 2 to 4 of Bachmair and Ganzinger's ``Resolution Theorem Proving'' chapter in the \emph{Handbook of Automated Reasoning}. This includes soundness and completeness of unordered and ordered variants of ground resolution with and without literal selection, the standard redundancy criterion, a general framework for refutational theorem proving, and soundness and completeness of an abstract first-order prover. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt \parskip 0.5ex \section{Introduction} Bachmair and Ganzinger's ``Resolution Theorem Proving'' chapter %\cite{bachmair-ganzinger-2001} in the \emph{Handbook of Automated Reasoning} is the standard reference on the topic. It defines a general framework for propositional and first-order resolution-based theorem proving. Resolution forms the basis for superposition, the calculus implemented in many popular automatic theorem provers. \medskip This Isabelle/HOL formalization covers Sections 2.1, 2.2, 2.4, 2.5, 3, 4.1, 4.2, and 4.3 of Bachmair and Ganzinger's chapter. Section 2 focuses on preliminaries. Section 3 introduces unordered and ordered variants of ground resolution with and without literal selection and proves them refutationally complete. Section 4.1 presents a framework for theorem provers based on -refutation and saturation. Finally, Section 4.2 generalizes the refutational +refutation and saturation. Section 4.2 generalizes the refutational completeness argument and introduces the standard redundancy criterion, which -can be used in conjunction with ordered resolution. Section 4.3 lifts the -result to a first-order prover, specified as a calculus. Figure~\ref{fig:thys} -shows the corresponding Isabelle theory structure. +can be used in conjunction with ordered resolution. Finally, Section 4.3 lifts +the result to a first-order prover, specified as a calculus. +Figure~\ref{fig:thys} shows the corresponding Isabelle theory structure. + +\medskip + +We refer to the following publications for details: + +\begin{quote} +Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann: \\ +Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. \\ +IJCAR 2018: 89-107 \\ +\url{http://matryoshka.gforge.inria.fr/pubs/rp_paper.pdf} + +\medskip + +Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann: \\ +Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. \\ +Journal of Automated Reasoning \\ +\url{http://matryoshka.gforge.inria.fr/pubs/rp_article.pdf} +\end{quote} \begin{figure} \begin{center} \includegraphics[width=0.75\textwidth,keepaspectratio]{session_graph} \end{center} \caption{Theory dependency graph} \label{fig:thys} \end{figure} % generated text of all theories \input{session} % optional bibliography % \bibliographystyle{abbrv} % \bibliography{bib} \end{document} diff --git a/thys/Sort_Encodings/document/root.tex b/thys/Sort_Encodings/document/root.tex --- a/thys/Sort_Encodings/document/root.tex +++ b/thys/Sort_Encodings/document/root.tex @@ -1,65 +1,65 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Sound and Complete Sort Encodings \\for First-Order Logic} \author{Jasmin Christian Blanchette and Andrei Popescu} \date{} \maketitle \begin{abstract} This is a formalization of the soundness and completeness properties for various efficient encodings of sorts in unsorted first-order logic used by Isabelle's Sledgehammer tool. The results are reported in -\cite[\S2,3]{blanchette-et-al-2013-types-conf} and the formalization itself +\cite[\S2,3]{blanchette-et-al-2013-types-conf}, and the formalization itself is presented in \cite[\S3--5]{froc}. % -Essentially, the encodings proceed as follows: a many-sorted problem is -decorated with (as few as possible) tags or guards that make the problem monotonic; -then sorts can be soundly erased. +The encodings proceed as follows:\ a many-sorted problem is decorated with (as +few as possible) tags or guards that make the problem monotonic; then sorts can +be soundly erased. % The proofs rely on monotonicity criteria recently introduced by -Claessen, Lilliestr{\"o}m and Smallbone \cite{claessen-et-al-2011}. - +Claessen, Lilliestr{\"o}m, and Smallbone \cite{claessen-et-al-2011}. -The development employs a formalization of many-sorted first-order logic in clausal -form (clauses, structures and the basic properties of the satisfaction relation), which could be -of interest as the starting point for other formalizations of first-order logic metatheory. -% +The development employs a formalization of many-sorted first-order logic in +clausal form (clauses, structures, and the basic properties of the satisfaction +relation), which could be of interest as the starting point for other +formalizations of first-order logic metatheory. + \end{abstract} \bibliographystyle{abbrv} \bibliography{root} \newpage \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: