2 \chapter{The Classical Reasoner}
3 \index{classical reasoner|(}
4 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
6 Although Isabelle is generic, many users will be working in some extension
7 of classical first-order logic. Isabelle's set theory~{\tt ZF} is built
8 upon theory~{\tt FOL}, while higher-order logic contains first-order logic
9 as a fragment. Theorem-proving in predicate logic is undecidable, but many
10 researchers have developed strategies to assist in this task.
12 Isabelle's classical reasoner is an \ML{} functor that accepts certain
13 information about a logic and delivers a suite of automatic tactics. Each
14 tactic takes a collection of rules and executes a simple, non-clausal proof
15 procedure. They are slow and simplistic compared with resolution theorem
16 provers, but they can save considerable time and effort. They can prove
17 theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
19 \[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))
20 \imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
21 \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
22 \imp \neg (\exists z. \forall x. F(x,z))
25 The tactics are generic. They are not restricted to first-order logic, and
26 have been heavily used in the development of Isabelle's set theory. Few
27 interactive proof assistants provide this much automation. The tactics can
28 be traced, and their components can be called directly; in this manner,
29 any proof can be viewed interactively.
31 The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner
32 already installed. We shall first consider how to use it, then see how to
33 instantiate it for new logics.
36 \section{The sequent calculus}
37 \index{sequent calculus}
38 Isabelle supports natural deduction, which is easy to use for interactive
39 proof. But natural deduction does not easily lend itself to automation,
40 and has a bias towards intuitionism. For certain proofs in classical
41 logic, it can not be called natural. The {\bf sequent calculus}, a
42 generalization of natural deduction, is easier to automate.
44 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
45 and~$\Delta$ are sets of formulae.%
46 \footnote{For first-order logic, sequents can equivalently be made from
47 lists or multisets of formulae.} The sequent
48 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
49 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
50 Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
51 while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf
52 basic} if its left and right sides have a common formula, as in $P,Q\turn
53 Q,R$; basic sequents are trivially valid.
55 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
56 side of the $\turn$~symbol they operate on. Rules that operate on the
57 right side are analogous to natural deduction's introduction rules, and
58 left rules are analogous to elimination rules.
59 Recall the natural deduction rules for
61 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
62 {Fig.\ts\ref{fol-fig}}.
63 The sequent calculus analogue of~$({\imp}I)$ is the rule
64 $$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
66 This breaks down some implication on the right side of a sequent; $\Gamma$
67 and $\Delta$ stand for the sets of formulae that are unaffected by the
68 inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
70 $$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
72 This breaks down some disjunction on the right side, replacing it by both
73 disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
75 To illustrate the use of multiple formulae on the right, let us prove
76 the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we
77 reduce this formula to a basic sequent:
78 \[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
79 {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
80 {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
81 {P, Q \turn Q, P\qquad\qquad}}}
83 This example is typical of the sequent calculus: start with the desired
84 theorem and apply rules backwards in a fairly arbitrary manner. This yields a
85 surprisingly effective proof procedure. Quantifiers add few complications,
86 since Isabelle handles parameters and schematic variables. See Chapter~10
87 of {\em ML for the Working Programmer}~\cite{paulson91} for further
91 \section{Simulating sequents by natural deduction}
92 Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.
93 But natural deduction is easier to work with, and most object-logics employ
94 it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
95 Q@1,\ldots,Q@n$ by the Isabelle formula
96 \[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
97 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
98 Elim-resolution plays a key role in simulating sequent proofs.
100 We can easily handle reasoning on the left.
102 \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
103 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
104 achieves a similar effect as the corresponding sequent rules. For the
105 other connectives, we use sequent-style elimination rules instead of
106 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
107 the rule $(\neg L)$ has no effect under our representation of sequents!
108 $$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
110 What about reasoning on the right? Introduction rules can only affect the
111 formula in the conclusion, namely~$Q@1$. The other right-side formulae are
112 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. In
113 order to operate on one of these, it must first be exchanged with~$Q@1$.
114 Elim-resolution with the {\bf swap} rule has this effect:
115 $$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$
116 To ensure that swaps occur only when necessary, each introduction rule is
117 converted into a swapped form: it is resolved with the second premise
118 of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
119 called~$({\neg\conj}E)$, is
120 \[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
121 Similarly, the swapped form of~$({\imp}I)$ is
122 \[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \]
123 Swapped introduction rules are applied using elim-resolution, which deletes
124 the negated formula. Our representation of sequents also requires the use
125 of ordinary introduction rules. If we had no regard for readability, we
126 could treat the right side more uniformly by representing sequents as
127 \[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
130 \section{Extra rules for the sequent calculus}
131 As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
132 must be replaced by sequent-style elimination rules. In addition, we need
133 rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
134 Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
135 simulates $({\disj}R)$:
136 \[ (\neg Q\Imp P) \Imp P\disj Q \]
137 The destruction rule $({\imp}E)$ is replaced by
138 \[ \List{P\imp Q;\; \neg P\imp R;\; Q\imp R} \Imp R. \]
139 Quantifier replication also requires special rules. In classical logic,
140 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
141 $(\exists R)$ and $(\forall L)$ are dual:
142 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
143 {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
145 \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
146 {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
148 Thus both kinds of quantifier may be replicated. Theorems requiring
149 multiple uses of a universal formula are easy to invent; consider
150 \[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
151 for any~$n>1$. Natural examples of the multiple use of an existential
152 formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
154 Forgoing quantifier replication loses completeness, but gains decidability,
155 since the search space becomes finite. Many useful theorems can be proved
156 without replication, and the search generally delivers its verdict in a
157 reasonable time. To adopt this approach, represent the sequent rules
158 $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
159 E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
161 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
162 Elim-resolution with this rule will delete the universal formula after a
163 single use. To replicate universal quantifiers, replace the rule by
164 $$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
165 \eqno(\forall E@3) $$
166 To replicate existential quantifiers, replace $(\exists I)$ by
167 \[ \Bigl(\neg(\exists x{.}P(x)) \Imp P(t)\Bigr) \Imp \exists x{.}P(x). \]
168 All introduction rules mentioned above are also useful in swapped form.
170 Replication makes the search space infinite; we must apply the rules with
171 care. The classical reasoner distinguishes between safe and unsafe
172 rules, applying the latter only when there is no alternative. Depth-first
173 search may well go down a blind alley; best-first search is better behaved
174 in an infinite search space. However, quantifier replication is too
175 expensive to prove any but the simplest theorems.
178 \section{Classical rule sets}
179 \index{classical sets|bold}
180 Each automatic tactic takes a {\bf classical rule set} --- a collection of
181 rules, classified as introduction or elimination and as {\bf safe} or {\bf
182 unsafe}. In general, safe rules can be attempted blindly, while unsafe
183 rules must be used with care. A safe rule must never reduce a provable
184 goal to an unprovable set of subgoals.
186 The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
187 rule is unsafe whose premises contain new unknowns. The elimination
188 rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
189 which discards the assumption $\forall x{.}P(x)$ and replaces it by the
190 weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
191 similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
192 since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
193 In classical first-order logic, all rules are safe except those mentioned
196 The safe/unsafe distinction is vague, and may be regarded merely as a way
197 of giving some rules priority over others. One could argue that
198 $({\disj}E)$ is unsafe, because repeated application of it could generate
199 exponentially many subgoals. Induction rules are unsafe because inductive
200 proofs are difficult to set up automatically. Any inference is unsafe that
201 instantiates an unknown in the proof state --- thus \ttindex{match_tac}
202 must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
203 is unsafe if it instantiates unknowns shared with other subgoals --- thus
204 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
206 Classical rule sets belong to the abstract type \ttindexbold{claset}, which
207 supports the following operations (provided the classical reasoner is
211 addSIs : claset * thm list -> claset \hfill{\bf infix 4}
212 addSEs : claset * thm list -> claset \hfill{\bf infix 4}
213 addSDs : claset * thm list -> claset \hfill{\bf infix 4}
214 addIs : claset * thm list -> claset \hfill{\bf infix 4}
215 addEs : claset * thm list -> claset \hfill{\bf infix 4}
216 addDs : claset * thm list -> claset \hfill{\bf infix 4}
217 print_cs : claset -> unit
219 There are no operations for deletion from a classical set. The add
220 operations do not check for repetitions.
221 \begin{ttdescription}
222 \item[\ttindexbold{empty_cs}] is the empty classical set.
224 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
225 adds safe introduction~$rules$ to~$cs$.
227 \item[$cs$ addSEs $rules$] \indexbold{*addSEs}
228 adds safe elimination~$rules$ to~$cs$.
230 \item[$cs$ addSDs $rules$] \indexbold{*addSDs}
231 adds safe destruction~$rules$ to~$cs$.
233 \item[$cs$ addIs $rules$] \indexbold{*addIs}
234 adds unsafe introduction~$rules$ to~$cs$.
236 \item[$cs$ addEs $rules$] \indexbold{*addEs}
237 adds unsafe elimination~$rules$ to~$cs$.
239 \item[$cs$ addDs $rules$] \indexbold{*addDs}
240 adds unsafe destruction~$rules$ to~$cs$.
242 \item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
245 Introduction rules are those that can be applied using ordinary resolution.
246 The classical set automatically generates their swapped forms, which will
247 be applied using elim-resolution. Elimination rules are applied using
248 elim-resolution. In a classical set, rules are sorted by the number of new
249 subgoals they will yield; rules that generate the fewest subgoals will be
250 tried first (see \S\ref{biresolve_tac}).
252 For a given classical set, the proof strategy is simple. Perform as many
253 safe inferences as possible; or else, apply certain safe rules, allowing
254 instantiation of unknowns; or else, apply an unsafe rule. The tactics may
255 also apply \ttindex{hyp_subst_tac}, if they have been set up to do so (see
256 below). They may perform a form of Modus Ponens: if there are assumptions
257 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
260 \section{The classical tactics}
261 \index{classical prover!tactics|bold}
262 \index{tactics!for classical proof|bold}
263 If installed, the classical module provides several tactics (and other
264 operations) for simulating the classical sequent calculus.
266 \subsection{Single-step tactics}
268 safe_step_tac : claset -> int -> tactic
269 safe_tac : claset -> tactic
270 inst_step_tac : claset -> int -> tactic
271 step_tac : claset -> int -> tactic
272 slow_step_tac : claset -> int -> tactic
274 The automatic proof procedures call these tactics. By calling them
275 yourself, you can execute these procedures one step at a time.
276 \begin{ttdescription}
277 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
278 subgoal~$i$. This may include proof by assumption or Modus Ponens, taking
279 care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.
281 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
282 subgoals. It is deterministic, with at most one outcome. If the automatic
283 tactics fail, try using {\tt safe_tac} to open up your formula; then you
284 can replicate certain quantifiers explicitly by applying appropriate rules.
286 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
287 but allows unknowns to be instantiated.
289 \item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. IF this
290 fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
291 This is the basic step of the proof procedure.
293 \item[\ttindexbold{slow_step_tac}]
294 resembles {\tt step_tac}, but allows backtracking between using safe
295 rules with instantiation ({\tt inst_step_tac}) and using unsafe rules.
296 The resulting search space is too large for use in the standard proof
297 procedures, but {\tt slow_step_tac} is worth considering in special
302 \subsection{The automatic tactics}
304 fast_tac : claset -> int -> tactic
305 best_tac : claset -> int -> tactic
307 Both of these tactics work by applying {\tt step_tac} repeatedly. Their
308 effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
309 solve this subgoal or fail.
310 \begin{ttdescription}
311 \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
312 depth-first search, to solve subgoal~$i$.
314 \item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
315 best-first search, to solve subgoal~$i$. A heuristic function ---
316 typically, the total size of the proof state --- guides the search. This
317 function is supplied when the classical reasoner is set up.
321 \subsection{Other useful tactics}
322 \index{tactics!for contradiction|bold}
323 \index{tactics!for Modus Ponens|bold}
325 contr_tac : int -> tactic
326 mp_tac : int -> tactic
327 eq_mp_tac : int -> tactic
328 swap_res_tac : thm list -> int -> tactic
330 These can be used in the body of a specialized search.
331 \begin{ttdescription}
332 \item[\ttindexbold{contr_tac} {\it i}] solves subgoal~$i$ by detecting a
333 contradiction among two assumptions of the form $P$ and~$\neg P$, or fail.
334 It may instantiate unknowns. The tactic can produce multiple outcomes,
335 enumerating all possible contradictions.
337 \item[\ttindexbold{mp_tac} {\it i}]
338 is like {\tt contr_tac}, but also attempts to perform Modus Ponens in
339 subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
340 $P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
343 \item[\ttindexbold{eq_mp_tac} {\it i}]
344 is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
347 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
348 the proof state using {\it thms}, which should be a list of introduction
349 rules. First, it attempts to solve the goal using \ttindex{assume_tac} or
350 {\tt contr_tac}. It then attempts to apply each rule in turn, attempting
351 resolution and also elim-resolution with the swapped form.
354 \subsection{Creating swapped rules}
356 swapify : thm list -> thm list
357 joinrules : thm list * thm list -> (bool * thm) list
359 \begin{ttdescription}
360 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
361 swapped versions of~{\it thms}, regarded as introduction rules.
363 \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
364 joins introduction rules, their swapped versions, and elimination rules for
365 use with \ttindex{biresolve_tac}. Each rule is paired with~{\tt false}
366 (indicating ordinary resolution) or~{\tt true} (indicating
371 \section{Setting up the classical reasoner}
372 \index{classical reasoner!setting up|bold}
373 Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
374 the classical reasoner already set up. When defining a new classical logic,
375 you should set up the reasoner yourself. It consists of the \ML{} functor
376 \ttindex{ClassicalFun}, which takes the argument
377 signature\indexbold{*CLASSICAL_DATA}
379 signature CLASSICAL_DATA =
384 val sizef : thm -> int
385 val hyp_subst_tacs : (int -> tactic) list
388 Thus, the functor requires the following items:
389 \begin{ttdescription}
390 \item[\ttindexbold{mp}] should be the Modus Ponens rule
391 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
393 \item[\ttindexbold{not_elim}] should be the contradiction rule
394 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
396 \item[\ttindexbold{swap}] should be the swap rule
397 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
399 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
400 search. It should estimate the size of the remaining subgoals. A good
401 heuristic function is \ttindex{size_of_thm}, which measures the size of the
402 proof state. Another size function might ignore certain subgoals (say,
403 those concerned with type checking). A heuristic function might simply
406 \item[\ttindexbold{hyp_subst_tac}] is a list of tactics for substitution in
407 the hypotheses, typically created by \ttindex{HypsubstFun} (see
408 Chapter~\ref{substitution}). This list can, of course, be empty. The
409 tactics are assumed to be safe!
411 The functor is not at all sensitive to the formalization of the
412 object-logic. It does not even examine the rules, but merely applies them
413 according to its fixed strategy. The functor resides in {\tt
414 Provers/classical.ML} on the Isabelle distribution directory.
416 \index{classical prover|)}