電子式里程表英文資料

1、 AutomationTom RidgeApril 12, 2005Contents1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Requirements. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2、. . . . . . . . . .13 Current Automation in Interactive Provers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54.1 Proof Search .

3、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .64.1.1 Logical System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.1.2 Intro Rules . . . . . . . . . . . . . . . . . .

4、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .64.2 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .84.2.1 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5、 . . . . . . . . . . . . . . . . . . . . . . .8 4.2.2 Conditional Simplification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2.3 Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

6、4.2.4 Dynamic Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .114.2.5 Equational Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 5 Interface and Integration . . . . .

7、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 6 Assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .136.1 Assessment wrt. Requirements . . . . . . . . . . . . .

8、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .136.2 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .146.3 Efficiency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9、. . . . . . . . . . . . . . . . . . . . . . .14 6.4 In Practice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 7 Alternative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10、. . . . . . . . . . . . . . .16 8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .191 IntroductionAutomation can be key to successful mechanisation. In some situations, mechanisation is feasible without automat

11、ion. Indeed, in highly abstract mathematical areas, most mechanised reasoning consists of the user spelling out complicated 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 de

12、fined subproblems. A typical example of such a mechanisation is our formalisation of Ramseys 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 mechanis

13、ation infeasible.Many man years have been spent developing fully automatic systems such as VampireVR and Otter McC. It would be foolish to imagine that we could compete with such systems. Their performance is way beyond that of systems currently implemented in interactive theorem provers. Projects a

14、re 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 ca

15、se 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 tec

16、hniques 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 proced

17、ures were developed in the HOL Light theorem prover, which we found to be an excellent vehicle for prototyping different approaches.2 RequirementsWhat do we require of our automation? Let us distinguish between automation for fully automatic use, and automation for interactive use, the requirements

18、for each being considerably different.Perhaps unexpectedly, failure of the automated proof engine is the norm, is the sense that when interactively developing complex proofs we spend most of our time on obligations that are almost provable. Thus we would like the prover to give us excel lent feedbac

19、k as to why obligations could not be discharged. Sym98This 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

20、before terminating a proof search). Indeed, automatic provers are judged on how many provable goals they can actually prove. In interactive pro of, we spend most of our time on obligations that are almost provable. This is the difference between interactive and automatic proof. If we spend most of t

21、he time trying to prove goals that are simply not provable, then completeness of the proof search becomes less important. This is not to say that it loses importance altogether: if a system lacks completeness, then it will fail to prove some provable goals. It is vitally important to know what sort

22、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 when combining systems: in order to understand the behaviour of the system as a whole oneshould first understand the behaviour of the parts.What properties

23、might be preferred, in an interactive setting, over completeness? 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 use

24、d 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 extremely complex thing to understand, and proofs which depend

25、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 t

26、o 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 for

27、m 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

28、 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 p

29、roof 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 a

30、s John Harrisons implementation of mo del eliminationHar96, 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

31、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

32、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 asE in many systems) should be performed, simplification steps

33、 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 r

34、ewritten. 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 i

35、s also important, although not necessarily completeness 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

36、 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 vi

37、sible, 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

38、 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 or not provable is less useful than automation that at least makes progress before returning. Automation

39、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 affe

40、ct 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 ProversThe current methods of automated proof in interactive theorem provers do not meet t

41、he 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 are combined in the single auto tactic. Isabelle also includes a model

42、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 simpl

43、e 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

44、) = yThis 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 failu

45、re 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

46、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 p

47、roving, 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 presentat

48、ions 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), bec

49、ause 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 sy

50、stem fails to make progress on goals that it is unable to prove outright.Let us also make the following observation about first order theorem provers. These provers are designed to find large quantifier instantiations, optionally modulo equality reasoning. Yet the failure of automation in interactiv

51、e theorem provers is not the failure to guess large quantifier instantiations.4 TechniquesIn the following sections, we describe how we built up the automation. First, we are trying to find proofs, so that we will need (at least) a proof search engine. Next, we wish to model, to a large extent, the

52、way the proofs were done by hand. Apart from proof search, the other main method employed during the hand proofs was simplification. We describe how we augment the simplifier.Conditional simplification is a form of simplification where the simplifier is invoked recursively in an attempt to solve con

53、ditions on rewrites that may be applicable to the current goal. We argue that invoking simplification on these goals is often not the best way to proceed, and suggest an alternative.Next, when using simplification, it is a good idea to ensure that the simpset is confluent and terminating. We describ

54、e an implementation of completion. When using simplification, however, one also wants to utilise assumptions that arise during the course of a proof as rewrites. To ensure the set of rewrite rules are still confluent and terminating, one must provide some form of dynamic completion during the proof

55、search itself. We discuss how we tackled these issues.4.1 Proof SearchIn this section, we describe our basic system for proof search. This is a single conclusion, intuitionistic system suitable for backwards proof search. We eschew unification in favour of term enumeration. This has several interest

56、ing consequences when combining proof search with other methods. Note that we are only interested in the automation of an essentiallyfirst order system.4.1.1 Logical SystemTwo main systems of proof search are resolution and tableaux. For automation in an interactive setting, resolution is too unnatu

57、ral. For this reason, tableaux are more promising. We therefore restrict our attention to tableaux based systems. Tableaux systems typically proceed by negating the goal and searching for a contradiction. We even consider that this is to o unnatural. We therefore focus on tableaux systems that execu

58、te directly in standard logical systems.Using such a system has significant advantages in terms of implementation complexity, since we can simply search at the level of HOL goals using more-or-less standard tactics. This also has advantages in terms of naturality, since the user is already familiar

59、with proof in such a system, and feedback, since we can present failing branches directly to the user, who does not have to translate the results from some alternative proof system.Single conclusion systems are unsuited to classical pro of, which is much better supported by multiple conclusion systems. However multiple conclusion systems are unnatural. If we are interested in classica