summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/LK.tex

changeset 9695 | ec7d7f877712 |

parent 7116 | 8c1caac3e54e |

child 19152 | d81fae81f385 |

--- a/doc-src/Logics/LK.tex Mon Aug 28 13:50:24 2000 +0200 +++ b/doc-src/Logics/LK.tex Mon Aug 28 13:52:38 2000 +0200 @@ -18,8 +18,8 @@ are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which belongs to class {\tt logic}. -\LK{} implements a classical logic theorem prover that is nearly as powerful -as the generic classical reasoner. The simplifier is now available too. +LK implements a classical logic theorem prover that is nearly as powerful as +the generic classical reasoner. The simplifier is now available too. To work in LK, start up Isabelle specifying \texttt{Sequents} as the object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}: @@ -179,17 +179,17 @@ of formulae. The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$ -satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{} -denote something, a description is always meaningful, but we do not know -its value unless $P[x]$ defines it uniquely. The Isabelle notation is -\hbox{\tt THE $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) -does not entail the Axiom of Choice because it requires uniqueness. +satisfying~$P[a]$, if one exists and is unique. Since all terms in LK denote +something, a description is always meaningful, but we do not know its value +unless $P[x]$ defines it uniquely. The Isabelle notation is \hbox{\tt THE + $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not +entail the Axiom of Choice because it requires uniqueness. Conditional expressions are available with the notation \[ \dquotes "if"~formula~"then"~term~"else"~term. \] -Figure~\ref{lk-grammar} presents the grammar of \LK. Traditionally, +Figure~\ref{lk-grammar} presents the grammar of LK. Traditionally, \(\Gamma\) and \(\Delta\) are meta-variables for sequences. In Isabelle's notation, the prefix~\verb|$| on a term makes it range over sequences. In a sequent, anything not prefixed by \verb|$| is taken as a formula. @@ -272,13 +272,13 @@ \section{Automatic Proof} -\LK{} instantiates Isabelle's simplifier. Both equality ($=$) and the +LK instantiates Isabelle's simplifier. Both equality ($=$) and the biconditional ($\bimp$) may be used for rewriting. The tactic \texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not -required; all the formulae{} in the sequent will be simplified. The -left-hand formulae{} are taken as rewrite rules. (Thus, the behaviour is what -you would normally expect from calling \texttt{Asm_full_simp_tac}.) +required; all the formulae{} in the sequent will be simplified. The left-hand +formulae{} are taken as rewrite rules. (Thus, the behaviour is what you would +normally expect from calling \texttt{Asm_full_simp_tac}.) For classical reasoning, several tactics are available: \begin{ttbox} @@ -325,15 +325,13 @@ These tactics refine a subgoal into two by applying the cut rule. The cut formula is given as a string, and replaces some other formula in the sequent. \begin{ttdescription} -\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] -reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It -then deletes some formula from the right side of subgoal~$i$, replacing -that formula by~$P$. - -\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] -reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It -then deletes some formula from the left side of the new subgoal $i+1$, -replacing that formula by~$P$. +\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and + applies the cut rule to subgoal~$i$. It then deletes some formula from the + right side of subgoal~$i$, replacing that formula by~$P$. + +\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and + applies the cut rule to subgoal~$i$. It then deletes some formula from the + left side of the new subgoal $i+1$, replacing that formula by~$P$. \end{ttdescription} All the structural rules --- cut, contraction, and thinning --- can be applied to particular formulae using {\tt res_inst_tac}. @@ -378,11 +376,11 @@ \section{A simple example of classical reasoning} The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the -classical treatment of the existential quantifier. Classical reasoning -is easy using~{\LK}, as you can see by comparing this proof with the one -given in the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the -proofs are essentially the same; the key step here is to use \tdx{exR} -rather than the weaker~\tdx{exR_thin}. +classical treatment of the existential quantifier. Classical reasoning is +easy using~LK, as you can see by comparing this proof with the one given in +the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs +are essentially the same; the key step here is to use \tdx{exR} rather than +the weaker~\tdx{exR_thin}. \begin{ttbox} Goal "|- EX y. ALL x. P(y)-->P(x)"; {\out Level 0} @@ -405,10 +403,10 @@ {\out |- EX y. ALL x. P(y) --> P(x)} {\out 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)} \end{ttbox} -Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not -become an assumption; instead, it moves to the left side. The -resulting subgoal cannot be instantiated to a basic sequent: the bound -variable~$x$ is not unifiable with the unknown~$\Var{x}$. +Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an +assumption; instead, it moves to the left side. The resulting subgoal cannot +be instantiated to a basic sequent: the bound variable~$x$ is not unifiable +with the unknown~$\Var{x}$. \begin{ttbox} by (resolve_tac [basic] 1); {\out by: tactic failed} @@ -548,10 +546,10 @@ Multiple unifiers occur whenever this is resolved against a goal containing more than one conjunction on the left. -\LK{} exploits this representation of lists. As an alternative, the -sequent calculus can be formalized using an ordinary representation of -lists, with a logic program for removing a formula from a list. Amy Felty -has applied this technique using the language $\lambda$Prolog~\cite{felty91a}. +LK exploits this representation of lists. As an alternative, the sequent +calculus can be formalized using an ordinary representation of lists, with a +logic program for removing a formula from a list. Amy Felty has applied this +technique using the language $\lambda$Prolog~\cite{felty91a}. Explicit formalization of sequents can be tiresome. But it gives precise control over contraction and weakening, and is essential to handle relevant @@ -575,10 +573,10 @@ rules require a search strategy, such as backtracking. A \textbf{pack} is a pair whose first component is a list of safe rules and -whose second is a list of unsafe rules. Packs can be extended in an -obvious way to allow reasoning with various collections of rules. For -clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is -essentially a type synonym: +whose second is a list of unsafe rules. Packs can be extended in an obvious +way to allow reasoning with various collections of rules. For clarity, LK +declares \mltydx{pack} as an \ML{} datatype, although is essentially a type +synonym: \begin{ttbox} datatype pack = Pack of thm list * thm list; \end{ttbox} @@ -628,8 +626,7 @@ \section{*Proof procedures}\label{sec:sequent-provers} -The \LK{} proof procedure is similar to the classical reasoner -described in +The LK proof procedure is similar to the classical reasoner described in \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}}. %