doc-src/Logics/LK.tex
changeset 291 a615050a7494
parent 264 ca6eb7e6e94f
child 316 813ee27cd4d5
--- a/doc-src/Logics/LK.tex	Tue Mar 22 12:43:51 1994 +0100
+++ b/doc-src/Logics/LK.tex	Wed Mar 23 11:10:16 1994 +0100
@@ -1,5 +1,5 @@
 %% $Id$
-\chapter{First-order sequent calculus}
+\chapter{First-Order Sequent Calculus}
 The directory~\ttindexbold{LK} implements classical first-order logic through
 Gentzen's sequent calculus (see Gallier~\cite{gallier86} or
 Takeuti~\cite{takeuti87}).  Resembling the method of semantic tableaux, the
@@ -244,7 +244,7 @@
 \ttindex{res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
 specifying the formula to duplicate.
 
-See the files \ttindexbold{LK/lk.thy} and \ttindexbold{LK/lk.ML}
+See the files {\tt LK/lk.thy} and {\tt LK/lk.ML}
 for complete listings of the rules and derived rules.
 
 
@@ -279,7 +279,7 @@
 
 \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 let side of the new subgoal $i+1$,
+then deletes some formula from the left side of the new subgoal $i+1$,
 replacing that formula by~$P$.
 \end{description}
 All the structural rules --- cut, contraction, and thinning --- can be
@@ -309,10 +309,11 @@
 checks that each conclusion formula is unifiable (using {\tt could_unify})
 with some subgoal formula.
 
-\item[\ttindexbold{could_resolve} $(t,u)$] 
-tests whether two sequents could be resolved.  Sequent $t$ is a premise
-(subgoal), while $u$ is the conclusion of an object-rule.  It uses {\tt
-could_res} to check the left and right sides of the two sequents.
+\item[\ttindexbold{could_resolve_seq} $(t,u)$] 
+  tests whether two sequents could be resolved.  Sequent $t$ is a premise
+  (subgoal), while $u$ is the conclusion of an object-rule.  It simply
+  calls {\tt could_res} twice to check that both the left and the right
+  sides of the sequents are compatible.
 
 \item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}] 
 uses {\tt filter_thms could_resolve} to extract the {\it thms} that are
@@ -324,10 +325,10 @@
 
 
 \section{Packaging sequent rules}
-For theorem proving, rules can be classified as {\bf safe} or {\bf
-unsafe}.  An unsafe rule (typically a weakened quantifier rule) may reduce
-a provable goal to an unprovable set of subgoals, and should only be used
-as a last resort.  
+For theorem proving, rules can be classified as {\bf safe} or {\bf unsafe}.
+An unsafe rule may reduce a provable goal to an unprovable set of subgoals,
+and should only be used as a last resort.  Typical examples are the
+weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.
 
 A {\bf 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
@@ -541,7 +542,7 @@
 \[  \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]
 This does not require special properties of membership; we may
 generalize $x\in y$ to an arbitrary predicate~$F(x,y)$.  The theorem has a
-short manual proof.  See the directory \ttindexbold{LK/ex} for many more
+short manual proof.  See the directory {\tt LK/ex} for many more
 examples.
 
 We set the main goal and move the negated formula to the left.