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

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.