doc-src/Logics/LK.tex
changeset 104 d8205bb279a7
child 111 1b3cddf41b2d
equal deleted inserted replaced
103:30bd42401ab2 104:d8205bb279a7
       
     1 %% $Id$
       
     2 \chapter{First-order sequent calculus}
       
     3 The directory~\ttindexbold{LK} implements classical first-order logic through
       
     4 Gentzen's sequent calculus (see Gallier~\cite{gallier86} or
       
     5 Takeuti~\cite{takeuti87}).  Resembling the method of semantic tableaux, the
       
     6 calculus is well suited for backwards proof.  Assertions have the form
       
     7 \(\Gamma\turn \Delta\), where \(\Gamma\) and \(\Delta\) are lists of
       
     8 formulae.  Associative unification, simulated by higher-order unification,
       
     9 handles lists.
       
    10 
       
    11 The logic is many-sorted, using Isabelle's type classes.  The
       
    12 class of first-order terms is called {\it term}.  No types of individuals
       
    13 are provided, but extensions can define types such as $nat::term$ and type
       
    14 constructors such as $list::(term)term$.  Below, the type variable $\alpha$
       
    15 ranges over class {\it term\/}; the equality symbol and quantifiers are
       
    16 polymorphic (many-sorted).  The type of formulae is~{\it o}, which belongs
       
    17 to class {\it logic}.  
       
    18 
       
    19 No generic packages are instantiated, since Isabelle does not provide
       
    20 packages for sequent calculi at present.  \LK{} implements a classical
       
    21 logic theorem prover that is as powerful as the generic classical module,
       
    22 except that it does not perform equality reasoning.
       
    23 
       
    24 
       
    25 \section{Unification for lists}
       
    26 Higher-order unification includes associative unification as a special
       
    27 case, by an encoding that involves function composition
       
    28 \cite[page~37]{huet78}.  To represent lists, let $C$ be a new constant.
       
    29 The empty list is $\lambda x.x$, while $[t@1,t@2,\ldots,t@n]$ is
       
    30 represented by
       
    31 \[ \lambda x.C(t@1,C(t@2,\ldots,C(t@n,x))).  \]
       
    32 The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways
       
    33 of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.
       
    34 
       
    35 Unlike orthodox associative unification, this technique can represent certain
       
    36 infinite sets of unifiers by flex-flex equations.   But note that the term
       
    37 $\lambda x.C(t,\Var{a})$ does not represent any list.  Flex-flex equations
       
    38 containing such garbage terms may accumulate during a proof.
       
    39 
       
    40 This technique lets Isabelle formalize sequent calculus rules,
       
    41 where the comma is the associative operator:
       
    42 \[ \infer[\conj\hbox{-left}]
       
    43 	 {\Gamma,P\conj Q,\Delta \turn \Theta}
       
    44          {\Gamma,P,Q,\Delta \turn \Theta}  \] 
       
    45 Multiple unifiers occur whenever this is resolved against a goal containing
       
    46 more than one conjunction on the left.  Explicit formalization of sequents
       
    47 can be tiresome, but gives precise control over contraction and weakening,
       
    48 needed to handle relevant and linear logics.
       
    49 
       
    50 \LK{} exploits this representation of lists.  As an alternative, the
       
    51 sequent calculus can be formalized using an ordinary representation of
       
    52 lists, with a logic program for removing a formula from a list.  Amy Felty
       
    53 has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.
       
    54 
       
    55 
       
    56 \begin{figure} 
       
    57 \begin{center}
       
    58 \begin{tabular}{rrr} 
       
    59   \it name    	&\it meta-type 		& \it description	\\ 
       
    60   \idx{Trueprop}& $o\To prop$		& coercion to $prop$	\\
       
    61   \idx{Seqof}   & $[o,sobj]\To sobj$  	& singleton sequence	\\
       
    62   \idx{Not}	& $o\To o$		& negation ($\neg$) 	\\
       
    63   \idx{True}	& $o$			& tautology ($\top$) 	\\
       
    64   \idx{False}	& $o$			& absurdity ($\bot$)
       
    65 \end{tabular}
       
    66 \end{center}
       
    67 \subcaption{Constants}
       
    68 
       
    69 \begin{center}
       
    70 \begin{tabular}{llrrr} 
       
    71   \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\
       
    72   \idx{ALL}  & \idx{All}  & $(\alpha\To o)\To o$ & 10 & 
       
    73 	universal quantifier ($\forall$) \\
       
    74   \idx{EX}   & \idx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
       
    75 	existential quantifier ($\exists$) \\
       
    76   \idx{THE} & \idx{The}  & $(\alpha\To o)\To \alpha$ & 10 & 
       
    77 	definite description ($\iota$)
       
    78 \end{tabular}
       
    79 \end{center}
       
    80 \subcaption{Binders} 
       
    81 
       
    82 \begin{center}
       
    83 \indexbold{*"=}
       
    84 \indexbold{&@{\tt\&}}
       
    85 \indexbold{*"|}
       
    86 \indexbold{*"-"-">}
       
    87 \indexbold{*"<"-">}
       
    88 \begin{tabular}{rrrr} 
       
    89     \it symbol  & \it meta-type & \it precedence & \it description \\ 
       
    90     \tt = &     $[\alpha,\alpha]\To o$   & Left 50 & equality ($=$) \\
       
    91     \tt \& &    $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
       
    92     \tt | &     $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
       
    93     \tt --> &   $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
       
    94     \tt <-> &   $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) 
       
    95 \end{tabular}
       
    96 \end{center}
       
    97 \subcaption{Infixes}
       
    98 
       
    99 \begin{center}
       
   100 \begin{tabular}{rrr} 
       
   101   \it external		& \it internal	& \it description \\ 
       
   102   \tt $\Gamma$ |- $\Delta$  &  \tt Trueprop($\Gamma$, $\Delta$) &
       
   103         sequent $\Gamma\turn \Delta$ 
       
   104 \end{tabular}
       
   105 \end{center}
       
   106 \subcaption{Translations} 
       
   107 \caption{Syntax of {\tt LK}} \label{lk-syntax}
       
   108 \end{figure}
       
   109 
       
   110 
       
   111 \begin{figure} 
       
   112 \dquotes
       
   113 \[\begin{array}{rcl}
       
   114     prop & = & sequence " |- " sequence 
       
   115 \\[2ex]
       
   116 sequence & = & elem \quad (", " elem)^* \\
       
   117          & | & empty 
       
   118 \\[2ex]
       
   119     elem & = & "\$ " id \\
       
   120          & | & "\$ " var \\
       
   121          & | & formula 
       
   122 \\[2ex]
       
   123  formula & = & \hbox{expression of type~$o$} \\
       
   124 	 & | & term " = " term \\
       
   125 	 & | & "\ttilde\ " formula \\
       
   126 	 & | & formula " \& " formula \\
       
   127 	 & | & formula " | " formula \\
       
   128 	 & | & formula " --> " formula \\
       
   129 	 & | & formula " <-> " formula \\
       
   130 	 & | & "ALL~" id~id^* " . " formula \\
       
   131 	 & | & "EX~~" id~id^* " . " formula \\
       
   132 	 & | & "THE~" id~     " . " formula
       
   133   \end{array}
       
   134 \]
       
   135 \caption{Grammar of {\tt LK}} \label{lk-grammar}
       
   136 \end{figure}
       
   137 
       
   138 
       
   139 \begin{figure} 
       
   140 \begin{ttbox}
       
   141 \idx{basic}       $H, P, $G |- $E, P, $F
       
   142 \idx{thinR}       $H |- $E, $F ==> $H |- $E, P, $F
       
   143 \idx{thinL}       $H, $G |- $E ==> $H, P, $G |- $E
       
   144 \idx{cut}         [| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E
       
   145 \subcaption{Structural rules}
       
   146 
       
   147 \idx{refl}        $H |- $E, a=a, $F
       
   148 \idx{sym}         $H |- $E, a=b, $F ==> $H |- $E, b=a, $F
       
   149 \idx{trans}       [| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> 
       
   150             $H|- $E, a=c, $F
       
   151 \subcaption{Equality rules}
       
   152 
       
   153 \idx{True_def}    True  == False-->False
       
   154 \idx{iff_def}     P<->Q == (P-->Q) & (Q-->P)
       
   155 
       
   156 \idx{conjR}   [| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F
       
   157 \idx{conjL}   $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
       
   158 
       
   159 \idx{disjR}   $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
       
   160 \idx{disjL}   [| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
       
   161             
       
   162 \idx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $
       
   163 \idx{impL}    [| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
       
   164             
       
   165 \idx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
       
   166 \idx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
       
   167 
       
   168 \idx{FalseL}  $H, False, $G |- $E
       
   169 \subcaption{Propositional rules}
       
   170 
       
   171 \idx{allR}    (!!x.$H|- $E, P(x), $F) ==> $H|- $E, ALL x.P(x), $F
       
   172 \idx{allL}    $H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G|- $E
       
   173             
       
   174 \idx{exR}     $H|- $E, P(x), $F, EX x.P(x) ==> $H|- $E, EX x.P(x), $F
       
   175 \idx{exL}     (!!x.$H, P(x), $G|- $E) ==> $H, EX x.P(x), $G|- $E
       
   176 
       
   177 \idx{The}     [| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
       
   178         $H |- $E, P(THE x.P(x)), $F
       
   179 \subcaption{Quantifier rules}
       
   180 \end{ttbox}
       
   181 
       
   182 \caption{Rules of {\tt LK}}  \label{lk-rules}
       
   183 \end{figure}
       
   184 
       
   185 
       
   186 \begin{figure} 
       
   187 \begin{ttbox}
       
   188 \idx{conR}        $H |- $E, P, $F, P ==> $H |- $E, P, $F
       
   189 \idx{conL}        $H, P, $G, P |- $E ==> $H, P, $G |- $E
       
   190 
       
   191 \idx{symL}        $H, $G, B = A |- $E ==> $H, A = B, $G |- $E
       
   192 
       
   193 \idx{TrueR}       $H |- $E, True, $F
       
   194 
       
   195 \idx{iffR}        [| $H, P |- $E, Q, $F;  $H, Q |- $E, P, $F |] ==> 
       
   196             $H |- $E, P<->Q, $F
       
   197 
       
   198 \idx{iffL}        [| $H, $G |- $E, P, Q;  $H, Q, P, $G |- $E |] ==>
       
   199             $H, P<->Q, $G |- $E
       
   200 
       
   201 \idx{allL_thin}   $H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E
       
   202 \idx{exR_thin}    $H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F
       
   203 \end{ttbox}
       
   204 
       
   205 \caption{Derived rules for {\tt LK}} \label{lk-derived}
       
   206 \end{figure}
       
   207 
       
   208 
       
   209 \section{Syntax and rules of inference}
       
   210 Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated
       
   211 by the representation of sequents.  Type $sobj\To sobj$ represents a list
       
   212 of formulae.
       
   213 
       
   214 The {\bf definite description} operator~$\iota x.P(x)$ stands for the
       
   215 unique~$a$ satisfying~$P(a)$, if such exists.  Since all terms in \LK{}
       
   216 denote something, a description is always meaningful, but we do not know
       
   217 its value unless $P[x]$ defines it uniquely.  The Isabelle notation is
       
   218 \hbox{\tt THE $x$.$P[x]$}.
       
   219 
       
   220 Traditionally, \(\Gamma\) and \(\Delta\) are meta-variables for sequences.
       
   221 In Isabelle's notation, the prefix~\verb|$| on a variable makes it range
       
   222 over sequences.  In a sequent, anything not prefixed by \verb|$| is taken
       
   223 as a formula.
       
   224 
       
   225 The theory has the \ML\ identifier \ttindexbold{LK.thy}.
       
   226 Figure~\ref{lk-rules} presents the rules.  The connective $\bimp$ is
       
   227 defined using $\conj$ and $\imp$.  The axiom for basic sequents is
       
   228 expressed in a form that provides automatic thinning: redundant formulae
       
   229 are simply ignored.  The other rules are expressed in the form most
       
   230 suitable for backward proof --- they do not require exchange or contraction
       
   231 rules.  The contraction rules are actually derivable (via cut) in this
       
   232 formulation.
       
   233 
       
   234 Figure~\ref{lk-derived} presents derived rules, including rules for
       
   235 $\bimp$.  The weakened quantifier rules discard each quantification after a
       
   236 single use; in an automatic proof procedure, they guarantee termination,
       
   237 but are incomplete.  Multiple use of a quantifier can be obtained by a
       
   238 contraction rule, which in backward proof duplicates a formula.  The tactic
       
   239 \ttindex{res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
       
   240 specifying the formula to duplicate.
       
   241 
       
   242 See the files \ttindexbold{LK/lk.thy} and \ttindexbold{LK/lk.ML}
       
   243 for complete listings of the rules and derived rules.
       
   244 
       
   245 
       
   246 \section{Tactics for the cut rule}
       
   247 According to the cut-elimination theorem, the cut rule can be eliminated
       
   248 from proofs of sequents.  But the rule is still essential.  It can be used
       
   249 to structure a proof into lemmas, avoiding repeated proofs of the same
       
   250 formula.  More importantly, the cut rule can not be eliminated from
       
   251 derivations of rules.  For example, there is a trivial cut-free proof of
       
   252 the sequent \(P\conj Q\turn Q\conj P\).
       
   253 Noting this, we might want to derive a rule for swapping the conjuncts
       
   254 in a right-hand formula:
       
   255 \[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]
       
   256 The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj
       
   257 P$.  Most cuts directly involve a premise of the rule being derived (a
       
   258 meta-assumption).  In a few cases, the cut formula is not part of any
       
   259 premise, but serves as a bridge between the premises and the conclusion.
       
   260 In such proofs, the cut formula is specified by calling an appropriate
       
   261 tactic.
       
   262 
       
   263 \begin{ttbox} 
       
   264 cutR_tac : string -> int -> tactic
       
   265 cutL_tac : string -> int -> tactic
       
   266 \end{ttbox}
       
   267 These tactics refine a subgoal into two by applying the cut rule.  The cut
       
   268 formula is given as a string, and replaces some other formula in the sequent.
       
   269 \begin{description}
       
   270 \item[\ttindexbold{cutR_tac} {\it formula} {\it i}] 
       
   271 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
       
   272 then deletes some formula from the right side of subgoal~$i$, replacing
       
   273 that formula by~$P$.
       
   274 
       
   275 \item[\ttindexbold{cutL_tac} {\it formula} {\it i}] 
       
   276 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
       
   277 then deletes some formula from the let side of the new subgoal $i+1$,
       
   278 replacing that formula by~$P$.
       
   279 \end{description}
       
   280 All the structural rules --- cut, contraction, and thinning --- can be
       
   281 applied to particular formulae using \ttindex{res_inst_tac}.
       
   282 
       
   283 
       
   284 \section{Tactics for sequents}
       
   285 \begin{ttbox} 
       
   286 forms_of_seq       : term -> term list
       
   287 could_res          : term * term -> bool
       
   288 could_resolve_seq  : term * term -> bool
       
   289 filseq_resolve_tac : thm list -> int -> int -> tactic
       
   290 \end{ttbox}
       
   291 Associative unification is not as efficient as it might be, in part because
       
   292 the representation of lists defeats some of Isabelle's internal
       
   293 optimizations.  The following operations implement faster rule application,
       
   294 and may have other uses.
       
   295 \begin{description}
       
   296 \item[\ttindexbold{forms_of_seq} {\it t}] 
       
   297 returns the list of all formulae in the sequent~$t$, removing sequence
       
   298 variables.
       
   299 
       
   300 \item[\ttindexbold{could_res} $(t,u)$] 
       
   301 tests whether two formula lists could be resolved.  List $t$ is from a
       
   302 premise (subgoal), while $u$ is from the conclusion of an object-rule.
       
   303 Assuming that each formula in $u$ is surrounded by sequence variables, it
       
   304 checks that each conclusion formula is unifiable (using {\tt could_unify})
       
   305 with some subgoal formula.
       
   306 
       
   307 \item[\ttindexbold{could_resolve} $(t,u)$] 
       
   308 tests whether two sequents could be resolved.  Sequent $t$ is a premise
       
   309 (subgoal), while $u$ is the conclusion of an object-rule.  It uses {\tt
       
   310 could_res} to check the left and right sides of the two sequents.
       
   311 
       
   312 \item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}] 
       
   313 uses {\tt filter_thms could_resolve} to extract the {\it thms} that are
       
   314 applicable to subgoal~$i$.  If more than {\it maxr\/} theorems are
       
   315 applicable then the tactic fails.  Otherwise it calls {\tt resolve_tac}.
       
   316 Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.
       
   317 \end{description}
       
   318 
       
   319 
       
   320 
       
   321 \section{Packaging sequent rules}
       
   322 For theorem proving, rules can be classified as {\bf safe} or {\bf
       
   323 unsafe}.  An unsafe rule (typically a weakened quantifier rule) may reduce
       
   324 a provable goal to an unprovable set of subgoals, and should only be used
       
   325 as a last resort.  
       
   326 
       
   327 A {\bf pack} is a pair whose first component is a list of safe
       
   328 rules, and whose second is a list of unsafe rules.  Packs can be extended
       
   329 in an obvious way to allow reasoning with various collections of rules.
       
   330 For clarity, \LK{} declares the datatype
       
   331 \ttindexbold{pack}:
       
   332 \begin{ttbox}
       
   333 datatype pack = Pack of thm list * thm list;
       
   334 \end{ttbox}
       
   335 The contents of any pack can be inspected by pattern-matching.  Packs
       
   336 support the following operations:
       
   337 \begin{ttbox} 
       
   338 empty_pack  : pack
       
   339 prop_pack   : pack
       
   340 LK_pack     : pack
       
   341 LK_dup_pack : pack
       
   342 add_safes   : pack * thm list -> pack               \hfill{\bf infix 4}
       
   343 add_unsafes : pack * thm list -> pack               \hfill{\bf infix 4}
       
   344 \end{ttbox}
       
   345 \begin{description}
       
   346 \item[\ttindexbold{empty_pack}] is the empty pack.
       
   347 
       
   348 \item[\ttindexbold{prop_pack}] contains the propositional rules, namely
       
   349 those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the
       
   350 rules \ttindex{basic} and \ttindex{refl}.  These are all safe.
       
   351 
       
   352 \item[\ttindexbold{LK_pack}] 
       
   353 extends {\tt prop_pack} with the safe rules \ttindex{allR}
       
   354 and~\ttindex{exL} and the unsafe rules \ttindex{allL_thin} and
       
   355 \ttindex{exR_thin}.  Search using this is incomplete since quantified
       
   356 formulae are used at most once.
       
   357 
       
   358 \item[\ttindexbold{LK_dup_pack}] 
       
   359 extends {\tt prop_pack} with the safe rules \ttindex{allR}
       
   360 and~\ttindex{exL} and the unsafe rules \ttindex{allL} and~\ttindex{exR}.
       
   361 Search using this is complete, since quantified formulae may be reused, but
       
   362 frequently fails to terminate.  It is generally unsuitable for depth-first
       
   363 search.
       
   364 
       
   365 \item[$pack$ \ttindexbold{add_safes} $rules$] 
       
   366 adds some safe~$rules$ to the pack~$pack$.
       
   367 
       
   368 \item[$pack$ \ttindexbold{add_unsafes} $rules$] 
       
   369 adds some unsafe~$rules$ to the pack~$pack$.
       
   370 \end{description}
       
   371 
       
   372 
       
   373 \section{Proof procedures}
       
   374 The \LK{} proof procedure is similar to the generic classical module
       
   375 described in the {\em Reference Manual}.  In fact it is simpler, since it
       
   376 works directly with sequents rather than simulating them.  There is no need
       
   377 to distinguish introduction rules from elimination rules, and of course
       
   378 there is no swap rule.  As always, Isabelle's classical proof procedures
       
   379 are less powerful than resolution theorem provers.  But they are more
       
   380 natural and flexible, working with an open-ended set of rules.
       
   381 
       
   382 Backtracking over the choice of a safe rule accomplishes nothing: applying
       
   383 them in any order leads to essentially the same result.  Backtracking may
       
   384 be necessary over basic sequents when they perform unification.  Suppose
       
   385 that~0, 1, 2,~3 are constants in the subgoals
       
   386 \[  \begin{array}{c}
       
   387       P(0), P(1), P(2) \turn P(\Var{a})  \\
       
   388       P(0), P(2), P(3) \turn P(\Var{a})  \\
       
   389       P(1), P(3), P(2) \turn P(\Var{a})  
       
   390     \end{array}
       
   391 \]
       
   392 The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,
       
   393 and this can only be discovered by search.  The tactics given below permit
       
   394 backtracking only over axioms, such as {\tt basic} and {\tt refl}.
       
   395 
       
   396 
       
   397 \subsection{Method A}
       
   398 \begin{ttbox} 
       
   399 reresolve_tac   : thm list -> int -> tactic
       
   400 repeat_goal_tac : pack -> int -> tactic
       
   401 pc_tac          : pack -> int -> tactic
       
   402 \end{ttbox}
       
   403 These tactics use a method developed by Philippe de Groote.  A subgoal is
       
   404 refined and the resulting subgoals are attempted in reverse order.  For
       
   405 some reason, this is much faster than attempting the subgoals in order.
       
   406 The method is inherently depth-first.
       
   407 
       
   408 At present, these tactics only work for rules that have no more than two
       
   409 premises.  They {\bf fail} if they can do nothing.
       
   410 \begin{description}
       
   411 \item[\ttindexbold{reresolve_tac} $thms$ $i$] 
       
   412 repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.
       
   413 
       
   414 \item[\ttindexbold{repeat_goal_tac} $pack$ $i$] 
       
   415 applies the safe rules in the pack to a goal and the resulting subgoals.
       
   416 If no safe rule is applicable then it applies an unsafe rule and continues.
       
   417 
       
   418 \item[\ttindexbold{pc_tac} $pack$ $i$] 
       
   419 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
       
   420 \end{description}
       
   421 
       
   422 
       
   423 \subsection{Method B}
       
   424 \begin{ttbox} 
       
   425 safe_goal_tac : pack -> int -> tactic
       
   426 step_tac      : pack -> int -> tactic
       
   427 fast_tac      : pack -> int -> tactic
       
   428 best_tac      : pack -> int -> tactic
       
   429 \end{ttbox}
       
   430 These tactics are precisely analogous to those of the generic classical
       
   431 module.  They use `Method~A' only on safe rules.  They {\bf fail} if they
       
   432 can do nothing.
       
   433 \begin{description}
       
   434 \item[\ttindexbold{safe_goal_tac} $pack$ $i$] 
       
   435 applies the safe rules in the pack to a goal and the resulting subgoals.
       
   436 It ignores the unsafe rules.  
       
   437 
       
   438 \item[\ttindexbold{step_tac} $pack$ $i$] 
       
   439 either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe
       
   440 rule.
       
   441 
       
   442 \item[\ttindexbold{fast_tac} $pack$ $i$] 
       
   443 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
       
   444 Despite the names, {\tt pc_tac} is frequently faster.
       
   445 
       
   446 \item[\ttindexbold{best_tac} $pack$ $i$] 
       
   447 applies {\tt step_tac} using best-first search to solve subgoal~$i$.  It is
       
   448 particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).
       
   449 \end{description}
       
   450 
       
   451 
       
   452 
       
   453 \section{A simple example of classical reasoning} 
       
   454 The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
       
   455 classical treatment of the existential quantifier.  Classical reasoning
       
   456 is easy using~{\LK}, as you can see by comparing this proof with the one
       
   457 given in~\S\ref{fol-cla-example}.  From a logical point of view, the
       
   458 proofs are essentially the same; the key step here is to use \ttindex{exR}
       
   459 rather than the weaker~\ttindex{exR_thin}.
       
   460 \begin{ttbox}
       
   461 goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
       
   462 {\out Level 0}
       
   463 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   464 {\out  1.  |- EX y. ALL x. P(y) --> P(x)}
       
   465 by (resolve_tac [exR] 1);
       
   466 {\out Level 1}
       
   467 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   468 {\out  1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
       
   469 \end{ttbox}
       
   470 There are now two formulae on the right side.  Keeping the existential one
       
   471 in reserve, we break down the universal one.
       
   472 \begin{ttbox}
       
   473 by (resolve_tac [allR] 1);
       
   474 {\out Level 2}
       
   475 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   476 {\out  1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
       
   477 by (resolve_tac [impR] 1);
       
   478 {\out Level 3}
       
   479 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   480 {\out  1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
       
   481 \end{ttbox}
       
   482 Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
       
   483 become an assumption;  instead, it moves to the left side.  The
       
   484 resulting subgoal cannot be instantiated to a basic sequent: the bound
       
   485 variable~$x$ is not unifiable with the unknown~$\Var{x}$.
       
   486 \begin{ttbox}
       
   487 by (resolve_tac [basic] 1);
       
   488 {\out by: tactic failed}
       
   489 \end{ttbox}
       
   490 We reuse the existential formula using~\ttindex{exR_thin}, which discards
       
   491 it; we will not need it a third time.  We again break down the resulting
       
   492 formula.
       
   493 \begin{ttbox}
       
   494 by (resolve_tac [exR_thin] 1);
       
   495 {\out Level 4}
       
   496 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   497 {\out  1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}
       
   498 by (resolve_tac [allR] 1);
       
   499 {\out Level 5}
       
   500 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   501 {\out  1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}
       
   502 by (resolve_tac [impR] 1);
       
   503 {\out Level 6}
       
   504 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   505 {\out  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
       
   506 \end{ttbox}
       
   507 Subgoal~1 seems to offer lots of possibilities.  Actually the only useful
       
   508 step is instantiating~$\Var{x@7}$ to $\lambda x.x$,
       
   509 transforming~$\Var{x@7}(x)$ into~$x$.
       
   510 \begin{ttbox}
       
   511 by (resolve_tac [basic] 1);
       
   512 {\out Level 7}
       
   513 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   514 {\out No subgoals!}
       
   515 \end{ttbox}
       
   516 This theorem can be proved automatically.  Because it involves quantifier
       
   517 duplication, we employ best-first search:
       
   518 \begin{ttbox}
       
   519 goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
       
   520 {\out Level 0}
       
   521 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   522 {\out  1.  |- EX y. ALL x. P(y) --> P(x)}
       
   523 by (best_tac LK_dup_pack 1);
       
   524 {\out Level 1}
       
   525 {\out  |- EX y. ALL x. P(y) --> P(x)}
       
   526 {\out No subgoals!}
       
   527 \end{ttbox}
       
   528 
       
   529 
       
   530 
       
   531 \section{A more complex proof}
       
   532 Many of Pelletier's test problems for theorem provers \cite{pelletier86}
       
   533 can be solved automatically.  Problem~39 concerns set theory, asserting
       
   534 that there is no Russell set --- a set consisting of those sets that are
       
   535 not members of themselves:
       
   536 \[  \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]
       
   537 This does not require special properties of membership; we may
       
   538 generalize $x\in y$ to an arbitrary predicate~$F(x,y)$.  The theorem has a
       
   539 short manual proof.  See the directory \ttindexbold{LK/ex} for many more
       
   540 examples.
       
   541 
       
   542 We set the main goal and move the negated formula to the left.
       
   543 \begin{ttbox}
       
   544 goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
       
   545 {\out Level 0}
       
   546 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   547 {\out  1.  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   548 by (resolve_tac [notR] 1);
       
   549 {\out Level 1}
       
   550 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   551 {\out  1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}
       
   552 by (resolve_tac [exL] 1);
       
   553 \end{ttbox}
       
   554 The right side is empty; we strip both quantifiers from the formula on the
       
   555 left.
       
   556 \begin{ttbox}
       
   557 {\out Level 2}
       
   558 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   559 {\out  1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}
       
   560 by (resolve_tac [allL_thin] 1);
       
   561 {\out Level 3}
       
   562 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   563 {\out  1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}
       
   564 \end{ttbox}
       
   565 The rule \ttindex{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either
       
   566 both true or both false.  It yields two subgoals.
       
   567 \begin{ttbox}
       
   568 by (resolve_tac [iffL] 1);
       
   569 {\out Level 4}
       
   570 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   571 {\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
       
   572 {\out  2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}
       
   573 \end{ttbox}
       
   574 We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both
       
   575 subgoals.  Beginning with subgoal~2, we move a negated formula to the left
       
   576 and create a basic sequent.
       
   577 \begin{ttbox}
       
   578 by (resolve_tac [notL] 2);
       
   579 {\out Level 5}
       
   580 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   581 {\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
       
   582 {\out  2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}
       
   583 by (resolve_tac [basic] 2);
       
   584 {\out Level 6}
       
   585 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   586 {\out  1. !!x.  |- F(x,x), ~ F(x,x)}
       
   587 \end{ttbox}
       
   588 Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
       
   589 \begin{ttbox}
       
   590 by (resolve_tac [notR] 1);
       
   591 {\out Level 7}
       
   592 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   593 {\out  1. !!x. F(x,x) |- F(x,x)}
       
   594 by (resolve_tac [basic] 1);
       
   595 {\out Level 8}
       
   596 {\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
       
   597 {\out No subgoals!}
       
   598 \end{ttbox}