自动化外文翻译Word文档格式.docx

1、1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Requirements. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 Current Automation i

2、n 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104.2.4 Dynamic Completion . . . . . . . . .

6、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 8 Conclusi

10、on . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .191 IntroductionAutomation can be key to successful mechanisation. In some situations, mechanisation is feasible without automation. Indeed, in highly abstract mathematic

11、al 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 defined subproblems. A typical example of su

12、ch 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 mechanisation infeasible.Many man years have been

13、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 are underway MP04 to link such systems to i

14、nteractive 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 so

15、lve 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 inte

16、grated. 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 theor

17、em 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 for each being considerably different.Perh

18、aps 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 feedback as to why obligations could not be disch

19、arged. 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 before terminating a proof search）. Indeed

20、, 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 the time trying to prove goals that are sim

21、ply 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 of goals one is giving up on, in order tha

22、t 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 might be preferred, in an interactive sett

23、ing, 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 used ubiquitously in interactive theorem prov

24、ing. 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 on these properties are presumably extreme

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

26、 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, destroy

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

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

29、 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 Harrisons implementation of mo del

30、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 by simply invoking the automatic prover a

31、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 Isabelles blast, leave the goal unchanged if they

32、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 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 mu