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

author | lcp |

Fri, 15 Apr 1994 16:29:48 +0200 | |

changeset 319 | f143f7686cd6 |

parent 318 | a0e27395abe3 |

child 320 | 76ae17549558 |

penultimate Springer draft

--- a/doc-src/Ref/classical.tex Fri Apr 15 16:08:31 1994 +0200 +++ b/doc-src/Ref/classical.tex Fri Apr 15 16:29:48 1994 +0200 @@ -1,5 +1,5 @@ %% $Id$ -\chapter{The Classical Reasoner} +\chapter{The Classical Reasoner}\label{chap:classical} \index{classical reasoner|(} \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} @@ -109,8 +109,9 @@ \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 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$. +represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. +\index{assumptions!negated} +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: $$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$ To ensure that swaps occur only when necessary, each introduction rule is @@ -176,8 +177,8 @@ \section{Classical rule sets} -\index{classical sets|bold} -Each automatic tactic takes a {\bf classical rule set} --- a collection of +\index{classical sets} +Each automatic tactic takes a {\bf classical 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 @@ -203,7 +204,7 @@ is unsafe if it instantiates unknowns shared with other subgoals --- thus \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}. -Classical rule sets belong to the abstract type \ttindexbold{claset}, which +Classical rule sets belong to the abstract type \mltydx{claset}, which supports the following operations (provided the classical reasoner is installed!): \begin{ttbox} @@ -252,14 +253,13 @@ For a given classical set, the proof strategy is simple. Perform as many safe inferences as possible; or else, apply certain safe rules, allowing instantiation of unknowns; or else, apply an unsafe rule. The tactics may -also apply \ttindex{hyp_subst_tac}, if they have been set up to do so (see +also apply {\tt hyp_subst_tac}, if they have been set up to do so (see below). They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$. \section{The classical tactics} -\index{classical prover!tactics|bold} -\index{tactics!for classical proof|bold} +\index{classical reasoner!tactics} If installed, the classical module provides several tactics (and other operations) for simulating the classical sequent calculus. @@ -275,8 +275,8 @@ yourself, you can execute these procedures one step at a time. \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}. +subgoal~$i$. This may include proof by assumption or Modus Ponens (taking +care not to instantiate unknowns), or {\tt hyp_subst_tac}. \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all subgoals. It is deterministic, with at most one outcome. If the automatic @@ -319,8 +319,8 @@ \subsection{Other useful tactics} -\index{tactics!for contradiction|bold} -\index{tactics!for Modus Ponens|bold} +\index{tactics!for contradiction} +\index{tactics!for Modus Ponens} \begin{ttbox} contr_tac : int -> tactic mp_tac : int -> tactic @@ -329,10 +329,11 @@ \end{ttbox} These can be used in the body of a specialized search. \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, -enumerating all possible contradictions. +\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory} + 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, enumerating all possible + contradictions. \item[\ttindexbold{mp_tac} {\it i}] is like {\tt contr_tac}, but also attempts to perform Modus Ponens in @@ -346,7 +347,7 @@ \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of the proof state using {\it thms}, which should be a list of introduction -rules. First, it attempts to solve the goal using \ttindex{assume_tac} or +rules. First, it attempts to solve the goal using {\tt 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{ttdescription} @@ -369,12 +370,12 @@ \section{Setting up the classical reasoner} -\index{classical reasoner!setting up|bold} +\index{classical reasoner!setting up} Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have the classical reasoner already set up. When defining a new classical logic, you should set up the reasoner yourself. It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the argument -signature\indexbold{*CLASSICAL_DATA} +signature {\tt CLASSICAL_DATA}: \begin{ttbox} signature CLASSICAL_DATA = sig @@ -387,13 +388,13 @@ \end{ttbox} Thus, the functor requires the following items: \begin{ttdescription} -\item[\ttindexbold{mp}] should be the Modus Ponens rule +\item[\tdxbold{mp}] should be the Modus Ponens rule $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. -\item[\ttindexbold{not_elim}] should be the contradiction rule +\item[\tdxbold{not_elim}] should be the contradiction rule $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$. -\item[\ttindexbold{swap}] should be the swap rule +\item[\tdxbold{swap}] should be the swap rule $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. \item[\ttindexbold{sizef}] is the heuristic function used for best-first @@ -403,7 +404,7 @@ those concerned with type checking). A heuristic function might simply count the subgoals. -\item[\ttindexbold{hyp_subst_tac}] is a list of tactics for substitution in +\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in 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! @@ -411,6 +412,6 @@ 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 -Provers/classical.ML} on the Isabelle distribution directory. +Provers/classical.ML} in the Isabelle distribution directory. -\index{classical prover|)} +\index{classical reasoner|)}