Automation
Tom Ridge
April 12, 2005
Contents
1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1
2 Requirements. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1
3 Current Automation in Interactive Provers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
4 Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
** Proof Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6
** Logical System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 ** Intro Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 ** Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . .8 ** Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 ** Conditional Simplification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 ** Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 ** Dynamic Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 ** Equational Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12
5 Interface and Integration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12
6 Assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 ** Assessment wrt. Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13
** Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 ** Efficiency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 ** In Practice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15
7 Alternative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16
8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19
1 Introduction
Automation can be key to successful mechanisation. In some situations, mechanisation is feasible without automation. Indeed, in highly abstract mathematical areas, most mechanised reasoning consists of the user spelling **plicated arguments which are far beyond those which can currently be tackled by automation. In this setting, automation, if it is used at all, is directed at easily solvable, tightly defined subproblems. A typical example of such a mechanisation is our formalisation of Ramsey's Theorem [Rid04]. On the other hand, automation can be fruitfully applied in verification style proofs, where the reasoning is relatively restricted, but the sheer level of detail makes a non-automated mechanisation infeasible.
Many man years have been spent developing fully automatic systems such as Vampire[VR] and Otter [McC]. It would be foolish to imagine that we **pete with such systems. Their performance is way beyond that of systems currently implemented in interactive theorem provers. Projects are underway [MP04] to link such systems to interactive theorem provers. This is extremely valuable work: if one knows that a first order statement is provable, then one should probably expect that the machine can provide a proof.
In this section, we outline some techniques we have applied in various case studies. Naturally we do not seek to solve the problem of automated reasoning once and for all. Rather we focus on the problems that typically arise in the case studies we have been involved with. We start by outlining the functionality we require of the automated engine. We then describe the techniques we applied, and how they were integrated. We evaluate the resulting engine qualitatively in terms of our requirements, and quantitatively with respect to a sizable case study. Few of these techniques are novel, rather, we seek to combine existing techniques in a suitable fashion.
These procedures were developed in the HOL Light theorem prover, which we found to be an excellent vehicle for prototyping different approaches.
2 Requirements
What do we require of our automation? Let us distinguish between automation for fully automatic use, and automation for interactive use, the requirements for each being considerably different.
Perhaps unexpectedly, failure of the automated proof engine is the norm, is the sense that when interactively **plex proofs we spend most of our time on obligations that are \provable. Thus we would like the prover to give us excel lent feedback as to why obligations could not be discharged. [Sym98]
This quote emphasizes an important difference between automatic and interactive proof. In automatic pro of, one typically knows that the goal is provable (or at least, suspects very strongly, and is prepared to wait a considerable amount of time before terminating a proof search). Indeed, automatic provers are judged on
how many provable goals they can actually prove. In interactive pro of, \obligations that are almost provable\spend most of the time trying to prove goals that are simply not provable, **pleteness of the proof search becomes less important. This is not to say that it loses importance altogether: if a system **pleteness, then it will fail to prove some provable goals. It is vitally important to know what sort of goals one is giving up on, in order that one can understand what it means when a prover fails to prove a goal. Such knowledge is also useful **bining systems: in order to understand the behaviour of the system as a whole one should first understand the behaviour of the parts.
What properties might be preferred, in an interactive setting, **pleteness? For us, the most important aspect of automation is simplicity. By this we do not mean implementation simplicity (how many lines did it take to implement the system? etc.), but conceptual simplicity. For instance, simplification is used ubiquitously in interactive theorem proving. If the set of rewrite rules is not confluent, then to understand the behaviour of the simplifier, one has to understand the order in which the rules are applied. Needless to say, this is an **plex thing to understand, and proofs which depend on these properties are presumably extremely fragile. Conceptual simplicity for a simplifier is closely bound up with confluence and termination of the simpset. Conceptual simplicity is important if a user is to understand the system. If a system is conceptually simple, it will hopefully be simple to use.
In an interactive setting, we expect automation to fail. In order to make progress, we must understand why a proof attempt fails: the prover must provide feedback. Resolution based systems can provide feedback, but they are destructive (in the sense that the goal is converted into a normal form before the proof attempt starts, destroying the original logical structure), so that the feedback can be difficult to understand (the point where the proof fails may lo ok very different to the original goal). A better approach is to conduct the proof in a way that is as close as possible to how a human might conduct the proof. We require the proof system to be natural in some sense. In this case, if a proof attempt fails, the failing branch can often be returned directly to the user for inspection.
Feedback is related to visibility. Often a user wishes to inspect a failed proof, but only a proof trace is available, which can cause a conceptual mismatch: the user is focused on sequents, whereas the trace may be of a different nature altogether. If there are many unproved branches, then a user might not inspect them all, but might wish to step through the proof. Automatic methods, such as John Harrison's implementation of mo del elimination[Har96], often search for a pro of in a tree making use of global information about nodes visited previously. If this global information is not present in the sequent the user has access to, it will be difficult to step through the automatic pro of by simply invoking the automatic prover a step at a time: the automatic prover will not make the same decisions it made when conducting the search using global information because it only has access to the
local sequent.
Many methods currently employed by interactive theorem provers, such as Isabelle's blast, leave the goal unchanged if they fail to prove it. Natural methods of proof search expect to make at least some progress in all situations, so that they can assist even if the goal is not provable. For instance, safe steps (such as∧E in many systems) should be performed, simplification steps applied and so on.
Automation should also be stable. In large proofs, one frequently mixes interactive and automatic proof. If the goals returned by automation are apt to change radically with slight variations in the goal, then the dependent interactive proofs can be rendered useless, and must be rewritten. For this reason, unsolvable subgoals returned by automation should be stable under small changes to the original goal.
If a proof can be found, then one begins to focus on aspects that make the pro of more maintainable, such as robustness. Efficiency is the icing on the cake. Completeness is also important, although not **pleteness in the full first order sense, but rather there should be a clear notion of the class of problems a given procedure solves. At any rate, it is vital to have some theoretical understanding of the behaviour of the system, if it is to approach the goal of being simple.
Let us summarize these points:
? Automation should be simple: it should be theoretically well understood, and predictable in use.
? Automation should also provide feedback, so that the user can assess why a proof attempt failed.
? An even stronger requirement is that automation be visible, in that one can directly inspect the execution of the automation e.g. by stepping though the pro of search.
? Automation should be natural, in order to minimise the conceptual gap between the prover and the user. For instance, automation should execute in standard logical systems that are close to, or identical with, the tactic level at which the user conducts proofs.
? Often, there are many safe steps that the user would make to progress a proof. Automation that simply returns \provable\is less useful than automation that at least makes progress before returning.
? Automation should be stable, so that small changes to theories do not produce large changes in the behaviour of the automation. This is important because interactive proofs contain large sections of interleaved user/automation steps.
? Automation should also be robust, in the sense that small changes do not affect automatic provability.
? We would like automation to be efficient for obvious reasons.
?Finally, we would like automation to be complete wrt. well defined classes of problems.
3 Current Automation in Interactive Provers
The current methods of automated proof in interactive theorem provers do not meet the requirements of the previous section.
Isabelle/HOL is representative of current HOL implementations as regards automation. The main automatic techniques that are used are a tableaux prover blast, and the simplifier simp. These **bined in the single auto tactic. Isabelle also includes a model elimination procedure which is similar in use to blast.
Simp is widely used, but is not a complete first order proof method. However, the fact that it does meet many of the requirements of the previous section explains why it is so popular in interactive proof. The blast method performs well on simple problems of predicate logic and sets, but it is hard to understand exactly what its properties are. It is based on a prover, leanTAP [BP95], that is complete for first order logic. On the other hand, the following goal is trivially provable in first order logic, but blast fails.
f (g a) = a┝ Зy .g(f y ) = y
This is even more upsetting when one realises that the term g a, occurring in the sequent itself, is a witness to the existential. To make matters worse, when expressed in a typed logic such as HOL, g a is the only term occurring in the sequent of the correct type that could be used! This failure to deal adequately with equational logic is a general failing of tableaux style procedures incorporating unification. The auto method is almost never used in the middle of interactive proofs because it is so unconstrained. Moreover, it is unstable, in that the subgoals it generates can be wildly different under minor changes to the goal, which renders is unusable except in tightly controlled areas.
The work [MP04] to integrate Vampire, a modern resolution prover, into Isabelle will not necessarily rectify these failings. Resolution based methods provide little support for interactive theorem proving, because the reduction to clause form means that the user has little visibility into the proof search, and little understanding of why a particular lemma failed. The proof search is a local forward synthetic search as opposed to a global backwards analytic search typical of tableaux presentations and the tactic level of Isabelle. Thus, resolution is an unnatural system for the user. In general the feedback from such systems is poor or at worst non-existent. Furthermore, whereas many steps should be considered safe(apply a terminating and confluent set of rewrites, perform a ∧E step), because the system is being used as a black box, either the goal is solved outright or, more usually, not solved at all, and information that is contained in the system about which steps can be safely applied is lost, leaving the user having to apply such steps manually. The problem here is that the system fails to make
电子式里程表设计资料-英文资料
