summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Mon, 04 Apr 1994 17:20:15 +0200 | |

changeset 308 | f4cecad9b6a0 |

parent 307 | 994dbab40849 |

child 309 | 3751567696bf |

modifications towards final draft

--- a/doc-src/Ref/classical.tex Mon Apr 04 17:09:45 1994 +0200 +++ b/doc-src/Ref/classical.tex Mon Apr 04 17:20:15 1994 +0200 @@ -1,12 +1,13 @@ %% $Id$ \chapter{The Classical Reasoner} \index{classical reasoner|(} -\newcommand\ainfer[2]{\begin{array}{r@{}l}#2\\ \hline#1\end{array}} +\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} + Although Isabelle is generic, many users will be working in some extension -of classical first-order logic (FOL). Isabelle's set theory is built upon -FOL, while higher-order logic contains FOL as a fragment. Theorem-proving -in FOL is of course undecidable, but many researchers have developed -strategies to assist in this task. +of classical first-order logic. Isabelle's set theory~{\tt ZF} is built +upon theory~{\tt FOL}, while higher-order logic contains first-order logic +as a fragment. Theorem-proving in predicate logic is undecidable, but many +researchers have developed strategies to assist in this task. Isabelle's classical reasoner is an \ML{} functor that accepts certain information about a logic and delivers a suite of automatic tactics. Each @@ -20,15 +21,16 @@ \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x)) \imp \neg (\exists z. \forall x. F(x,z)) \] -The tactics are generic. They are not restricted to~FOL, and have been -heavily used in the development of Isabelle's set theory. Few interactive -proof assistants provide this much automation. Isabelle does not record -proofs, but the tactics can be traced, and their components can be called -directly. In this manner, any proof can be viewed interactively. +% +The tactics are generic. They are not restricted to first-order logic, and +have been heavily used in the development of Isabelle's set theory. Few +interactive proof assistants provide this much automation. The tactics can +be traced, and their components can be called directly; in this manner, +any proof can be viewed interactively. -The logics FOL, HOL and ZF have the classical reasoner already installed. We -shall first consider how to use it, then see how to instantiate it for new -logics. +The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner +already installed. We shall first consider how to use it, then see how to +instantiate it for new logics. \section{The sequent calculus} @@ -40,8 +42,9 @@ generalization of natural deduction, is easier to automate. A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$ -and~$\Delta$ are sets of formulae.\footnote{For FOL, sequents can -equivalently be made from lists or multisets of formulae.} The sequent +and~$\Delta$ are sets of formulae.% +\footnote{For first-order logic, sequents can equivalently be made from + lists or multisets of formulae.} The sequent \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \] is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true, @@ -52,8 +55,12 @@ Sequent rules are classified as {\bf right} or {\bf left}, indicating which side of the $\turn$~symbol they operate on. Rules that operate on the right side are analogous to natural deduction's introduction rules, and -left rules are analogous to elimination rules. The sequent calculus -analogue of~$({\imp}I)$ is the rule +left rules are analogous to elimination rules. +Recall the natural deduction rules for + first-order logic, +\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}% + {Fig.\ts\ref{fol-fig}}. +The sequent calculus analogue of~$({\imp}I)$ is the rule $$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q} \eqno({\imp}R) $$ This breaks down some implication on the right side of a sequent; $\Gamma$ @@ -82,7 +89,7 @@ \section{Simulating sequents by natural deduction} -Isabelle can represent sequents directly, as in the object-logic~{\sc lk}. +Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@. But natural deduction is easier to work with, and most object-logics employ it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn Q@1,\ldots,Q@n$ by the Isabelle formula @@ -91,16 +98,17 @@ Elim-resolution plays a key role in simulating sequent proofs. We can easily handle reasoning on the left. -As discussed in the {\em Introduction to Isabelle}, +As discussed in +\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$ achieves a similar effect as the corresponding sequent rules. For the other connectives, we use sequent-style elimination rules instead of -destruction rules. But note that the rule $(\neg L)$ has no effect -under our representation of sequents! +destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that +the rule $(\neg L)$ has no effect under our representation of sequents! $$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P} \eqno({\neg}L) $$ What about reasoning on the right? Introduction rules can only affect the -formula in the conclusion, namely~$Q@1$. The other right-side formula are +formula in the conclusion, namely~$Q@1$. The other right-side formulae are represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. In order to operate on one of these, it must first be exchanged with~$Q@1$. Elim-resolution with the {\bf swap} rule has this effect: @@ -129,8 +137,8 @@ The destruction rule $({\imp}E)$ is replaced by \[ \List{P\imp Q;\; \neg P\imp R;\; Q\imp R} \Imp R. \] Quantifier replication also requires special rules. In classical logic, -$\exists x{.}P$ is equivalent to $\forall x{.}P$, and the rules $(\exists R)$ -and $(\forall L)$ are dual: +$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules +$(\exists R)$ and $(\forall L)$ are dual: \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P} {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R) \qquad @@ -139,9 +147,9 @@ \] Thus both kinds of quantifier may be replicated. Theorems requiring multiple uses of a universal formula are easy to invent; consider -$(\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(x))$, for any~$n>1$. -Natural examples of the multiple use of an existential formula are rare; a -standard one is $\exists x.\forall y. P(x)\imp P(y)$. +\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \] +for any~$n>1$. Natural examples of the multiple use of an existential +formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$. Forgoing quantifier replication loses completeness, but gains decidability, since the search space becomes finite. Many useful theorems can be proved @@ -169,22 +177,21 @@ \section{Classical rule sets} \index{classical sets|bold} -Each automatic tactic takes a {\bf classical rule set} -- a collection of +Each automatic tactic takes a {\bf classical rule set} --- a collection of rules, classified as introduction or elimination and as {\bf safe} or {\bf unsafe}. In general, safe rules can be attempted blindly, while unsafe rules must be used with care. A safe rule must never reduce a provable -goal to an unprovable set of subgoals. The rule~$({\disj}I1)$ is obviously -unsafe, since it reduces $P\disj Q$ to~$P$; fortunately, we do not require -this rule. +goal to an unprovable set of subgoals. -In general, any rule is unsafe whose premises contain new unknowns. The -elimination rule~$(\forall E@2)$ is unsafe, since it is applied via -elim-resolution, which discards the assumption $\forall x{.}P(x)$ and -replaces it by the weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ -is unsafe for similar reasons. The rule~$(\forall E@3)$ is unsafe in a -different sense: since it keeps the assumption $\forall x{.}P(x)$, it is -prone to looping. In classical first-order logic, all rules are safe -except those mentioned above. +The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any +rule is unsafe whose premises contain new unknowns. The elimination +rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution, +which discards the assumption $\forall x{.}P(x)$ and replaces it by the +weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for +similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense: +since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping. +In classical first-order logic, all rules are safe except those mentioned +above. The safe/unsafe distinction is vague, and may be regarded merely as a way of giving some rules priority over others. One could argue that @@ -211,29 +218,30 @@ \end{ttbox} There are no operations for deletion from a classical set. The add operations do not check for repetitions. -\begin{description} +\begin{ttdescription} \item[\ttindexbold{empty_cs}] is the empty classical set. -\item[\tt $cs$ addSIs $rules$] \indexbold{*addSIs} -adds some safe introduction~$rules$ to the classical set~$cs$. +\item[$cs$ addSIs $rules$] \indexbold{*addSIs} +adds safe introduction~$rules$ to~$cs$. -\item[\tt $cs$ addSEs $rules$] \indexbold{*addSEs} -adds some safe elimination~$rules$ to the classical set~$cs$. +\item[$cs$ addSEs $rules$] \indexbold{*addSEs} +adds safe elimination~$rules$ to~$cs$. -\item[\tt $cs$ addSDs $rules$] \indexbold{*addSDs} -adds some safe destruction~$rules$ to the classical set~$cs$. +\item[$cs$ addSDs $rules$] \indexbold{*addSDs} +adds safe destruction~$rules$ to~$cs$. -\item[\tt $cs$ addIs $rules$] \indexbold{*addIs} -adds some unsafe introduction~$rules$ to the classical set~$cs$. +\item[$cs$ addIs $rules$] \indexbold{*addIs} +adds unsafe introduction~$rules$ to~$cs$. -\item[\tt $cs$ addEs $rules$] \indexbold{*addEs} -adds some unsafe elimination~$rules$ to the classical set~$cs$. +\item[$cs$ addEs $rules$] \indexbold{*addEs} +adds unsafe elimination~$rules$ to~$cs$. -\item[\tt $cs$ addDs $rules$] \indexbold{*addDs} -adds some unsafe destruction~$rules$ to the classical set~$cs$. +\item[$cs$ addDs $rules$] \indexbold{*addDs} +adds unsafe destruction~$rules$ to~$cs$. -\item[\ttindexbold{print_cs} $cs$] prints the rules of the classical set~$cs$. -\end{description} +\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$. +\end{ttdescription} + Introduction rules are those that can be applied using ordinary resolution. The classical set automatically generates their swapped forms, which will be applied using elim-resolution. Elimination rules are applied using @@ -265,7 +273,7 @@ \end{ttbox} The automatic proof procedures call these tactics. By calling them yourself, you can execute these procedures one step at a time. -\begin{description} +\begin{ttdescription} \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on subgoal~$i$. This may include proof by assumption or Modus Ponens, taking care not to instantiate unknowns, or \ttindex{hyp_subst_tac}. @@ -288,7 +296,7 @@ The resulting search space is too large for use in the standard proof procedures, but {\tt slow_step_tac} is worth considering in special situations. -\end{description} +\end{ttdescription} \subsection{The automatic tactics} @@ -299,7 +307,7 @@ Both of these tactics work by applying {\tt step_tac} repeatedly. Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either solve this subgoal or fail. -\begin{description} +\begin{ttdescription} \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using depth-first search, to solve subgoal~$i$. @@ -307,7 +315,7 @@ best-first search, to solve subgoal~$i$. A heuristic function --- typically, the total size of the proof state --- guides the search. This function is supplied when the classical reasoner is set up. -\end{description} +\end{ttdescription} \subsection{Other useful tactics} @@ -320,7 +328,7 @@ swap_res_tac : thm list -> int -> tactic \end{ttbox} These can be used in the body of a specialized search. -\begin{description} +\begin{ttdescription} \item[\ttindexbold{contr_tac} {\it i}] solves subgoal~$i$ by detecting a contradiction among two assumptions of the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The tactic can produce multiple outcomes, @@ -341,23 +349,23 @@ rules. First, it attempts to solve the goal using \ttindex{assume_tac} or {\tt contr_tac}. It then attempts to apply each rule in turn, attempting resolution and also elim-resolution with the swapped form. -\end{description} +\end{ttdescription} \subsection{Creating swapped rules} \begin{ttbox} swapify : thm list -> thm list joinrules : thm list * thm list -> (bool * thm) list \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the swapped versions of~{\it thms}, regarded as introduction rules. -\item[\ttindexbold{joinrules} \tt({\it intrs}, {\it elims})] +\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})] joins introduction rules, their swapped versions, and elimination rules for use with \ttindex{biresolve_tac}. Each rule is paired with~{\tt false} (indicating ordinary resolution) or~{\tt true} (indicating elim-resolution). -\end{description} +\end{ttdescription} \section{Setting up the classical reasoner} @@ -378,7 +386,7 @@ end; \end{ttbox} Thus, the functor requires the following items: -\begin{description} +\begin{ttdescription} \item[\ttindexbold{mp}] should be the Modus Ponens rule $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. @@ -399,7 +407,7 @@ the hypotheses, typically created by \ttindex{HypsubstFun} (see Chapter~\ref{substitution}). This list can, of course, be empty. The tactics are assumed to be safe! -\end{description} +\end{ttdescription} The functor is not at all sensitive to the formalization of the object-logic. It does not even examine the rules, but merely applies them according to its fixed strategy. The functor resides in {\tt