refman is the directory for manul. Style changes and small fixes. (#202)

* refman is the directory for manul. It has a Makefile

* Format changes (b5, small margin) to reference manual

* LISA becomes Lisa

* pull out title page

* Formatted kernel proof system to fit pages

* wider margins

* Fixed reference

* change margins again. Added text showing margin width with our font is similar to that of LNCS

.gitignore

@@ -18,4 +18,7 @@ silex/*
 scallion/*
 
 # caching of theorems
-cache
+cache
\ No newline at end of file
+
+# emacs backup files
+*~

Reference Manual/lisa.tex

-% !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}
\ No newline at end of file

refman/.gitignore

+lisa.aux
+lisa.bbl
+lisa.blg
+lisa.fdb_latexmk
+lisa.fls
+lisa.log
+lisa.out
+lisa.toc

refman/Makefile

+# Makefile for compiling lisa.tex using latexmk
+
+# Default target
+all: lisa.pdf
+
+lisa.pdf: lisa.tex kernel.tex  lisa.tex  macro.tex  prooflib.tex  quickguide.tex  shortcuts.tex  theory.tex  theorytopics.tex
+	latexmk lisa.tex
+
+# Clean target
+clean:
+	latexmk -c lisa.tex

refman/alttitlepage.tex

+%\newfontfamily\titlefont{Arial}
+\begin{titlepage}
+\sf
+%\fontfamily{\sfdefault}\selectfont
+
+    \begin{center}
+        \vspace*{1cm}
+ 
+        \textbf{\Huge \ourtitle}
+
+        \vspace{1.5cm}
+        
+        {\Large \ournames}
+             
+        \vspace{1.5cm}
+ 
+        {\Large Laboratory for Automated Reasoning and Analysis \\[1ex] EPFL, Switzerland}
+
+    \end{center}
+
+   \vfill
+
+   \begin{center}
+   \Large
+     \textbf{\large \today}
+   \end{center}
+
+   %% \begin{flushright}
+   %%  \begin{minipage}{15em}
+   %%    \Large
+   %%       Contributors: \\[1ex]
+   %%      \hspace*{3em} \begin{tabular}{l}
+   %%       Simon Guilloud\\
+   %%       Sankalp Gambhir
+   %%      \end{tabular}
+   %%  \end{minipage}
+   %% \end{flushright}
+             
+ \end{titlepage}

refman/lisa.tex

+% !TEX program = xelatex
+
+% Page size:
+\documentclass[11pt,b5paper]{book}
+  % Reduce margins whatever the original text area size was.
+  \edef\mtht{\the\textheight}
+  \edef\mtwd{\dimexpr\the\textwidth+1cm}
+  \usepackage[paperwidth=\dimexpr\mtwd+1.4cm\relax,
+              paperheight=\dimexpr\mtht+1.8cm\relax,
+              text={\mtwd,\mtht},
+              left=0.7cm,
+              top=1.3cm]{geometry}
+
+\input{macro} % also imports
+\input{shortcuts} 
+
+\newcommand{\ourtitle}{Lisa Manual}
+\newcommand{\ournames}{Simon Guilloud, Sankalp Gambhir, Viktor Kun\v{c}ak}
+\title{\ourtitle}
+\author{\ournames}
+\date{}
+
+% PDF links and meta data
+\usepackage{hyperref} 
+\makeatletter
+\hypersetup{
+    colorlinks=true,
+    linkcolor=blue,
+    filecolor=magenta,      
+    urlcolor=blue,
+    pdftitle={\@title},
+    pdfauthor={\@author}
+}
+\makeatother
+\urlstyle{same}
+
+\begin{document} 
+\input{titlepage.tex}
+
+% Uncomment once the chapter says something useful to readers as opposed to authors:
+%\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}

Reference Manual/macro.tex → refman/macro.tex

@@ -12,7 +12,6 @@
 \usepackage[dvipsnames]{xcolor}
 \usepackage{csquotes}
 \usepackage[strings]{underscore}
-\usepackage{hyperref} 
 \usepackage{bussproofs}
 \usepackage{makecell}
 \usepackage{subcaption}
@@ -24,6 +23,7 @@
 \usepackage[T1]{fontenc}
 \usepackage{newunicodechar} %To map unicode in listings to a different font than Fira Code
 \renewcommand\sfdefault{ua1}
+
 \sloppy % better (?) margin handling
 
 
@@ -47,20 +47,6 @@
 \newcommand*{\definitionautorefname}{Definition}
 
 
-% URLs
-
-\hypersetup{
-    colorlinks=true,
-    linkcolor=blue,
-    filecolor=magenta,      
-    urlcolor=blue,
-    pdftitle={LISA Reference Manual},
-    pdfpagemode=FullScreen,
-}
-\urlstyle{same}
-
-
-
 %  Code fonts
 
 %\usepackage{lstfiracode}
@@ -79,6 +65,7 @@
 
 
 %  Correct lstlisting parsing of unicode character. Add unicode points at the end.
+% To add: code for \vdash 
 \makeatletter
 \lst@InputCatcodes
 \def\lst@DefEC{%
@@ -104,7 +91,7 @@
 \def\verbatim@nolig@list{}
 \makeatother
 
-\definecolor{green}{rgb}{0, 0.6, 0}
+\definecolor{green}{rgb}{0, 0.35, 0}
 
 \definecolor{comments}{RGB}{80,0,110}
 

Reference Manual/prooflib.tex → refman/prooflib.tex

 \chapter{Developping Mathematics with Prooflib}
 \label{chapt:prooflib}
-LISA's kernel offers all the necessary tools to develops proofs, but  reading and writing proofs written directly in its language is cumbersome. 
-To develop and maintain a library of mathematical development, LISA offers a dedicate interface and DSL to write proofs: Prooflib
-LISA provides a canonical way of writing and organizing Kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features.
-\autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in LISA.
+Lisa's kernel offers all the necessary tools to develops proofs, but  reading and writing proofs written directly in its language is cumbersome. 
+To develop and maintain a library of mathematical development, Lisa offers a dedicate interface and DSL to write proofs: Prooflib
+Lisa provides a canonical way of writing and organizing Kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features.
+\autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in Lisa.
 
 \begin{figure}
 \begin{lstlisting}[language=lisa, frame=single]
@@ -33,7 +33,7 @@ object MyTheoryName extends lisa.Main {
 
 }
 \end{lstlisting}
-\caption{An example of a theory file in LISA}
+\caption{An example of a theory file in Lisa}
 \label{fig:theoryFileExample}
 \end{figure}
 
@@ -75,7 +75,7 @@ Formally, the proof in (...) is a proof of $P(c) \vdash \phi$. This can be trans
 \end{center}
 Not that for this step to be correct, $c$ must not be free in $\phi$. This correspond to the fact that $c$ is an arbitrary free symbol.
 
-This simulation is provided by LISA through the \lstinline|witness|{} method. It takes as argument a fact showing $\exists x. P(x)$, and introduce a new symbol with the desired property. For an example, see figure \ref{fig:localDefinitionExample}.
+This simulation is provided by Lisa through the \lstinline|witness|{} method. It takes as argument a fact showing $\exists x. P(x)$, and introduce a new symbol with the desired property. For an example, see figure \ref{fig:localDefinitionExample}.
 
 \begin{figure}
   \begin{lstlisting}[language=lisa, frame=single]
@@ -86,7 +86,7 @@ This simulation is provided by LISA through the \lstinline|witness|{} method. It
             c.definition, emptySetAxiom of (x:= c))
     }
   \end{lstlisting}
-  \caption{An example use of local definitions in LISA}
+  \caption{An example use of local definitions in Lisa}
   \label{fig:localDefinitionExample}
   \end{figure}
 

Reference Manual/quickguide.tex → refman/quickguide.tex

-\chapter{Quick Guide for writing proofs in LISA}
+\chapter{Starting with Proofs in Lisa}
 \label{chapt:quickguide}
-LISA is a proof assistant, i.e. a tool to help humans to write completely formal proofs of mathematical statements. 
+Lisa is a proof assistant. Proof assistants support development of formal proofs of mathematical statements. 
 
-The centerpiece of LISA (called the kernel) contains a definition of first order logic (FOL), which is a logical framework to make formal mathematical statements and proofs. This kernel is what provides correctness guarantees to the user. It only accepts a small set of formal deduction rule such as ``if $a$ is true and $b$ is true then $a\land b$ is true". 
-This is in contrast with human-written proofs, which can contain a wide variety of complex or implicit arguments. Hence, if a proof is accepted as being correct by the kernel, we are guaranteed that it indeed is\footnote{Of course, it is always possible that the kernel itself has a bug in its implementation, but because it is a very small and simple program, we can build strong confidence that it is correct.}.
-LISA's kernel is described in details in \autoref{chapt:kernel}.
+The centerpiece of Lisa (called the \emph{kernel}) contains a mechanized implementation of first order logic (FOL), a logical framework to write mathematical statements and their proofs. This kernel is what provides correctness guarantees to the user. The kernel only accepts a small set of formal deduction rule such as ``if $a$ is true and $b$ is true then $a\land b$ is true''.
+This is in contrast to human-written proofs, which may contain a wide variety of complex or implicit arguments. If a proof is accepted as being correct by the kernel, it is expected to meet objective criteria for valid proofs according to the field of formal mathematical logic.\footnote{It is possible that the kernel itself has an implementation bug, but because it is a very small and simple program available in open source, we can build strong confidence that it is correct.}
+Lisa's kernel is described in more detail in \autoref{chapt:kernel}.
 
-However, building advanced math such as topology or probability theory only from those primitive constructions would be excessively tedious. Instead, we use them as primitive building blocs which can be combined and automatized. Beyond the correctness guarantees of the kernel, LISA's purpose is to provide tools to make writing formal proofs easier. This include automation, via decision procedure which automatically prove theorems and deductions, and layers of abstraction (helpers, domain specific language) which make the presentation of formal statements and proofs closer to the traditional, human way of writing proofs. 
-This is not unlike programming languages: assembly is in theory sufficient to write any program on a computer, but high level programming languages offer many convenient features which make writing complex programs easier and which are ultimately translated into assembly. 
-\autoref{chapt:prooflib} explain in details how all these layers of abstraction and automation work. The rest of the present chapter will give a quick guide on how to use LISA. If you are not familiar with first order logic, we suggest you first read an introduction to first order logic such as \url{lara.epfl.ch/w/sav08/predicate_logic_informally}.
+Writing mathematical theories (for example, group theory, combinatorics, topology, theory of computation) directly from these primitive constructions would be tedious. Instead, we use them as building blocs that can be combined and automatized. Beyond the correctness guarantees of the kernel, Lisa's purpose is to provide tools to make writing formal proofs easier. This include automation, via search procedures that automatically prove theorems, and layers of abstraction (helpers, domain specific language), which make the presentation of formal statements and proofs closer to the traditional, human way of writing proofs. 
+This is similar to programming languages: machine language is sufficient to write any program on a computer, but high level programming languages offer many convenient features which make writing complex programs easier and which are ultimately translated into assembly automatically. 
+\autoref{chapt:prooflib} explains how these layers of abstraction and automation work. The rest of the present chapter gives a quick guide on how to use Lisa.
 
 \section{Installation}
-LISA requires the Scala programming language to run. You can download and install Scala following \url{www.scala-lang.org/download/}. Once this is done, clone the LISA repository:
+Lisa requires the Scala programming language to run. You can download and install Scala following the instructions at the Scala home page\footnote{\url{www.scala-lang.org/}}. Subsequently, clone the Lisa git repository:
 \begin{lstlisting}[language=console]
 > git clone https://github.com/epfl-lara/lisa
 \end{lstlisting}
@@ -20,37 +20,36 @@ To test your installation, do
 > cd lisa
 > sbt
 \end{lstlisting}
-SBT is a tool to run scala project and manage versions and dependencies. When it finished loading, do
+\lstinline|sbt| is a tool to run a Scala project and manage versions and dependencies. Once inside sbt, run the following commands:
 \begin{lstlisting}[language=console]
 > project lisa-examples
 > run
 \end{lstlisting}
-Wait for the LISA codebase to be compiled and then press the number corresponding to "Example". You should obtain the following result:
+Wait for the Lisa codebase to be compiled and then press the number corresponding to "Example". You should obtain the result demonstrating some example theorems proven, such as the following:
+
 \noindent\begin{minipage}{\linewidth}\vspace{1em}
 \begin{lstlisting}[language=console]
   @*Theorem fixedPointDoubleApplication := 
-    ∀'x. 'P('x) ==> 'P('f('x)) ⊢ 'P('x) ==> 'P('f('f('x)))
+    ∀'x. 'P('x) ==> 'P('f('x)) |- 'P('x) ==> 'P('f('f('x)))
 
-  Theorem emptySetIsASubset := ⊢ subsetOf(emptySet, 'x)
+  Theorem emptySetIsASubset := |- subsetOf(emptySet, 'x)
 
   Theorem setWithElementNonEmpty := 
-    elem('y, 'x) ⊢ ¬('x = emptySet)
+    elem('y, 'x) |- ¬('x = emptySet)
 
-  Theorem powerSetNonEmpty := ⊢ ¬(powerSet('x) = emptySet)
+  Theorem powerSetNonEmpty := |- ¬(powerSet('x) = emptySet)
   *@
 \end{lstlisting}
 \end{minipage}
 
-
-
 \section{Development Environment}
-To write LISA proofs, you can use any text editor or IDE. We recommend using \emph{Visual Studio Code} with the \emph{Metals} plugin.
+To write Lisa proofs, you can use any text editor or IDE. We recommend using \emph{Visual Studio Code} (henceforth VSCode) with the \emph{Metals} plugin.
 
 \subsection*{A Note on Special Characters}
-Math is full of special character. Lisa usually admits both an ascii name and a unicode name for such symbols. By enabling ligatures, common ascii characters such as \lstinline|=|\lstinline|=|\lstinline|>| are rendered as \lstinline|==>|. 
-The present document uses the font \href{https://github.com/tonsky/FiraCode}{Fira Code}. Once installed on your system, you can activate it and ligatures on VSCode the following way:
+Math often uses symbols beyond the Latin alphabet. Lisa usually admits both an English alphabet name and a unicode name for such symbols. By enabling \emph{font ligatures}, common character sequences, such as \lstinline|=|\lstinline|=|\lstinline|>| are rendered as \lstinline|==>|. 
+The present document also uses the font \href{https://github.com/tonsky/FiraCode}{Fira Code}. Once installed on your system, you can activate it and ligatures on VSCode the following way:
 \begin{enumerate}
-  \item Press ctrl-shift-P
+  \item Press Ctrl-Shift-P
   \item Search for ``Open User Settings (JSON)''
   \item in the \lstinline|settings.json| file, add:
   \begin{lstlisting}
@@ -58,7 +57,7 @@ The present document uses the font \href{https://github.com/tonsky/FiraCode}{Fir
 "editor.fontLigatures": true,
   \end{lstlisting}
 \end{enumerate}
-Other symbols such as \lstinline|∀| are unicode symbols, which can be entered via their unicode code, depending on your OS\footnote{alt+numpad on windows, ctrl-shift-U+code on Linux}, or by using an extension for VS Code such as \emph{Fast Unicode Math Characters}, \emph{Insert Unicode} or \emph{Unicode Latex}.
+Other symbols such as \lstinline|∀| are Unicode symbols, which can be entered via their unicode code, depending on your OS\footnote{alt+numpad on windows, Ctrl-Shift-U+code on Linux}, or by using an extension for VS Code such as \emph{Fast Unicode Math Characters}, \emph{Insert Unicode} or \emph{Unicode Latex}.
 A cheat sheet of the most common symbols and how to input them is in \autoref{tab:Unicode}.
 \begin{table}
   \center
@@ -75,13 +74,13 @@ A cheat sheet of the most common symbols and how to input them is in \autoref{ta
     \lstinline| ⊆   | & U+2286           & subseteq \\ \hline
     \lstinline| ∅   | & U+2205           & emptyset \\ 
   \end{tabular}
-  \caption{Most frequently used Unicode symbols and ligatures.}
+  \caption{Frequently used Unicode symbols and ligatures.}
   \label{tab:Unicode}
 \end{table}
-Note that by default, unicode characters will not be printed correctly on a Windows console. You will need to activate the corresponding charset and pick a font with support for unicode in your console's options, such as Consolas.
+Note that by default, Unicode characters may not be printed correctly on a Windows console. You will need to activate the corresponding charset and pick a font with support for unicode in your console's options, such as Consolas.
 
 \section{Writing theory files}
-LISA provides a canonical way of writing and organizing kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features.
+Lisa provides a canonical way of writing and organizing kernel proofs by mean of a set of utilities and a domain-specific language (DSL) made possible by some of Scala's features.
 To prove some theorems by yourself, start by creating a file named \lstinline|MyTheoryName.scala| right next to the Example.scala file\footnote{The relative path is lisa/lisa-examples/src/main/scala}.
 Then simply write:
 
@@ -92,11 +91,11 @@ object MyTheoryName extends lisa.Main {
 }
 \end{lstlisting}
 \end{minipage}
-and that's it! This will give you access to all the necessary LISA features. Let see how one can use them to prove a theorem:
+and that's it! This will give you access to all the necessary Lisa features. Let see how one can use them to prove a theorem:
 $$
   \forall x. P(x) \implies P(f(x)) \vdash P(x) \implies P(f(f(x)))
 $$
-To state the theorem, we first need to tell LISA that $x$ is a variable, $f$ is a function symbol and $P$ a predicate symbol. 
+To state the theorem, we first need to tell Lisa that $x$ is a variable, $f$ is a function symbol and $P$ a predicate symbol. 
 
 \noindent\begin{minipage}{\linewidth}\vspace{1em}
 \begin{lstlisting}[language=lisa, frame=single]
@@ -109,7 +108,7 @@ object MyTheoryName extends lisa.Main {
 \end{lstlisting}
 \end{minipage}
 
-where \lstinline|[1]| indicates that the symbol is of arity 1 (it takes a single argument). The symbols \lstinline|x, f, P| are scala identifiers that can be freely used in theorem statements and proofs, but they are also formal symbols of FOL in LISA's kernel. 
+where \lstinline|[1]| indicates that the symbol is of arity 1 (it takes a single argument). The symbols \lstinline|x, f, P| are scala identifiers that can be freely used in theorem statements and proofs, but they are also formal symbols of FOL in Lisa's kernel. 
 We now can state our theorem:
 
 \noindent\begin{minipage}{\linewidth}\vspace{1em}
@@ -148,14 +147,14 @@ object MyTheoryName extends lisa.Main {
 \end{lstlisting}
 \end{minipage}
 First, we use the \lstinline|assume| construct in line 6.
-This tells to LISA that the assumed formula is understood as being implicitly on the left hand side of every statement in the rest of the proof. 
+This tells to Lisa that the assumed formula is understood as being implicitly on the left hand side of every statement in the rest of the proof. 
 
 Then, we need to instantiate the quantified formula twice using a specialized tactic. In lines 7 and 8, we use \lstinline|have| to state that a formula or sequent is true (given the assumption inside \lstinline|assume|), and that the proof of this is produced by the tactic \lstinline|InstantiateForall|.
 We'll see more about the interface of a tactic later. To be able to reuse intermediate steps at any point later, we also assign the intermediates step to a variable.
 
 Finally, the last line says that the conclusion of the theorem itself, \lstinline|thesis|, can be proven using the tactic \lstinline|Tautology| and the two intermediate steps we reached. \lstinline|Tautology| is a tactic that is able to do reasoning with propositional connectives. It implements a complete decision procedure for propositional logic that is described in \autoref{tact:Tautology}.
 
-LISA is based on set theory, so you can also use set-theoretic primitives such as in the following theorem.
+Lisa is based on set theory, so you can also use set-theoretic primitives such as in the following theorem.
 
 \noindent\begin{minipage}{\linewidth}\vspace{1em}
   \begin{lstlisting}[language=lisa, frame=single]
@@ -194,7 +193,7 @@ is equivalent to
   \end{lstlisting}
 \end{minipage}
 
-LISA also allows to introduce definitions. There are essentially two kind of definitions, \emph{aliases} and definition via \emph{unique existence}.
+Lisa also allows to introduce definitions. There are essentially two kind of definitions, \emph{aliases} and definition via \emph{unique existence}.
 An alias defines a constant, a function or predicate as being equal (or equivalent) to a given formula or term. For example,
 
 \noindent\begin{minipage}{\linewidth}\vspace{1em}
@@ -283,4 +282,4 @@ If a \lstinline|subst| is a formula rather than a proven fact, then it should be
   have(Q(s) /\ s===f(t)) by ???
   thenHave(A, f(t) === t |- P(s) /\ s===t) 
       .by Substitution.ApplyRules(subst, f(t) === t)
-\end{lstlisting}
+\end{lstlisting}
\ No newline at end of file

refman/r

+latexmk lisa.tex

Reference Manual/theory.tex → refman/theory.tex

@@ -9,20 +9,20 @@ Actual mathematical functions on the other hand, are proper sets which contains
 
 Indeed, on one hand a predicate symbol defines a truth value on all possible sets, but on the other hand it is impossible to use the symbol alone, without applying it to arguments, or to quantify over function symbol.
 
-LISA is based on set theory. More specifically, it is based on ZF with (still not decided) an axiom of choice, of global choice, or Tarski's universes.
+Lisa is based on set theory. More specifically, it is based on ZF with (still not decided) an axiom of choice, of global choice, or Tarski's universes.
 
 ZF Set Theory stands for Zermelo-Fraenkel Set Theory. It contains a set of initial predicate symbols and function symbols, as shown in Figure \ref{fig:symbolszf}. It also contains the 7 axioms of Zermelo (Figure \ref{fig:axiomsz}), which are technically sufficient to formalize a large portion of mathematics, plus the axiom of replacement of Fraenkel (Figure \ref{fig:axiomszf}), which is needed to formalize more complex mathematical theories.
 In a more typical mathematical introduction to Set Theory, ZF would naturally only contain the set membership symbol $\in$. Axioms defining the other symbols would then only express the existence of functions or predicates with those properties, from which we could get the same symbols using extensions by definitions.
 
 In a very traditional sense, an axiomatization is any possibly infinite semi-recursive set of axioms. Hence, in its full generality, Axioms should be any function producing possibly infinitely many formulas.
-This is however not a convenient definition. In practice, all infinite axiomatizations are schematic, meaning that they are expressable using schematic variables. Axioms \ref{axz:comprehension} (comprehension schema) and \ref{axzf:replacement} (replacement schema) are such examples of axiom schema, and motivates the use of schematic variables in LISA.
+This is however not a convenient definition. In practice, all infinite axiomatizations are schematic, meaning that they are expressable using schematic variables. Axioms \ref{axz:comprehension} (comprehension schema) and \ref{axzf:replacement} (replacement schema) are such examples of axiom schema, and motivates the use of schematic variables in Lisa.
 
 
 
 \begin{figure}
   \begin{center}
     \begin{tabular}{l|c|l}
-      {}                         & Math symbol       & LISA Kernel             \\ \hline
+      {}                         & Math symbol       & Lisa Kernel             \\ \hline
       Set Membership predicate   & $\in$             & \lstinline$in(s,t)$     \\
       Subset predicate           & $\subset$         & \lstinline$subset(s,t)$ \\
       Empty Set constant         & $\emptyset$       & \lstinline$emptyset()$  \\
@@ -101,14 +101,14 @@ Note that the replacement axiom \autoref{axzf:replacement} is conditional of the
 $$ \exists B, \forall y. y \in B \iff (\exists x. x \in A \land P(y, e) \land ∀ z. \psi(x, z) \implies z = y) $$
 Which maps elements of $A$ through the functional component of $\psi$ only. If $\psi$ is functional, those are equivalent.
 
-LISA allows to write, for an arbitrary term \lstinline|t| and lambda expression \lstinline|P: (Term, Term) \mapsto Formula|,
+Lisa allows to write, for an arbitrary term \lstinline|t| and lambda expression \lstinline|P: (Term, Term) \mapsto Formula|,
 \begin{center}
   \lstinline|val c = t.replace(P)|
 \end{center}
 One can then use \lstinline|c.elim(e)| to obtain the fact 
 $e \in B \iff (\exists x. x \in A \land P(x, e) \land \forall z. \psi(x, z) \implies z = y)$. As in the case of local definitions, this statement will automatically be eliminated from the context at the end of the proof.
 
-Moreover, we most often want to map a set by a known function. In those case, LISA provides refined versions \lstinline|t.filter|, \lstinline|t.map| and \lstinline|t.collect|, which are detailed in table \ref{tab:comprehensions}. In particular, these versions already prove the functionality requirement of replacement.
+Moreover, we most often want to map a set by a known function. In those case, Lisa provides refined versions \lstinline|t.filter|, \lstinline|t.map| and \lstinline|t.collect|, which are detailed in table \ref{tab:comprehensions}. In particular, these versions already prove the functionality requirement of replacement.
 \begin{table}[h]
   \begin{tabular}{l|l}
     \textbf{\lstinline|val c = |} & \textbf{\lstinline|c.elim(e)|} \\ \hline
@@ -117,7 +117,7 @@ Moreover, we most often want to map a set by a known function. In those case, LI
     \lstinline|t.map(M)| & $e \in c \iff (\exists x. x \in t \land M(x) = e)$ \\
     \lstinline|t.filter(F)| & $e \in c \iff e \in t \land F(e)$ \\   
   \end{tabular}
-  \caption{Comprehensions in LISA}
+  \caption{Comprehensions in Lisa}
   \label{tab:comprehensions}
 \end{table}
 

Reference Manual/theorytopics.tex → refman/theorytopics.tex

 \chapter{Selected Theoretical Topics}
 \label{part:theory}
 
+Algorithms and techniques to solve and reduce formulas in propositional logic (and its generalizations) are a major field of study. They have prime relevance in SAT and SMT solving algorithms. Lisa makes use of some of them: some of the in the kernel, others as available tactics. 
+
 \section{Set Theory and Mathematical Logic}
 \subsection{First Order Logic with Schematic Variables}
 \label{sec:theoryfol}

refman/titlepage.tex

+%\newfontfamily\titlefont{Arial}
+\begin{titlepage}
+\sf
+%\fontfamily{\sfdefault}\selectfont
+
+    \begin{center}
+        \vspace*{1cm}
+ 
+        \textbf{\Huge \ourtitle}
+
+        \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}
+
+   \vfill
+
+   Contributors:
+   \begin{flushright}
+     \large
+     \ournames
+   \end{flushright}
+             
+ \end{titlepage}