-
Simon Guilloud authored
This PR introduces methods witness, t.replace, t.collect, t.map and t.filter. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.
Simon Guilloud authoredThis PR introduces methods witness, t.replace, t.collect, t.map and t.filter. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.
lisa.tex 1.38 KiB
% !TEX program = xelatex
\documentclass[11pt,a4paper]{book}
\input{macro}
\input{shortcuts}
\title{LISA Reference Manual (WIP)}
\author{Simon Guilloud\\Laboratory for Automated Reasoning and Analysis, EPFL}
\date{}
\begin{document}
\newfontfamily\titlefont{Arial}
\begin{titlepage}
\titlefont
%\fontfamily{\sfdefault}\selectfont
\begin{center}
\vspace*{1cm}
\textbf{\Huge LISA Reference Manual}
\vspace{1.5cm}
%\textbf{\large Version 0.2.1}
\textbf{\large \today}
\vspace{1.5cm}
{\Large Laboratory for Automated Reasoning and Analysis\\ EPFL, Switzerland}
\vspace{1.5cm}
\date{}
\end{center}
\vspace*{10em}
\begin{flushright}\huge
\begin{tabular}{l}
Contributors: \hspace*{2em} \\[1em]
Simon Guilloud\\
Sankalp Gambhir
\end{tabular}
\end{flushright}
\end{titlepage}
\chapter*{Introduction}
This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations.
\tableofcontents
\input{quickguide.tex}
\input{kernel.tex}
\input{prooflib.tex}
\input{theory.tex}
\input{theorytopics.tex}
\bibliographystyle{plain}
\bibliography{sguilloud.bib}
\end{document}