Automation

 

Tom Ridge

 

April 12, 2005

 

Contents

1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1

 

2 Requirements. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1

 

3 Current Automation in Interactive Provers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

 

4 Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

4.1 Proof Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6

4.1.1 Logical System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

4.1.2 Intro Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6

4.2 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . .8

4.2.1 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8

4.2.2 Conditional Simplification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

4.2.3 Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

4.2.4 Dynamic Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11

4.2.5 Equational Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12

 

5 Interface and Integration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12

 

6 Assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13

6.1 Assessment wrt. Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13

6.2 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14

6.3 Efficiency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14

6.4 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 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 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 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 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 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 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, "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 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 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 one

should first understand the behaviour of the parts.

What properties 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 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 extremely complex 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 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 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" or "not 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 are combined 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 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 interactive theorem provers is not the failure to guess large quantifier instantiations.

 

4 Techniques

In 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 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 conditions 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 describe 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 search itself. We discuss how we tackled these issues.

 

4.1 Proof Search

In 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 interesting consequences when combining proof search with other methods. Note that we are only interested in the automation of an essentially

first order system.

 

4.1.1 Logical System

Two main systems of proof search are resolution and tableaux. For automation in an interactive setting, resolution is too unnatural. 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 execute 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 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 classical proof, we must admit that our single conclusion system has disadvantages. On the other hand, we believe that the large scale structure of proofs is mostly intuitionistic: typically we are focussed on one goal, and our lemmas serve as intermediate points in the proof, i.e. ├ A٨ B→ C as a lemma is not typically equivalent to ├ ┑(A ٨ B ) ٧C, since we expect to reach a point in the proof where A ｡ﾄ B is provable, not to do a disjunctive split. Certainly for the domains we are interested in, all proofs were essentially intuitionistic, with classical reasoning restricted to small areas which could be dealt with by simplification or other constrained techniques.

 

4.1.2 Intro Rules

There is one more improvement we wish to make. Although the procedure outlined above is complete, it is rather one sided. Since most proofs make heavy use of lemmas, the antecedent of a corresponding goal tends to become rather crowded. Moreover, many lemmas are naturally viewed as introduction rules, that is, are intended to be used to refine the conclusion C rather than used to chain forward fromГ . For these reasons, we also utilize intro rules à la Paulson [PNW03]. These are typically unsafe, but again, completeness can be preserved if we backtrack, and take other precautions. These intro rules are implemented in the same way as lemmas, but are marked as intro rules. During proof search, the conclusions of such lemmas are matched against the current goal. If the conclusion matches the current goal, the goal is replaced with the condition of the intro rule, and backtracking is employed in the event that these assumptions cannot be proved. If an intro rule is marked safe, then backtracking does not occur. Note that this improvement is unnecessary from a theoretical view, and its sole motivation is to model natural forms of proof.

If completeness is considered in a certain way, then this can be seen to preserve completeness. In the presence of simplification, one needs equational unification if these rules are to behave as expected. However, currently we simulate uses of equational unification by hand.

Failure of completeness for intro rules: if we use a rule as an intro rule, then we can fail to be complete? but this is not true- either the rule is safe, in which case we are fine, or unsafe, in which case we backtrack. the requirement of unification means that we can avoid using the rule as an additional assumption. however, this only works if at some stage we can use the rule as an intro rule- there are situations where an intro rule was intended to be used, but there was no connecting chain, whereas considered as an extra assumption there would have been no problem. eunification

Moreover, since we are not utilizing such a rule as a standard lemma, it is not even clear what notion of completeness to use. Let us define completeness wrt. an intro rule to mean that if there is a proof using the rule as a lemma, then there is a proof using the rule as an intro rule. In the presence of equality, we must therefore use eunification to ensure that our intro rule can be applied wherever possible. Since at every stage we have a finite set of ground terms, and a terminating and confluent rewrite order, such an approach can be made feasible, although at this stage we manually simulate such steps.

The use of intro rules brings complications because it is not clear what notion of completeness is appropriate. If the intro rule were used as a normal lemma, then completeness is preserved, since the lemma is handled just as it would be in normal predicate logic. The idea behind an intro rule is to balance the proof search, which would otherwise operate mainly on the left. The difference between a rule ├ A → B as a lemma, and as an intro rule, is that the automation can apply→ L with the rule as a lemma, whereas as an intro rule, we expect the goal to eventually become B, and to replace this with A.

 

4.2 Equality

4.2.1 Rewriting

Rewriting is the process of transforming a term by replacing subterms with equal subterms. For example, we might use the lemma f (a) = a to rewrite Q f (f (a)) to Q f (a) and then to Q a. In this section, we are informal about various rewriting notions. For more information the reader may consult the excellent [BN98].

A note on terminology: a simplification order is a restriction of a rewrite order, used to prove termination of a term rewriting system. However, the word "simplification" is often used informally to refer to rewriting, and the word "simpset" is often used to refer to the system of rewrite rules. We follow this informal usage.

Two key properties of simplification are termination and confluence. Without confluence, to understand the behaviour of the simplifier one must understand the order in which rewrites are applied. This is too much to expect of the user. Termination is useful in an interactive setting, for instance, to allow feedback. Moreover, termination allows simplification to be integrated with the main proof search. If we have both confluence and termination, then each term has a unique normal form, and equality testing becomes decidable. This is an extremely useful property of a simpset.

Our basic strategy is to apply simplification eagerly, after each step of the proof search, using assumptions to simplify other assumptions and the conclusion. We work with a terminating and confluent simpset. We check termination and confluence manually using completion. We apply simplification at the types of individuals. If the simpset is terminating and confluent, then this preserves completeness of the proof search. We also apply simplification at boolean type, which is not a possibility in first order logic. For instance, we employ higher order rewrites to miniscope quantifiers. It is not too difficult to argue that this also preserves completeness of the proof search. Assumptions resembling rewrites often arise during proof, and these may be incorporated into the simpset. Given an assumption x. P x, and an assumption P t, one could simplify P t = , which is again a simplification at Boolean type, and so not a first order operation. We do not use assumptions of this form as rewrites:our basic approach to quantifier instantiation is via term enumeration, and using these simplifications would destroy the completeness of this approach. We do use assumptions of the form x = y (possibly quantified) as rewrites. In order to retain confluence and termination we complete the simpset wrt. these dynamically arising rewrites. Because completion is not guaranteed to terminate, completion is limited to a certain number of steps, although in our applications, completion always succeeds.

 

4.2.2 Conditional Simplification

In this section, we describe conditional simplification, and note that the standard approach to solving the conditions -recursive invocation of the simplifier- may not be desirable. We suggest some other approaches, and discuss other problems with conditional simplification. We conclude that conditional simplification is, at present, too complicated to count as a "simple" technique, and certainly too complicated to be linked with proof search in a reasonable way. We suggest the alternative of considering conditional rewrites just as ordinary lemmas.

Simplification works with rewrites of the form a = b, rewriting a to b anywhere in the goal. Conditional simplification works with conditional rewrites of the form    ├A→a = b(where A is typically a conjunction). In a sequent Г├ C, we are justified in rewriting a to b in the goal C if we can prove A from  ﹃C, Г.

How should we attempt to prove the condition A? Suppose we are linking a complete proof search system with simplification. In this case, very good (from a theoretical standpoint) behaviour would be obtained by requiring that, if A is provable, then it is actually proved. Because the search for a proof of A is potentially non-terminating, we would then have to orchestrate a complicated process of interleaving the main proof search, with the subproof searches attempting to solve the conditions on conditional rewrites. Such an approach is unpalatable not only for efficiency reasons.

One of the benefits of simplification is that, unlike proof search, it is terminating. If we wish to preserve this terminating behaviour, whilst employing conditional simplification, we must tame the non-termination involved when attempting to prove the conditions. One way would be to employ our main proof search to prove the conditions, but limit the search to a particular depth. This is unpalatable too. In order to keep simplification running in a reasonable amount of time, it is likely that this depth would have to be very small, because conditions arise very frequently. It is likely that this small depth would not permit the solution of many more conditions than other simple approaches. Limiting proof search to a small depth means that its theoretical limitations also become practical limitations: any limited proof search will be incomplete, but with large depth we could hopefully ignore such incompleteness. Small depth means that we would probably encounter situations where it was clear to the user that the condition could be solved, but that the restricted depth of the search meant that the condition was not solved. In our experience, the depth would have to be at least 10 logical steps (∨E etc.), coupled with intermediate effective equality reasoning(we imagine a scenario where we have an proof search which handles equality effectively). In experiments, performance with this approach became impractical in terms of response times from the simplifier, after a depth of around 4. It is possible that this approach will be feasible for computers in the (distant?) future. At the moment it is not.

An alternative to using limited proof search to solve the conditions is to fix a decidable class of conditions, and accept that there will be some conditions that may be provable, but that will fall outside the given class. The obvious choice is propositional logic. However, the problems with conditional simplification extend much deeper than the occasional failure to prove a propositionally valid condition, as we discuss later, so that this approach would not yield any great practical benefit, although the behaviour would at least be theoretically well understood.

The current approach taken in HOL, HOL Light, and Isabelle, is to invoke the simplifier itself on the conditions. This recursive calling is potentially non-terminating (conditional simplification is extremely prone to looping), so that the number of times the simplifier is recursively invoked is limited. This restriction of the depth of search when solving conditions suffers from the same problems as those discussed in the previous paragraph. The approach is in many ways worse than that above because the exact properties of simplification, which are necessary if one is to understand its behaviour when solving conditions, may be unclear even on propositional conditions, let alone conditions involving predicates. For a typical goal, we only require that simplification makes progress in a way that is simple to understand. For conditions, our requirement is usually that the condition is solved if possible. Simplification is not a complete form of proof, so we are hoping that our conditions will be such that the simplifier usually performs well. However, the simplifier cannot prove all prepositional conditions so that its behaviour even at the propositional level is hard to understand. On quantifier reasoning, even at the most basic level, failure is the norm.

So, current approaches fail to deal adequately with the problem of non-termination when proving conditions. Moreover the class of conditions solvable by simplification is hard to characterize, and so will not qualify as "simple" for the user to understand.

 

4.2.3 Completion

Completion is a process that can ensure a simpset is confluent and terminating.    Confluence and termination are the two main properties that we require of a simpset, so that completion is clearly a useful tool for when employing simplification. We discuss our use of completion.

The standard example of using completion on the axioms of group theory, to derive a set of terminating and confluent rewrite rules that constitute a canonical rewrite system for this theory, show that completion is a powerful technique. In our work, such power was never needed. We implemented basic completion which we found to be very useful. Because our needs were limited, we did not implement the full completion procedure of Huet, although in different settings this would be desirable. We leave this for future work.

Our completion procedure also permits conditional completion. When working in a typed setting, one often wishes to refer to a subset of the individuals at a given type. Then one introduces a predicate subtype, and restricts statements to talk about members of the subtype only.

 

4.2.4 Dynamic Completion

We mentioned previously that it is often the case that one wishes to use assumptions as rewrites. Clearly, the assumptions are dynamic and change throughout the course of a proof. Although we may start off with a confluent and terminating set of simplification rules, if we use assumptions as rewrites, it may very well be that our base simpset, augmented with assumptions, is no longer confluent and terminating. If we wish to preserve the properties that accompany a terminating and confluent simpset, then we must perform some sort of completion during the course of a proof. We call such completion dynamic, since it must be performed on the fly during the course of a proof.

Unfortunately, completion is a rather costly process. Moreover, it is in general nonterminating. Yet, when one looks at the kind of rules that are being used, typically they are of a very simple form. For instance, we often derive assumptions similar to

 a = b ٧ a = c, then proceed to do a disjunctive elimination. The resulting goals have assumptions a = b and a = c which we wish to use as simplification rules. The majority of these simplification rules are ground. In this case, completion is guaranteed to terminate, and one feels that there should be a way of short-circuiting the completion procedure to get an equivalent procedure that perhaps runs faster. Hopefully, if we can reduce completion to mere rewriting of one rule by another, then one can hope that the rewriting procedures are relatively highly optimised (certainly this is the case for Isabelle's fantastically good simplifier, and HOL Light's simplifier is optimised to some extent also), and that the performance will be acceptable.

There are several papers covering completion with ground terms. We looked at [GNP +93]. This algorithm takes a set of ground rewriting rules, and produces a reduced canonical rewriting system in polynomial time. Unfortunately, although the procedure operates in polynomial time, it makes use of congruence closure. Congruence closure is not implemented in HOL Light or Isabelle, and it is likely that an unoptimised version would be relatively slow (that is, although the algorithm from [GNP+93] is polynomial in time, there would be a high constant of proportionality). Of course, during a proof one is making incremental changes to the set of equalities, so one might hope to improve on this somewhat, but still there was a feeling that we should be able to do better.

Looking at the assumptions we use as rewrites, it was clear that beyond being ground, they were of an even simpler nature: no subterm of a left hand side was used in any other rewrite rule (for instance, with assumption a = b, there were no proper subterms of the left hand side at all, and we never had occasion that another assumption of the form a = d occurred at the same time). In this instance, it sufficed to rewrite all the other simplification rules with this rule in order to maintain confluence and termination. If we require online completion where these conditions are not satisfied, we would fall back on our (time limited) completion procedure, but in our case study this does not happen. When considered in the context of the proof of correctness of basic completion, this result is clear. However, during our case studies there were a number of tricky scenarios which, without this optimisation, caused our prover to take extraordinarily longer.

 

4.2.5 Equational Unification

Our top level proof search is based on enumerating terms up to a fixed term depth. Unification is not present at all in such a procedure. We introduce intro rules, à la Paulson, into our search procedure. Currently this is accomplished simply by matching conclusions of intro rules against the current goal.

The intro rules are treated like other lemmas, in that they are incorporated into the

sequent as additional assumptions. However, they are marked as intro rules. We instantiate them with terms from the enumeration just like other lemmas. The conclusions get rewritten by the simplifier. At each stage of the proof search, we check whether the conclusion of any intro rule matches the current goal, and if so we replace the goal with the condition of the intro rule, backtracking over unsafe intro rules. This has the effect of simulating equational unification.

 

5 Interface and Integration

In this section we describe how the techniques outlined in the previous section are integrated into a single tactic, and the interface between this tactic and the user.

Our automation consists of a tableaux proof search, with quantifier instantiation to a fixed term depth, interspersed with calls to the simplifier. How should these be integrated? If simplification is terminating and confluent, then the obvious strategy of applying simplification after every step of proof search preserves completeness. This is the essential observation behind the integration of these two techniques.

The tactic provides an interface to the user. To use the procedure the user must specify a set of terminating and confluent rewrite rules and a set of introduction rules. In fact, the user also specifies a set of lemmas that should be considered during the pro of, and these are simply incorporated into the goal statement as described previously. Proof search proceeds, with safe rules and simplification applied eagerly, and with backtracking over unsafe rules. If proof is unsuccessful, the failing branch is returned to the user at the point where no safe rules, or simplification steps, could be applied. A downside to our approach is that the sequent can get rather large, since we are instantiating quantifiers with all (type-correct) terms below a certain depth. It would be trivial to adapt the user interface so that these instantiations are not directly presented to the user, but are viewable on demand. We leave this to further work.

 

6 Assessment

In this section, we discuss how our proof procedure fairs in terms of the criteria outlined in Sect. 2. We then discuss the issue of completeness. We do not claim to have a formal proof for completeness wrt. some class of problems, but we do argue that the procedure has good properties. We assess the efficiency by locating our technique wrt. other theorem proving techniques such as resolution. We then assess the practical use of the procedure by giving examples of its success, and by describing the "feel" of the procedure.

 

6.1 Assessment wrt. Requirements

Our procedure was designed with the criteria of Sect. 2 in mind. We feel that it meets the requirement of simplicity. Conceptually, we are performing a standard intuitionistic proof search. We incorporate safe and unsafe rules. We use simplification, both at the logical level (type boolean) and at domain specific types. Our simplification rules should be confluent and terminating. We ensure that any assumptions used as rewrites do not destroy this important property. We use simplification, and conditional simplification rules only in restricted instances where they are well behaved. All these notions are readily comprehensible.

Conceptual simplicity leads to simplicity when using the procedure. We must only decide on our simpset, our set of intro rules, and the lemmas relevant to the goal. The tactic executes at the tactic level, so we can step through a failed proof attempt by invoking the tactic a step at a time. Since the procedure is non-destructive (in the sense that we search directly using the rules of natural deduction, rather than converting to normal form), we have a high level of visibility into the proof search. Failing branches are typically immediately comprehensible. The notion of safe steps means that even if we fail to find a proof, we return to the user having performed a considerable amount of work i.e. we make progress. Incompleteness manifests itself as a failure to guess large quantifier instantiations. Incompleteness can also arise as a failure of completion, which the user invokes prior to proof search. Incompleteness

also arises during pro of search, with the failure of dynamic completion.

Simplicity leads to stability. One of the properties we would claim is that the prover is monotonic, in that adding lemmas, simplification rules, or unsafe rules does not cause the procedure to fail when before it had succeeded. Likewise the prover is robust in the face of minor changes to definitions and so on. We would not claim that the procedure is efficient.

 

6.2 Completeness

There are several sources of incompleteness in our automation. Provability in FOL is in general undecidable. We restrict to a depth limited subset of the term universe. Whether there is a pro of involving only depth restricted terms is now decidable, but we will inevitably fail to find proofs that involve terms lying outside our restricted subset. This is a source of incompleteness. However, we may successively increase the term depth and in this way regain completeness at a cost to decidability.

FOL can be embedded in equational reasoning [McK75], so that one expects that equality reasoning manifests similar problems to general proof search. Our approach is to restrict ourselves to terminating and confluent sets of rewrite rules. Since completion may fail, or may not terminate, this is a source of incompleteness. Moreover, we employ completion dynamically, which can similarly fail, although in practice this was not a problem. However, completion is largely handled interactively by the user. If the user ensures that the set of rewrite rules is confluent and terminating, and if dynamic completion during proof search always succeeds, then our equality handling will be complete.

 

6.3 Efficiency

The current success of automatic methods rests largely on unification, whereas we use unification only trivially, when handling intro rules. In terms of proof search, our procedure will be broadly similar to pre-unification procedures, such as Gilmour's procedure, in terms of performance. For instance, the following goal5 is decidable:

( xyz.P x y →P y z →P x z)

→ ( xyz.Q x y → Q y z → Q x z)

→ ( xy.P x y→P y x)

→ ( xy.P x y ∨ Q x y)

→ ( xy.P x y) ∨ ( xy.Q x y)

Indeed, the truth or falsity of such a formula can be evaluated in a model with just four elements. However, even though such a goal is decidable, even some modern resolution based provers struggle. Sadly, our procedure is doomed to take an extremely long time. In defense, such goals are rarely met in interactive theorem proving. If they are met, the user is of course free to call a resolution prover interactively to solve them.

In addition to basic pro of search, we pay special attention to equality reasoning. Our approach to equality rests on completion, and so is suitable only in case various conditions are satisfied. However, if these conditions hold, this approach to equality is probably as effective as exists elsewhere. Modern resolution provers employ unfailing completion, which will presumably behave not more efficiently than completion in case a complete set of rewrites exists.

 

6.4 In Practice

Because it is conceptually simple, the prover is very easy to use. One typically moves from one theorem to the next, and invokes the prover with the simpset and the set of previous lemmas to use, often unchanged from the previous theorem. If a proof is not found, we see the failing branch. This branch is usually readily comprehensible. Almost always (in our case study, always) one needs to add either a simp rule, or a non-trivial lemma. If the lemma is not already proved one must break out and prove it. Having added the necessary rule, the process is repeated, usually with success. Generally, we do not tailor the sets of simplification rules and lemmas to each theorem: these rules are utilised depending on the context, and it is always a good idea to use them if available, by their very nature. Against this, too many rules can cause the performance to degrade, but generally one is working in a given theory, where the number of lemmas is relatively restricted.

Occasionally one must instantiate a quantifier with a clever term, but these are naturally difficult steps. The ability to step through the proof at the user level (rather than inspecting some representation of the failed branch) is very useful, and provides great visibility if something is not working correctly.

We argued that completeness was not of overriding importance, but clearly the aim of automation is to assist the user in proving lemmas. If the automation can prove the lemmas outright, we will not complain.

In our case study we carried out many proofs. One of the main results consisted of over 250 lines of interactive proof script. These proof scripts were not transcriptions of the original proofs, so that automation could feasibly reproduce them. Our automation was able to solve each of the lemmas. We give statistics for a section of the proof concerning a lemma theorem_ 3_ nes_Mup, which is representative of the other lemmas. This lemma in turn consists of a sublemma, theorem_ 3_ nes _ Mup _3. In the following table, we record the theorem name, the lines of tactic script without our automation, the lines with our automation, and the time taken. The sublemma theorem_3_nes_Mup_3 was fed to the automation when proving theorem_3_nes_Mup.We also record what happened when this sublemma was omitted, and the main lemma attempted without this assistance, theorem_3_nes_Mup'. This involved the prover reproving the sublemma during the proof of the main lemma. In this case, a pro of was also found, although this took over 5 minutes. However, we believe this was due to inefficient implementation of the automation tactic, and we intend to reimplement this in future work. These lemmas are representative of the effect of the automation on the other lemmas in the case study. Moreover, we have applied such techniques in other areas, with similar success.

Even though the performance is poor, coordinating these pro of procedures so that such

 

Tactic       Automated         Automated

Theorem Name                 Lines          Tactic Lines        Time/s

theorem3_ nes_Mup _3           28                1                66

theorem3_ nes_ Mup             12                1                24

theorem3_ nes_Mup'             n/a                1               305

 

lemmas could be proved is a major achievement. The fact that we are able to do so in a general way provides evidence that the procedure has good theoretical properties.

 

7 Alternative

The automation we developed was motivated by the problems we met during our case study. However, the fact that we were always able to complete our simpset must be counted a lucky accident. In general we can expect completion to fail e.g. for rules expressing commutativity, so that an approach to testing equality of two terms via a canonical set of rewrites appears too strong. There are ways of handling problematic situations, such as rules for commutativity, e.g. by ordered rewriting, but we would like to take this opportunity to consider an alternative general approach to equality handling.

So far, our pro of search limits the depth of terms considered. It seems very reasonable to likewise limit equality reasoning to a subset of the term universe, and employ congruence closure within this restricted subset. This introduces incompleteness of course.

Proving s = t using the axioms for equality requires, in general, terms of arbitrarily large depth. If we restrict the depth of the terms we consider, our equality reasoning will be incomplete. For instance, suppose we prove an equality s = t by a transitivity chain s = u = v = x = y = t. One can picture such a proof as shown in Fig. 1. If we restrict the depth of terms we consider to d or less, the picture might resemble Fig. 2. In such a situation, the equalities s = u = v will be derived, but the equalities x = y and y = t will not be. If no proof of s = t exists within the restricted term universe, we will not be able to deduce s = t.

Thus at any given stage of our pro of search, our equality reasoning will be incomplete. However, if we successively increase the depth of terms we consider, we regain completeness for equality reasoning.

In this setting, equational unification, wrt. the restricted set of terms, becomes decidable, and moreover can be implemented very efficiently.

Another advantage of this approach is that the representative for the equivalence class can be chosen in a user specified manner. For example, the user might choose the smallest member of the equivalence class as representative, or the smallest wrt. some lexicographic path order. This can help to keep sequents readable.

Another advantage of this approach is that it is simple for the user to understand, and moreover dovetails well with our approach to pro of search. The focus on a single measure of complexity, i.e. term depth, over several procedures, is a unifying step. Moreover, the disadvantages and incompleteness of the approach via completion are absent here. We leave the implementation of this alternative to future work.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Term depth

 

 

 

s   u   v   x  y   t

 

 

Term

 

Figure 1: Equality Proof by Transitivity

 

 

 

d

 

Term depth

 

 

 

s   u   v   x   y    t

 

Term

 

Figure 2: Equality Pro of by Transitivity, with Depth Restriction

 

 

 

8 Conclusion

We have presented the automation we developed to tackle a large case study. The automation is tailored to interactive use. The automation is based on the integration of a pro of search engine and simplification, relying essentially on completion.

The contributions of this section are to address the failings of current automation in an interactive setting, in terms of basic pro of search, and its integration with simplification. Our techniques do not step outside the realm of predicate logic with equality, but even in this very restricted domain, we encountered numerous problems. On the other hand, having solved these problems, we had no requirement for domain specific automation. We do not deny that in areas like linear arithmetic, such procedures are necessary for effective automation. However, our experience suggests that simplification and proof search are a very effective combination. This may be an instance of the phenomenon in logic that "a little goes a long way".

In the previous sections we noted several possibilities for future work, which we here summarize.

• The theoretical issue of completeness of intro rules should be addressed, although this is unlikely to have much of a practical impact.

• The issue of how lemmas are incorporated during proof search should be addressed. Craig's Interpolation Lemma suggests the naive approach based on syntactic features

shared between the current goal and a lemma: if a lemma and the current goal are expressed in different languages, then the lemma is not useful in order to prove the current goal. Craig's Interpolation Lemma holds for FOL, but it may be possible to extend the idea to richer theories.

• Completion may be extended to full completion ` a la Huet. Conditional completion should also be implemented so that it copes with common cases, and supporting theory should be developed. Further, the implementation of completion should be parameterised by a notion of equality which is not identical with HOL's inbuilt equality, in order to support different equality notions. An additional task is to integrate good automatic termination provers, such as AProVE [GTSKF04] with the completion procedure, so that user interaction is minimised.

• The interface for the automation should be extended so that the user is not swamped with to o much information.

• The automation as a whole needs reimplementing in order to increase the efficiency of the tactic.

• We intend to implement the alternative approach to handling equality via congruence closure and link this with proof search.

This covers future work arising as a direct consequence of this work. We now consider other opportunities which this work has uncovered.

Although we believe our approach largely solve the problem of proof for a given lemma, still the choice of lemmas and definitions is largely a matter of art. In the case of lemmas, we typically accumulate them on the boundaries of theories, then look for general lemmas that cover several of these as instances. This strengthening is reminiscient of the strengthening of inductive hypotheses.

We also found that in some areas, there was an explosion of non-trivial lemmas on the boundaries between theories, which could not be reduced by generalising. This typically occurs for common mathematical objects, such as trees. Many of the lemmas are intuitively immediately plausible, but their proofs often involve considerable e ort. In this case, it seems hard to control the spread of the subtheory into the main theory, since the lemmas of the subtheory are used so pervasively in the main theory. So here we have three related problems, namely

• Explosion of non-trivial and independent lemmas required from a subtheory.

• Lemmas intuitively plausible, hard to prove.

• Lemmas permeate main theory, reducing modularity and making the main theory

heavily dependent on the subtheory.

There seems to be no way to reduce the explosion in the number of lemmas. In terms of proof, we note that the difficulty arises from the need to state induction lemmas carefully, so that this is primarily a failure of automation of inductive proof. We also note that most of the definitions in this area are implicitly executable, so that there is scope for some form of model checking via execution of the definitions. This in turn could be used to tip off an inductive prover as to the truth or otherwise of conjectured lemmas.

We have not touched on the subject of automating induction, or other higher order

features. We have more to say about induction in Sect. ??, but suffice it to say this seems like a difficult area.

We would also like to note the difficulty in reasoning about combinations of tactics. We feel that recent moves [?] towards a calculus of tactics could prove interesting. We suggest that relatively trivial steps, such as ensuring that tactic scripts are tree structured rather than linearly structured, and incorporating proper handling of parameters in proofs via lambda binding at the ML level, can improve robustness of scripts. However, beyond this the way is unclear.

There is much related work. Automatic theorem proving is already a vast field, and we cannot hope to survey it in a reasonable space. Our primary source was the two volumes of the Handbook of Automated Reasoning [RV01]. We note the prevalence of model theoretic methods over proof theoretic methods, which can make implementing some techniques problematic. Our work is aimed at addressing the needs of automation in an interactive setting. Relevant here is the PhD of Syme [Sym98] who addresses the needs of automation in a declarative setting. Much of his conclusions apply in an interactive setting. Our analysis of the problems of automation in an interactive setting draws on his work.

編號(hào)：               

 

 

 

 

 

畢業(yè)設(shè)計(jì)英文翻譯譯文

 

 

 

題    目:        Automation        

院 （系）：       計(jì)算機(jī)系         

專    業(yè)：        自動(dòng)化          

學(xué)生姓名：        李 林           

學(xué)    號(hào)：       201300022        

指導(dǎo)教師：        王 超           

          職    稱：        實(shí)驗(yàn)師          

 

 

 

 

                 

2005 年 6 月 3日

 

自動(dòng)化

湯姆里治

2005 年四月 12 日

目 錄

 

1  介紹  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1                                                   

2  需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1                                                   

3  目前交互式證明器的自動(dòng)化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4                         

4  技術(shù). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5                          

4.1 證明的搜尋. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6

4.1.1邏輯系統(tǒng). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6

4.1.2引進(jìn)規(guī)則. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6

4.2 等式. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8

4.2.1改寫. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8

4.2.2條件的簡(jiǎn)單化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9

4.2.3完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

4.2.4動(dòng)態(tài)的完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11

4.2.5方程式的統(tǒng)一. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12

5  連接與整合. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12                              

6  評(píng)估. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13                                               

6.1 評(píng)估生產(chǎn)需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13

6.2 完整性. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

6.3 效率. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14

6.4 實(shí)際應(yīng)用. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

7  替代選擇. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16                                                  

8  結(jié)論. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19                                                  

 

 

 

 

 

 

 

1  介紹

自動(dòng)化可能是成功的機(jī)械化的關(guān)鍵。在一些情形中，機(jī)械化不需要自動(dòng)化就可以實(shí)行。確實(shí)，在高度抽象的數(shù)學(xué)區(qū)域，大部分由使用者拼出的復(fù)雜證明組成的機(jī)械化推論遠(yuǎn)遠(yuǎn)超過(guò)了那些目前能被自動(dòng)化解決的范圍。在這一背景下，如果自動(dòng)化它被全部使用， 將指導(dǎo)在容易的可以解決的被緊緊地限定的次問(wèn)題上。一個(gè)機(jī)械化的典型例子是我們的拉姆齊定理的形式化。另一方面，在推論相對(duì)被限制的地方，自動(dòng)化能富有成效地在確認(rèn)類型的證明中被應(yīng)用，但是絕對(duì)程度的細(xì)節(jié)將使一個(gè)非自動(dòng)化的機(jī)械化不可實(shí)行。

許多人已經(jīng)花費(fèi)了數(shù)年來(lái)發(fā)展全自動(dòng)系統(tǒng)。比如Vampire [VR] 和otter [McC]全自動(dòng)系統(tǒng)。我們可以和這樣的系統(tǒng)競(jìng)爭(zhēng)的設(shè)想是愚蠢的。它們的執(zhí)行是一種方式，這種方式超過(guò)目前在交互式定理證明器被實(shí)行的系統(tǒng)。這些計(jì)劃正在進(jìn)行是為了把這些系統(tǒng)和交互式定理證明器相連。這是極其有價(jià)值的工作：如果知道一個(gè)一階的陳述是可證明的，這時(shí)應(yīng)該期待機(jī)器能提供一個(gè)證明。

在這一節(jié)中，我們簡(jiǎn)略說(shuō)明一些我們已經(jīng)在各種不同的情況應(yīng)用研究的技術(shù)。自然地我們不企圖僅此一次去解決自動(dòng)化推論的問(wèn)題。寧可我們把重心集中在問(wèn)題，而這些問(wèn)題典型地出現(xiàn)在我們已經(jīng)涉及的研究。我們首先簡(jiǎn)略說(shuō)明我們需要的自動(dòng)化的引擎功能。我們?nèi)缓竺枋鑫覀儜?yīng)用的技術(shù)，而且他們是如何整合的。我們?cè)u(píng)估根據(jù)我們的需求性質(zhì)上地產(chǎn)生的引擎，和數(shù)量地有關(guān)于一件相當(dāng)大的案例研究。這些技術(shù)中的少數(shù)是新奇的，寧可，我們企圖用一種適宜的方式來(lái)融合現(xiàn)行的技術(shù)。

這些步驟在HOL啟發(fā)定理證明器被發(fā)展，這是我們建立的設(shè)計(jì)原型的一輛優(yōu)良車輛的不同方法。

 

2  需求

我們的自動(dòng)化的需求是什么? 讓我們區(qū)別一下自動(dòng)化和全自動(dòng)化的使用，以及交互式自動(dòng)化的使用，每一種的需求都有非常地不同。

也許料想不到地，失敗的自動(dòng)化證明引擎是基準(zhǔn)，是觀念，這觀念是當(dāng)交互式發(fā)展的復(fù)雜證明使我們花費(fèi)大多數(shù)時(shí)間對(duì) " 幾乎 " 的可證明的義務(wù)的時(shí)候。因此我們想要證明器給我們完美的反饋?zhàn)鳛闉槭裁慈蝿?wù)不能夠被執(zhí)行的原因。

這引證強(qiáng)調(diào)一種在自動(dòng)化和交互式證明之間的重要的不同。在自動(dòng)校對(duì)中，可典型地知道，目標(biāo)是可證明的 ( 或至少，非常強(qiáng)烈地懷疑，而且在結(jié)束相當(dāng)多量的時(shí)間之前準(zhǔn)備等候證明的搜尋)。的確，自動(dòng)證明器被判斷在他們能實(shí)際上證明多少可證明的目標(biāo)之上。在交互式證明中，" 我們花費(fèi)我們大多數(shù)的時(shí)間在幾乎可證明的義務(wù)上"。這是交互式和證明之間的不同。如果我們花費(fèi)大部份的時(shí)間嘗試去證明簡(jiǎn)單但不可證實(shí)的目標(biāo)，然后校正的搜尋完全變成比較不重要。這雖不能說(shuō)是它全部失去重要:：如果一個(gè)系統(tǒng)缺乏完整性，這時(shí)它將會(huì)無(wú)法證明一些可證明的目標(biāo)。什么類型的目標(biāo)正在被放棄，這是非常必要而且主要去知道的，這是為了知道當(dāng)一個(gè)證明器失敗于證明一個(gè)目標(biāo)時(shí)就能理解它是什么意思。這些知識(shí)也非常有用，當(dāng)混合系統(tǒng)為了了解作為整個(gè)系統(tǒng)的行為，應(yīng)當(dāng)首先了解部分的行為。

在一個(gè)交互式的環(huán)境中，在完全之上所有物可能被偏愛(ài)，就我們而言，自動(dòng)化的最重要方面是簡(jiǎn)單化。 而這些我們不是意味著去落實(shí)簡(jiǎn)單 ( 要布多少根線來(lái)實(shí)現(xiàn)系統(tǒng)? 等等)，而是概念上的簡(jiǎn)單化。例如，簡(jiǎn)單化到處被用于交互式定理求證。如果一組改寫規(guī)則不能融合，這時(shí)去了解簡(jiǎn)化器的行為，必須了解適用的規(guī)則順序。不用說(shuō)，對(duì)于理解這是一件極端復(fù)雜的事情，而且屬于這些所有物的證明在推測(cè)上極端易碎。概念上的簡(jiǎn)單化通過(guò)聚集和簡(jiǎn)易裝置的終端對(duì)一個(gè)簡(jiǎn)化器進(jìn)行緊密地約束。如果一個(gè)使用者要了解系統(tǒng)，概念上的簡(jiǎn)單化很重要。如果一個(gè)系統(tǒng)的概念簡(jiǎn)單，它將會(huì)很有希望被簡(jiǎn)單的使用。

在一個(gè)交互式環(huán)境中，我們期待自動(dòng)化失敗。為了取得進(jìn)步，我們必須了解一種證明的嘗試為什么失敗，證明器一定會(huì)提供反饋�；�于系統(tǒng)的決議能提供反饋，但是他們是毀滅性的 (在某種意義上目標(biāo)轉(zhuǎn)換成一種正常的形式在證明的嘗試之前開(kāi)始，破壞了最初的邏輯結(jié)構(gòu))，所以反饋很難被了解 (論證失敗的點(diǎn)對(duì)于最初的目標(biāo)能看出明顯的不同)。較好的方式是引導(dǎo)在一個(gè)盡可能接近的方法證明到一個(gè)人類可能如何引導(dǎo)證明。在一些感覺(jué)中我們需要證明的系統(tǒng)應(yīng)該是自然的。在這情況下，如果一種證明的嘗試失敗，失敗的部分能時(shí)常被作為檢驗(yàn)直接地返回給使用者。

反饋與能見(jiàn)度相關(guān)。時(shí)常一個(gè)使用者希望檢查失敗的證明，但是只有證明的蹤跡是可得的，它能引起一個(gè)概念上的錯(cuò)誤結(jié)合: 使用者把重心集中在結(jié)果，然而蹤跡可能全部是有不同的自然。如果有許多沒(méi)有被證明的部分，這時(shí)一個(gè)使用者不可能檢查它們的全部，但是可能愿意沿著證明走。像約翰 哈里森的模式消除的執(zhí)行的自動(dòng)化方法，時(shí)常利用全球化的節(jié)點(diǎn)優(yōu)先尋址的信息在一棵樹(shù)里搜尋一個(gè)證明。如果全球化的信息不是出現(xiàn)在結(jié)果中使用者有機(jī)會(huì)接近，它將會(huì)難以經(jīng)過(guò)通過(guò)簡(jiǎn)單運(yùn)用的自動(dòng)證明器一步一次的自動(dòng)化證明。當(dāng)傳導(dǎo)的搜尋正在使用全球化的信息時(shí)，自動(dòng)證明器將不做出它做出的相同決定，因?yàn)樗�只能進(jìn)入本地的結(jié)果。

許多方法現(xiàn)在被交互式定理證明器所使用，就像伊莎貝爾的blast，留下未改變的目標(biāo)如果它們失敗于證明這目標(biāo)的話。證明搜尋的自然方法期待在所有的情形中至少能做出一些進(jìn)步，所以即使目標(biāo)不是可證明的，它們也能夠有所幫助。 比如，安全的步驟 (就像在許多系統(tǒng)的∧E) 應(yīng)該被實(shí)行，簡(jiǎn)單化步驟被應(yīng)用等等。

自動(dòng)化也應(yīng)該是穩(wěn)定的。在大量的證明中，一個(gè)證明時(shí)�；旌辖换ナ胶妥詣�(dòng)的證明。如果被自動(dòng)化返回的目標(biāo)容易根本地以目標(biāo)的微小變化改變，這時(shí)關(guān)聯(lián)的交互式證明將被毫無(wú)用處的給予，而且一定被改寫。因?yàn)檫@一個(gè)理由，被自動(dòng)化返回的不能解決的次目標(biāo)應(yīng)該在對(duì)于最初的目標(biāo)的微小改變下穩(wěn)定。

如果一個(gè)證明能被建立，然后一開(kāi)始把重心集中在使證明更加可維持的方面，就像魯棒一樣。效率是在蛋糕上的糖衣。完全也是重要的，雖然沒(méi)有必要在一階邏輯完全，但是寧可應(yīng)該有一個(gè)給定的程序解決的層次問(wèn)題一個(gè)清楚的觀念。無(wú)論如何，一些系統(tǒng)的行為理論上理解是重要的，如果它接近簡(jiǎn)單的目標(biāo)。

讓我們總結(jié)出這些觀點(diǎn)：

• 自動(dòng)化應(yīng)該很簡(jiǎn)單：它應(yīng)該在理論上很好地被了解，和在使用中可預(yù)期的。

• 自動(dòng)化也應(yīng)該提供反饋，以至于使用者能估定一種證明的嘗試為什么失敗。

• 一個(gè)甚至比較強(qiáng)烈的需求是，自動(dòng)化是可視的，在可視中通過(guò)證明的研究，能直接地檢查自動(dòng)化的執(zhí)行。

• 自動(dòng)化應(yīng)該是自然的，這是為了使證明器和使用者之間的概念差距最小化。舉例來(lái)說(shuō)，自動(dòng)化應(yīng)該在標(biāo)準(zhǔn)的邏輯系統(tǒng)中執(zhí)行，或者與使用者傳導(dǎo)證明的決策程度相一致。

• 時(shí)常，使用者對(duì)一個(gè)證明進(jìn)行優(yōu)化有很多的安全步驟。與自動(dòng)化在返回前至少做出改進(jìn)相比，自動(dòng)化簡(jiǎn)單的返回“可證明”與“不可證明”是沒(méi)什么用處的。

• 自動(dòng)化應(yīng)該是穩(wěn)定的，以至于在自動(dòng)化的行為中理論上微小的改變不會(huì)產(chǎn)生大的變化。這是很重要的，因?yàn)榻换ナ降淖C明包含大量隔行掃描使用者或自動(dòng)化步驟的環(huán)節(jié)。

• 自動(dòng)化也應(yīng)該是魯棒的，在意義上微小的變化不會(huì)影響自動(dòng)化的可證實(shí)性。

• 我們想要自動(dòng)化對(duì)明顯的理論是有效率的。

• 最后，我們想要自動(dòng)化是完全精密的。她能很好的定義問(wèn)題的層次。

 

3  目前交互式證明器的自動(dòng)化

目前交互式定理證明器的自動(dòng)化證明方法不符合先前環(huán)節(jié)的需求。

Isabelle/ HOL是目前作為被認(rèn)可的HOL執(zhí)行的代表。 主要被使用的技術(shù)是一個(gè)描述的證明器blast，和簡(jiǎn)化器simp。這些都混合在單個(gè)的自動(dòng)化策略里。 Isabelle也包括一個(gè)模式消除程序，它和blast使用起來(lái)有點(diǎn)相似。

Simp 被廣泛地使用，但是它并不是一個(gè)完全的一階證明方法。然而，它能滿足許多前期環(huán)節(jié)需求的事實(shí)解釋了為什么它這么流行，在交互式證明中。blast方法在肯定邏輯和組的簡(jiǎn)單問(wèn)題上運(yùn)行得很好，但是它很難了解它的特性是什么。它基于一個(gè)證明器leanTAP，那對(duì)一階邏輯是完全的。另一方面，下列的目標(biāo)稍微可證明在一階邏輯，但是blast不行。

f( g a)=a┝З y •g(f y)=y

它甚至更加的混亂，但它在區(qū)間 g a 實(shí)現(xiàn)的時(shí)候，這區(qū)間在結(jié)果本身中發(fā)生，并是存在的證明。更糟的是，當(dāng)像HOL 的類型邏輯被表達(dá)的時(shí)候，g a 是唯一的區(qū)間發(fā)生在可以使用的正確類型結(jié)果中。這一個(gè)失敗對(duì)于有效地處理等式邏輯是一個(gè)描述類型程序失敗的合并統(tǒng)一。因?yàn)樗�是這么的不受限制，所以自動(dòng)方法幾乎從不被用于交互式證明的中間。而且，它是不穩(wěn)定的，在它產(chǎn)生的子目標(biāo)中在對(duì)目標(biāo)的較小變化之下可能是野性地不同的，它的提出是無(wú)用的除了在緊緊地被控領(lǐng)域。

整合一個(gè)現(xiàn)代的解決證明器Vampire進(jìn)入Isabelle將沒(méi)有必要糾正這些錯(cuò)誤�；�于解決的方式提供了一點(diǎn)支持對(duì)于交互式理論證明器，因?yàn)樽泳湫问降臏p少意味著使用者有很少的可觀性進(jìn)入證明的搜尋，而且很少知道為什么一個(gè)特殊的輔助定理會(huì)失效。證明的搜尋是一個(gè)本地的向前的綜合的搜尋，與一個(gè)全球化的向后的綜合搜尋的典型描述介紹以及Isabelle的策略水平相反。因此，對(duì)于使用者，解決是一個(gè)不自然的系統(tǒng)。通常從這些系統(tǒng)來(lái)的反饋是極差的甚至不存在的。此外，許多步驟應(yīng)該被認(rèn)為是安全的 (應(yīng)用一個(gè)終端和聚合的改寫組，運(yùn)行一個(gè)∧ E 步驟) 因?yàn)橄到y(tǒng)被當(dāng)作一個(gè)黑盒子使用，或目標(biāo)率直地被解決，或者更通常，一點(diǎn)也不解決，而且系統(tǒng)包含的關(guān)于可靠應(yīng)用的步驟被丟失的信息，留給使用者可以手動(dòng)的應(yīng)用這些步驟。這里的問(wèn)題是系統(tǒng)無(wú)法做出改進(jìn)那些無(wú)法直接證明的目標(biāo)。

我們也作關(guān)于一階理論證明器的以下觀察。這些證明器被設(shè)計(jì)去尋找大量的數(shù)量詞實(shí)例，尋找可選擇地系數(shù)平等推論。然而在交互式定理證明器里的自動(dòng)化的失敗沒(méi)有失敗于猜測(cè)大量的數(shù)量詞實(shí)例。

 

4  技術(shù)

在下面這節(jié)，我們描述我們?nèi)绾谓�立自�?dòng)化。首先，我們正在嘗試尋找證明，所以我們將會(huì)需要 ( 至少) 證明的搜尋引擎。然后，我們?cè)诤艽蟮某潭壬显缸鲇檬謩?dòng)的方式的模型證明。除了證明的搜尋之外，在手動(dòng)證明中其他主要的利用方法是簡(jiǎn)單化。我們描述我們?cè)鯓佑懻摵?jiǎn)化器。

有條件的簡(jiǎn)單化是一種簡(jiǎn)單化的形式，它的簡(jiǎn)化器采用遞歸的方式企圖解決可能被應(yīng)用的當(dāng)前目標(biāo)的改寫選擇。我們討論正采用在這些目標(biāo)上的簡(jiǎn)化器沒(méi)有被最好的運(yùn)行，并建議替代選擇。

然后，當(dāng)使用簡(jiǎn)單化的時(shí)候，它是一個(gè)很好的方法去確定簡(jiǎn)單裝置是匯合的和終端的。我們描述完成的執(zhí)行。當(dāng)使用簡(jiǎn)單化的時(shí)候，然而，也想利用在改寫一個(gè)證明的過(guò)程中產(chǎn)生的假設(shè)。確定改寫規(guī)則的組仍然是聚合的和終止的，就應(yīng)該在證明搜尋時(shí)提供一些動(dòng)態(tài)完成的形式。我們討論我們?nèi)绾巫プ×诉@些議題。

 

4.1證明的搜尋

在這節(jié)中，我們描述我們證明搜尋的基本系統(tǒng)。這是一個(gè)單一的結(jié)論，對(duì)向后的證明搜尋是適當(dāng)?shù)闹庇^系統(tǒng)。我們避開(kāi)統(tǒng)一的流行的區(qū)間計(jì)算。這有一些有趣的結(jié)果當(dāng)混合證明搜尋時(shí)用其他的方法。注意我們只對(duì)自動(dòng)化的一階系統(tǒng)感興趣。

 

4.1.1邏輯系統(tǒng)

證明搜尋的二個(gè)主要系統(tǒng)是決議和描述。因?yàn)橐粋�(gè)交互式環(huán)境的自動(dòng)化，決議太不自然。因?yàn)檫@一原因，描述是更有希望的。我們因此限制我們的注意在基于描述的系統(tǒng)。描述系統(tǒng)典型地藉由否定目標(biāo)而且尋找矛盾著手進(jìn)行。我們甚至考慮到這是不自然的。我們因此集中在標(biāo)準(zhǔn)邏輯系統(tǒng)中直接執(zhí)行的描述系統(tǒng)。

使用這樣一個(gè)系統(tǒng)根據(jù)復(fù)雜的執(zhí)行有重要的意義，因?yàn)槲覀兡苤皇呛?jiǎn)單地在 HOL 目標(biāo)的水平搜尋使用或多或少標(biāo)準(zhǔn)的策略。這也對(duì)自然化有有利條件，因?yàn)槭褂谜咭呀?jīng)熟悉一個(gè)如此系統(tǒng)的證明和反饋，因此我們能直接地對(duì)使用者呈現(xiàn)失敗的部分，這些使用者沒(méi)有翻譯出來(lái)自一些其它可能的證明系統(tǒng)的結(jié)果。

單一結(jié)論系統(tǒng)對(duì)古典的證明是不適宜的，古典的證明被多樣結(jié)論系統(tǒng)更好的支援。然而多樣的結(jié)論系統(tǒng)是不自然的。如果我們對(duì)古典的證明感興趣，我們一定承認(rèn)我們的單一結(jié)論系統(tǒng)有缺點(diǎn)。另一方面，我們相信大規(guī)模的證明結(jié)構(gòu)大概是直觀的：我們典型地集中于一個(gè)目標(biāo)，并且我們的輔助定理服務(wù)作為證明中的中間觀點(diǎn)，和我們的補(bǔ)助定理如證明的中間點(diǎn)服務(wù)，即├A٨B→ C作為一個(gè)補(bǔ)助定理對(duì)├ ┑(A ٨ B ) ٧C不是典型地相等，因此我們期待在證明中達(dá)到一個(gè)點(diǎn)，這里A ٨ B 是可證明的，而不是去做一個(gè)可分的拆開(kāi)。確定地對(duì)于我們感興趣的領(lǐng)域，所有的證明本質(zhì)上是直觀的，以及古典的推論被限制到可能被簡(jiǎn)單化或其他的限制技術(shù)處理的小區(qū)域。

 

4.1.2引進(jìn)規(guī)則

我們希望做出更多的進(jìn)步。雖然程序簡(jiǎn)述說(shuō)明上方是完全的，它寧可是一邊的。既然大多數(shù)的證明大量利用輔助定理，對(duì)應(yīng)的目標(biāo)傳輸容易變成相當(dāng)擁擠。而且，當(dāng)引進(jìn)規(guī)定的時(shí)候，許多輔助定理自然地被瀏覽，也就是說(shuō)，趨于使用精煉的結(jié)論 C 而不愿使用從Г開(kāi)始向前連接著的結(jié)論。因?yàn)檫@些理由，我們也利用引進(jìn)規(guī)則à la Paulson[PNW03]。這些典型不安全，但是如果我們?cè)僖淮畏祷�，而且輪流其他的防備，完全性就能被保存。這些引進(jìn)規(guī)則能像輔助定理一樣被執(zhí)行，但是被作記號(hào)作為引進(jìn)規(guī)則。在證明的搜尋時(shí)候，這些輔助定理的結(jié)論被相配對(duì)抗當(dāng)前的目標(biāo)。如果結(jié)論與當(dāng)前的目標(biāo)相配，那么目標(biāo)將被選擇的引進(jìn)規(guī)則所代替，而且在事件中這些假定不能夠被證明，那么返回將被采用。如果一條引進(jìn)規(guī)則標(biāo)明是安全的，這時(shí)返回不發(fā)生。注意，這些提高沒(méi)有必要來(lái)自理論的觀點(diǎn)，而且它的唯一動(dòng)機(jī)是做模型自然形式的證明。

如果完全性以特定的方式被考慮，這時(shí)候能夠看見(jiàn)完全性的保存。如果這些規(guī)則是行為表現(xiàn)所預(yù)期的，則在簡(jiǎn)單化之前需要等式的統(tǒng)一。然而，目前我們用手動(dòng)的方式來(lái)模擬等式統(tǒng)一的使用。

完全性失敗對(duì)于引用規(guī)則：如果我們以一條規(guī)則作為一條引進(jìn)規(guī)則，這時(shí)我們無(wú)法是完全的? 不過(guò)這不是真實(shí)的，而且規(guī)則是安全的，在哪一情況我們都很順利，或不安全的，在哪一情況我們返回。需求的統(tǒng)一意味著我們能避免我們能避免作為增加的假設(shè)而使用的規(guī)則。然而，如果在一些階段我們能以規(guī)則作為一條引進(jìn)規(guī)則，這里有一個(gè)引進(jìn)規(guī)則被打算使用的環(huán)境，但是沒(méi)有連接鏈，然而當(dāng)一項(xiàng)額外的假定可能有時(shí)這里將沒(méi)有統(tǒng)一的問(wèn)題。

而且，自從我們沒(méi)有使用一個(gè)作為標(biāo)準(zhǔn)的輔助定理的規(guī)則，使用完全化的概念將不是很清楚。讓我們定義完全化的生產(chǎn)一個(gè)引進(jìn)規(guī)則去了解是否有一個(gè)證明作為一個(gè)輔助定理的規(guī)則。這時(shí)一個(gè)使用規(guī)則的證明作為一條引進(jìn)規(guī)則。在平等面前，我們應(yīng)該因此使用統(tǒng)一去確定我們的引進(jìn)規(guī)則能被無(wú)論在那里都可能應(yīng)用。既然在每個(gè)階段我們有一個(gè)有限的場(chǎng)地區(qū)間組，與一個(gè)終端和匯合的改寫次序，這樣一個(gè)方法能夠可以實(shí)行，即使在現(xiàn)階段我們只能用人工模擬這樣的步驟。

引進(jìn)規(guī)則的使用會(huì)帶來(lái)復(fù)雜化，因?yàn)橥耆�化是否適合不清楚。如果引進(jìn)規(guī)則能作為一個(gè)正常的輔助定理使用，這時(shí)完全化是可以保留的，因此輔助定理被操作就像它是個(gè)正常的肯定邏輯。在一條引進(jìn)規(guī)則后面的計(jì)劃是去平衡證明的搜尋，這會(huì)以別的方式主要地在左邊上操作。在規(guī)則├ A → B作為幾個(gè)輔助定理和作為一個(gè)引進(jìn)規(guī)則之間的差異，是自動(dòng)化能應(yīng)用→ L與一個(gè)作為輔助定理的規(guī)則相結(jié)合。因此作為一個(gè)引進(jìn)規(guī)則，我們期望目標(biāo)最終成為B和它能用A代替這些。

 

4.2 等式

4.2.1改寫

改寫是由用相等的子術(shù)語(yǔ)更換一個(gè)術(shù)語(yǔ)的變換過(guò)程。例如，我們可能使用輔助定理f (a) = a去改寫Q f (f (a)) 到 Q f (a)然后到Q (a)。在這節(jié)中，我們的各種改寫概念是非正式的。對(duì)于更多的信息讀者可以請(qǐng)教優(yōu)秀者。

在用辭上的一個(gè)注解：一個(gè)簡(jiǎn)單化的次序是一個(gè)改寫被限制的次序，過(guò)去一直用來(lái)證明一個(gè)區(qū)間改寫系統(tǒng)的終止。然而，“簡(jiǎn)單化”這個(gè)詞時(shí)常被非正式地用于提到改寫，而且“ 簡(jiǎn)化組”這個(gè)詞時(shí)常用來(lái)提及改寫的系統(tǒng)規(guī)則。我們下面采用這些非正式的用法。

兩個(gè)主要的簡(jiǎn)單化財(cái)富是終止和聚集。沒(méi)有聚集，了解簡(jiǎn)化器的行為就必須知道改寫被應(yīng)用的次序。這太多而不是使用者所期待的。在一個(gè)交互式環(huán)境中終止非常有用，例如，它允許反饋。而且，終止允許簡(jiǎn)單化與主要的證明的搜尋相整合。如果我們有聚集和終端，這時(shí)每一個(gè)區(qū)間有一個(gè)獨(dú)特正式形式，而且嘗試的等式變得可決定。這是一個(gè)極其有用的簡(jiǎn)化組的財(cái)富。

我們的基本策略是熱心地應(yīng)用簡(jiǎn)單化，在證明的搜尋每個(gè)步驟之后，使用假定去簡(jiǎn)化其他的假定和結(jié)論。我們用一個(gè)有終止和聚集的簡(jiǎn)化器工作。我們檢查終止和聚集的手動(dòng)使用完成。我們?cè)趥�(gè)體的類型中應(yīng)用簡(jiǎn)單化。如果簡(jiǎn)化組正在終止和聚合，這時(shí)它保存了證明搜尋的完全性。我們也在布爾類型應(yīng)用簡(jiǎn)單化，但它不是一階邏輯的一種可能性。例如，我們采用高階對(duì)微小范圍的數(shù)量詞改寫。不是太困難而無(wú)法爭(zhēng)論而這也保存證明的搜尋完全。經(jīng)常相似改寫的假定在證明期間出現(xiàn)，而且這些可能被簡(jiǎn)化組合并。給一項(xiàng)假定 x.P x和假定 P t，就可以簡(jiǎn)化 P t=，是再一次在布爾類型的簡(jiǎn)化，而不是一階的操作。我們不以這一種形式的假定作為改寫：我們的對(duì)數(shù)量詞示例的基本途徑經(jīng)由區(qū)間計(jì)算，而且使用這些簡(jiǎn)單化會(huì)破壞這方式的完全。我們使用假定形式x= y(可能數(shù)量化)來(lái)改寫。 為了保有聚集和終止，我們完成簡(jiǎn)化組的生產(chǎn)并動(dòng)態(tài)的產(chǎn)生改寫。因?yàn)橥瓿蓻](méi)被保證結(jié)束，完成被限制到一個(gè)步驟的確定數(shù)字，雖然在我們的應(yīng)用中，完成總是成功。

 

4.2.2條件的簡(jiǎn)單化

在這節(jié)中，我們描述有條件的簡(jiǎn)單化，并且注意到標(biāo)準(zhǔn)的途徑去解決遞歸環(huán)境下簡(jiǎn)化器的實(shí)施可能沒(méi)有被期待。我們建議一些其他的方法，而且討論其他的有條件的簡(jiǎn)單化的問(wèn)題。我們得出結(jié)論，目前有條件的簡(jiǎn)單化太復(fù)雜而無(wú)法作為 " 簡(jiǎn)單的 " 技術(shù)計(jì)算，并且的確太復(fù)雜而無(wú)法以一合理的方式與證明的搜尋相連接。我們建議考慮有條件的改寫就如平常的輔助定理的一樣的替代選擇。

簡(jiǎn)單化的工作在于對(duì)形式a = b的改寫，在目標(biāo)的任何地方改寫a到 b。有條件的簡(jiǎn)單化的工作在于對(duì)有條件的形式├A→a = b（A是一典型的連接）的改寫。在一個(gè)依次的Г├ C 中，如果我們能證明﹃C, Г的話，我們就能在目標(biāo)里調(diào)整a到b的改寫。

我們應(yīng)該如何嘗試去證明條件A? 假如我們正在用簡(jiǎn)單化連接一個(gè)完全的證明搜尋系統(tǒng)。在這情況下，非常好的 (從一個(gè)理論上的立場(chǎng)) 行為會(huì)被由需求獲得，如果A是可證明的，那么它實(shí)際上是被證明的。因?yàn)閷?duì)A的證明的搜尋是潛在的沒(méi)有終止的，我們這時(shí)應(yīng)該妥善地安排一個(gè)復(fù)雜的隔行掃描主要證明搜尋的過(guò)程，與子證明搜尋企圖去解決有條件的改寫情況。一個(gè)如此方式是不適口的不只因?yàn)樾�率的原因�?/span>

簡(jiǎn)單化的好處之一是，不像證明的搜尋，它正在終止。如果當(dāng)采用有條件的簡(jiǎn)單化的時(shí)候，我們希望保留這一終止的行為，當(dāng)企圖證明條件的時(shí)候，我們應(yīng)該遵行被涉及的非終止。一個(gè)我們應(yīng)該采用的主要證明搜尋是去證明條件，但是限制對(duì)特別深度的搜尋。這也是不適口的。為了在一個(gè)合理的時(shí)間里保持簡(jiǎn)單化的運(yùn)行，這深度應(yīng)當(dāng)非常小，因?yàn)闂l件的產(chǎn)生是很頻繁的。這些小的深度不能提供更多的條件解決辦法比其他簡(jiǎn)單的方法。對(duì)于一個(gè)小深度的有限制的證明搜尋，這也意味著它的理論限制也能成為實(shí)際的限制：任何的有限制的證明搜尋將會(huì)是不完全的，但是由于大的深度我們可以有希望的忽略這樣的不完全。小的深度意味著我們可能面臨的條件能被解決的條件，這條件對(duì)于使用者是很清晰的，不過(guò)被限制的搜尋深度意味著情況沒(méi)有被解決。根據(jù)我們的經(jīng)驗(yàn)，深度必須至少有10個(gè)邏輯的步驟 ( ∨ E 及其他。)，連接中間有效的等式推論(我們想像一個(gè)情節(jié)我們有一個(gè)有效地處理等式的證明搜尋)。在實(shí)驗(yàn)方面，根據(jù)簡(jiǎn)化器的反應(yīng)時(shí)間執(zhí)行這些方法變得不實(shí)際，在深度4之后。在將來(lái)，這些方法對(duì)于電腦將變得是可實(shí)行的，雖然目前它不能。

一個(gè)使用有限制的證明搜尋的替代選擇是為了解決從一個(gè)條件去確定一個(gè)可接受的條件類別，而且接受一些將會(huì)有可能是可證明的條件，但是它將會(huì)在外部被給的類別上失敗。明顯的選擇是提議的邏輯。然而，有條件的簡(jiǎn)單化的問(wèn)題擴(kuò)充多深入地超過(guò)偶然的失敗證明一種提議有效的條件，如同我們稍后討論一樣，所以這方式不能產(chǎn)生任何很大實(shí)際的效益，雖然行為會(huì)至少在理論上有好的理解。

被采用的 HOL ， HOL 啟發(fā)和 Isabelle 的目前方式，是在條件上激發(fā)簡(jiǎn)單器它自己。這些遞歸的召集是潛在的非終止 (有條件的簡(jiǎn)單化極端地傾向于成環(huán))，以至于被激發(fā)的遞歸簡(jiǎn)化器的時(shí)間是限制的。這些深度搜尋的限制當(dāng)解決條件遭受同樣的問(wèn)題，這些問(wèn)題在先前的段落被討論過(guò)的。方式在許多方面比上面的很差，因?yàn)轭~外的簡(jiǎn)單化所有物有必要了解它的行為，當(dāng)解決條件時(shí)，可能是不清晰的甚至在提議的條件上，讓單獨(dú)的情況來(lái)涉及述語(yǔ)。對(duì)于一個(gè)典型的目標(biāo)，我們只需要簡(jiǎn)單化能在一個(gè)簡(jiǎn)單了解的方法方面有進(jìn)步。對(duì)于條件，我們的需求通常是體檢可能的話，就被解決。簡(jiǎn)單化不是完全形式的證明，因此，我們希望，我們的情況將會(huì)是以致于那簡(jiǎn)單化能經(jīng)常很好地運(yùn)行。然而，簡(jiǎn)單化不能夠證明所有的前置詞條件以至于它的行為甚至在提議的水平是難了解的。在數(shù)量詞推論上，甚至在最基本的水平，失敗是基準(zhǔn)。

因此，當(dāng)求證條件時(shí)，目前的方法無(wú)法足夠地以非終止的問(wèn)題處理。而且條件的級(jí)別可被簡(jiǎn)單化解決的很難去描述，而且不是簡(jiǎn)單的適合使用者去理解。

 

4.2.3完成

完成是一個(gè)能確定簡(jiǎn)單組是聚合還是終止的程序。聚合與終止是我們要求簡(jiǎn)化組具備的兩個(gè)主要所有物，所以完成是當(dāng)采用簡(jiǎn)單化時(shí)一個(gè)有用的工具。我們討論我們的完成使用。

在群的公理理論上使用完成的標(biāo)準(zhǔn)例子，源自一組終止和聚合的改寫對(duì)于這一個(gè)理論構(gòu)成一個(gè)標(biāo)準(zhǔn)的改寫系統(tǒng)的規(guī)則，展示了完成是有力的技術(shù)。在我們的工作中，這樣的動(dòng)力是從不被需要。我們實(shí)現(xiàn)了我們發(fā)現(xiàn)的非常有用的基本完成。因?yàn)槲覀兊男枰�是被限制的，我們沒(méi)有實(shí)現(xiàn) Huet 的完全完成程序，雖然在不同的設(shè)定中這是令人想要的。我們放下這些是為了將來(lái)的工作。

我們的完成程序也允許有條件的完成。當(dāng)工作在一個(gè)鍵入設(shè)定的時(shí)候，時(shí)常希望在一個(gè)給定的類型中提及個(gè)體的一個(gè)子集。然后介紹一個(gè)述語(yǔ)的子類型，而且限制語(yǔ)句只談?wù)撟宇愋偷慕M成。

 

4.2.4動(dòng)態(tài)的完成

我們先前提到了它時(shí)常是一個(gè)希望以假定作為改寫的例子。清楚地說(shuō)，假定是動(dòng)態(tài)的并且在證明的程序中各處改變。雖然我們可能開(kāi)始就錯(cuò)在改寫的簡(jiǎn)單化規(guī)則的組，如果我們使用假定，它可能很好的作為我們的基本簡(jiǎn)化組，增大假定，不再是聚合和終止。如果我們?cè)副４嬉粋�(gè)正在共同聚合和終止的簡(jiǎn)化組的所有形式，這時(shí)我們?cè)谧C明的過(guò)程期間必須運(yùn)行一些完成形式。我們需要這樣的動(dòng)態(tài)完成，因?yàn)樗�一定能在證明的過(guò)程期間被很好地運(yùn)行。

不幸地是，完成是一個(gè)相當(dāng)昂貴的過(guò)程。而且，它大體上非終止的。然而，當(dāng)看到各種規(guī)則類型被使用的時(shí)候，典型地它們是一種非常簡(jiǎn)單的形式。舉例來(lái)說(shuō)，我們時(shí)常獲得與假定類似的a = b ∨ a = c，然后著手進(jìn)行一個(gè)可分的除去。 產(chǎn)生的目標(biāo)有假定a = b 和 a = c，我們?cè)缸鳛楹?jiǎn)單化的規(guī)則來(lái)使用它。多數(shù)的這些簡(jiǎn)單化規(guī)則是基礎(chǔ)的。在這情況下，完成被保證去結(jié)束，應(yīng)該有一個(gè)方法發(fā)生短路的完成程序去得到一個(gè)能更快速地運(yùn)行的相等程序。希望，如果我們能微小地減少完成的一條到另外一條規(guī)則的改寫，這時(shí)希望改寫程序相對(duì)地充分運(yùn)用( 當(dāng)然地，這是伊莎貝爾空想的簡(jiǎn)單化的情形，而且 HOL 光簡(jiǎn)單化也在某些程度上是充分運(yùn)用的) ，而且執(zhí)行將會(huì)是可接受的。

有一些文件覆蓋了基本區(qū)間的完成。我們看 [GNP +93]。這一個(gè)運(yùn)算法則帶來(lái)了一個(gè)基本的改寫規(guī)則組，而且在多項(xiàng)式產(chǎn)生一個(gè)減少的權(quán)威改寫系統(tǒng)的時(shí)間。不幸地是，雖然過(guò)程在多項(xiàng)式時(shí)間里操作，但是它利用合適的終止。合適的終止在HOL啟發(fā)或Isabelle 中沒(méi)有被執(zhí)行，而且在及時(shí)上可能有一個(gè)沒(méi)有充分運(yùn)用的版本相對(duì)緩慢是多項(xiàng)式的(即，雖然來(lái)自[ GNP+93] 的運(yùn)算法則是多項(xiàng)式的在及時(shí)上，這里會(huì)有一個(gè)比例的高常數(shù))。當(dāng)然，在證明期間做一個(gè)增加的變化給等式組，因此，在這某種程度希望有一點(diǎn)提高，但是我們?nèi)匀粦?yīng)該有能夠做更多的感覺(jué)。

看一下我們使用作為改寫的假定，它是清楚，超過(guò)基本的，他們甚至有比較簡(jiǎn)單的自然：沒(méi)有左手邊的子區(qū)間被用于任何其他的改寫規(guī)則(比如，假定a = b，全然沒(méi)有左手邊的一個(gè)適當(dāng)子區(qū)間，而且我們從沒(méi)有另一項(xiàng)假定形式a = d同時(shí)發(fā)生的情況)。在這個(gè)例子中，它足夠?yàn)榱艘�維持聚合和終止，用這一條規(guī)則改寫所有其他的簡(jiǎn)單化規(guī)則。如果我們需要在線完成這些沒(méi)有被滿足的條件，我們會(huì)依靠我們的 (被限制的時(shí)間) 完成程序，但是在我們的個(gè)案研究中這不發(fā)生。當(dāng)在基本完成的正確證明的上下文中考慮的時(shí)候，這一個(gè)結(jié)果是清晰的。然而，在我們的個(gè)案研究期間有若干的復(fù)雜情節(jié)，沒(méi)有這最佳化，導(dǎo)致我們的證明器花了特別久的時(shí)間。

 

4.2.5 方程式的統(tǒng)一

我們的最高水平的證明搜尋基于列舉區(qū)間上升到一個(gè)確定的區(qū)間深度。統(tǒng)一沒(méi)有出現(xiàn)在一個(gè)這樣的程序中。我們引用引進(jìn)規(guī)則à la Paulson進(jìn)入我們的搜尋程序。現(xiàn)在由相配對(duì)的引進(jìn)規(guī)則對(duì)抗現(xiàn)在的目標(biāo)規(guī)則的結(jié)論被簡(jiǎn)單的完成。

引進(jìn)規(guī)則像其他的輔助定理被對(duì)待，作為補(bǔ)充的假定它們合并的進(jìn)入結(jié)果。不過(guò)，他們作為引進(jìn)規(guī)則被作記號(hào)。我們用具體的例子說(shuō)明它們的從區(qū)間的列舉像其他輔助定理一樣。結(jié)論通過(guò)簡(jiǎn)化器被改寫。在證明搜尋的每個(gè)階段，我們檢查任何引進(jìn)規(guī)則的結(jié)論是否與目前的目標(biāo)相配，而且如果因此我們以引進(jìn)規(guī)則的條件替換目標(biāo)，返回不安全的引進(jìn)規(guī)定，這有模擬等式統(tǒng)一的效果。

 

5  連接與整合

在這節(jié)中我們描述在早先的章節(jié)中被簡(jiǎn)述的技術(shù)如何整合進(jìn)入一個(gè)單一戰(zhàn)略，和在這一個(gè)戰(zhàn)略和使用者之間的連接。

我們的自動(dòng)化包含一個(gè)描述的證明搜尋，藉由對(duì)固定的區(qū)間深度的數(shù)量詞實(shí)例化，以要求散布到簡(jiǎn)單化。這些應(yīng)該如何被整合? 如果簡(jiǎn)單化正在終止和聚集的，這時(shí)應(yīng)用在證明搜尋的每個(gè)步驟后的簡(jiǎn)單化的明顯策略保存完全。這是在這兩項(xiàng)技術(shù)整合后的必要觀察。

策略提供了一個(gè)連接給使用者。使用過(guò)程中使用者必須敘述一組終止和聚集的改寫規(guī)則和一組引進(jìn)規(guī)則的過(guò)程。事實(shí)上，使用者也敘述一組應(yīng)該在證明期間被考慮的輔助定理，而且這些只是被當(dāng)作先前描述與目標(biāo)陳述的合并。證明搜尋地進(jìn)行，與安全的規(guī)則和簡(jiǎn)單化熱心地應(yīng)用，以及在不安全規(guī)則上的返回。如果證明是不成功的，失敗部分被返回給使用者幾乎沒(méi)有安全規(guī)則，或簡(jiǎn)單化的步驟，可能被應(yīng)用。對(duì)我們的方式一個(gè)缺點(diǎn)是結(jié)果相當(dāng)大，因?yàn)槲覀冋�在特定的深度下面用所有�?/span>(類型-正確的) 區(qū)間例示數(shù)量詞。它將有一點(diǎn)適應(yīng)使用者的連接，以使這些實(shí)例化不直接地呈現(xiàn)給使用者，但是在要求上可視的。我們離開(kāi)這更進(jìn)一步工作。

 

6  評(píng)估

在這節(jié)中，我們討論我們的證明的過(guò)程怎樣相當(dāng)于根據(jù)在第2節(jié)中被簡(jiǎn)述的標(biāo)準(zhǔn)。我們?nèi)缓笥懻撏耆�的議題。我們沒(méi)有宣稱有一個(gè)正式的證明對(duì)完全產(chǎn)生一些問(wèn)題的類別，但是我們確實(shí)討論過(guò)程有好的所有物。我們通過(guò)設(shè)置我們的技術(shù)產(chǎn)生其他的就像分析一樣的理論證明技術(shù)。然后我們通過(guò)給出的成功例子評(píng)估實(shí)際的過(guò)程使用，而且描述過(guò)程的感覺(jué)。

 

6.1評(píng)估生產(chǎn)需求

我們的程序與在第2節(jié)提到的標(biāo)準(zhǔn)一起被設(shè)計(jì)。我們感到它滿足簡(jiǎn)單化的需求。在概念上，我們正在執(zhí)行一個(gè)標(biāo)準(zhǔn)直觀的證明搜尋。我們合并安全的和不安全的規(guī)則。我們?cè)谶壿嫷乃��?/span>(布爾類型)和領(lǐng)域的特性類型里使用簡(jiǎn)單化。我們的簡(jiǎn)單化規(guī)則應(yīng)該是聚集和終止的。當(dāng)改寫不破壞重要的所有物時(shí)候，我們確信任何的假定都可以使用。我們只有在限制的它們有很好的行為的例子中使用簡(jiǎn)單 化以及有條件的簡(jiǎn)單化規(guī)則。所有的這些觀念很容易理解的。

當(dāng)使用程序的時(shí)候，概念上的簡(jiǎn)單化導(dǎo)致簡(jiǎn)單化。我們應(yīng)當(dāng)確定我們的簡(jiǎn)化組，我們的引進(jìn)規(guī)則組，以及與目標(biāo)相關(guān)的輔助定理。策略在策略水平運(yùn)行，因此，我們能通過(guò)激發(fā)一次一步的策略步進(jìn)經(jīng)過(guò)一個(gè)失敗的證明嘗試。既然程序是非破壞力的( 在某種意義上我們直接地搜尋使用自然減除的規(guī)則，并非對(duì)正常的形式轉(zhuǎn)換)，我們有高水平的可視化進(jìn)入證明的搜尋。失敗部分典型地立刻被理解。安全步驟的觀念意謂，即使我們無(wú)法找到證明，我們回到使用者執(zhí)行得相當(dāng)多的我們?nèi)〉眠M(jìn)步的工作。不完全顯示它本身作為一個(gè)失敗去猜測(cè)大量的數(shù)量詞實(shí)例。隨著動(dòng)態(tài)完成的失敗，不完全也能在證明搜尋期間產(chǎn)生。

簡(jiǎn)單化導(dǎo)致了穩(wěn)定性。當(dāng)在它已經(jīng)成功之前，我們會(huì)稱的證明器是單調(diào)的，在那增加的輔助定理中，簡(jiǎn)單化的規(guī)則，或不安全的規(guī)則不會(huì)導(dǎo)致程序的失敗。同樣地證明器是魯棒的，即使對(duì)定義有微小的變化等等。我們不會(huì)宣稱程序是有效率的。

 

6.2完全

我們自動(dòng)化有一些不完全的來(lái)源。FOL 的可證明性大體上是無(wú)法決定的。我們對(duì)區(qū)間集合的子集深度限制。是否有一個(gè)證明僅僅涉及到深度限制區(qū)間是現(xiàn)在可決定的，但是我們將會(huì)不可避免地失敗于找到我們的限制子集之外包括區(qū)間放置的證明。這是一個(gè)不完全的來(lái)源。然而，我們可能連續(xù)地增加區(qū)間深度并且這樣來(lái)恢復(fù)對(duì)可決定性花費(fèi)的完全。

FOL 能在方程序的推論 [McK75] 中置入，所以期待等式推論表明對(duì)通常證明搜尋的類似問(wèn)題。我們的方式是限制我們自己對(duì)終止和聚集的改寫規(guī)則組。因此完成可能失敗，或不可能結(jié)束，這是一個(gè)不完全的來(lái)源。而且，我們采用動(dòng)態(tài)的完成，能同樣地失敗，雖然在實(shí)踐中這不是一個(gè)問(wèn)題。然而，完成能讓使用者大量的進(jìn)行交互式處理。如果使用者確定，改寫規(guī)則組是聚集和終止的，而且如果動(dòng)態(tài)的完成在證明搜尋期間總是成功的，這時(shí)我們的等式操作將會(huì)是完整的。

 

6.3 效率

目前自動(dòng)化方法的成功很大停留在統(tǒng)一上，然而我們只有稍微地使用統(tǒng)一，當(dāng)操作引進(jìn)規(guī)則時(shí)。根據(jù)證明的搜尋，根據(jù)執(zhí)行我們的程序?qū)��?huì)廣泛類似像吉爾曼這樣的前統(tǒng)一程序。舉例來(lái)說(shuō)，下列的目標(biāo)是可決定的：

( xyz.P x y →P y z →P x z)

→ ( xyz.Q x y → Q y z → Q x z)

→ ( xy.P x y→P y x)

→ ( xy.P x y ∨ Q x y)

→ ( xy.P x y) ∨ ( xy.Q x y)

的確，事實(shí)或一個(gè)公式的虛偽能在一個(gè)只有四種要素的模型中被評(píng)估。然而，即使這樣一個(gè)的目標(biāo)是可決定的，甚至于一些現(xiàn)代解決方法基于證明器的努力。不幸的是，我們的程序注定要花非常長(zhǎng)的時(shí)間。在防御中，這樣的目標(biāo)很少在交互式定理的證明中被碰到。如果他們被遇見(jiàn)，使用者當(dāng)然可以用一個(gè)交互式的決議證明器去解決他們。

除了基本的證明搜尋之外，我們對(duì)等式推論給予特別的關(guān)注。我們?cè)谕瓿缮蠈?duì)等式結(jié)束的方式，和在各種可變的條件是滿足的。然而，如果保持這些情況，達(dá)成平等的方式或許是有效的�，F(xiàn)代的決議證明器采用無(wú)窮盡的完成，推測(cè)的行為將不再比完成一個(gè)完全存在的改寫組有效率。

 

6.4實(shí)際應(yīng)用

因?yàn)樗�概念�?jiǎn)單，證明器是非常容易使用的。從一個(gè)定理到下一個(gè)定理的典型移動(dòng)，激發(fā)證明器關(guān)于簡(jiǎn)化組和預(yù)先輔助定理組的使用。如果證明沒(méi)有被建立，我們會(huì)見(jiàn)到失敗部分。這個(gè)部分通常是很容易理解的。幾乎總是(在我們的個(gè)案研究中，總是)需要增加一個(gè)簡(jiǎn)化規(guī)則，或一個(gè)不是不重要的輔助定理。如果輔助定理沒(méi)有已經(jīng)被證明就應(yīng)該取出并證明它。增加必要的規(guī)則，程序被重復(fù)執(zhí)行，通常是成功的。大體上說(shuō)，我們沒(méi)有修整簡(jiǎn)單化規(guī)則和輔助定理組到每個(gè)定理：這些規(guī)則被利用取決與上下文的內(nèi)容，而且總是一個(gè)良好的主意去使用它們?nèi)绻�可以的話。相�?duì)于這些，太多的規(guī)則能導(dǎo)致執(zhí)行能力的降低，但是通常它正工作在一個(gè)給定的理論中，這里輔助定理的數(shù)量相對(duì)地被限制。

有時(shí)候必須用一個(gè)巧妙的區(qū)間例示一個(gè)數(shù)量詞，但是這些是自然的困難的步驟。在使用者的手段(并非檢查一些失敗的部分的表現(xiàn))下步進(jìn)的經(jīng)過(guò)證明的能力是非常有用的，而且提供很好的可視化，如果一些東西沒(méi)有正確工作的話。

我們討論完全不是首要重要的，但是清楚地自動(dòng)化的目標(biāo)是協(xié)助使用者證明輔助定理。如果自動(dòng)化能直接證明輔助定理，我們將沒(méi)有抱怨的了。

在我們的個(gè)案研究中我們執(zhí)行許多證明。一個(gè)主要的結(jié)果包含超過(guò)250條交互式證明的手寫體。這些證明的手寫體不是最初的證明抄寫，所以自動(dòng)化可以可實(shí)現(xiàn)的再造它們。我們的自動(dòng)化能夠解決每一個(gè)輔助定理。 我們提供針對(duì)證明的一個(gè)區(qū)段的統(tǒng)計(jì)，它涉及輔助定理 theorem_3_ nes_Mup，對(duì)于其他輔助定理是代表性的。這些輔助定理依次有一個(gè)次補(bǔ)助定理theorem_3__Mup _3。在下面的列表中，我們記錄定理名稱，策略手寫體的組成沒(méi)有我們的自動(dòng)化，組成有我們的自動(dòng)化和花費(fèi)的時(shí)間。當(dāng)求證 theorem_3_nes_Mup時(shí)，次輔助定理 theorem_3_nes_Mup_3 被提供給自動(dòng)化。當(dāng)這個(gè)次輔助定理被省略，而且主要的輔助定理不需要theorem_3_nes_Mup協(xié)助的時(shí)候，我們也記錄發(fā)生的東西。這涉及了證明器在主要的輔助定理的證明期間的再次證明。在這情況下，一個(gè)證明被建立，雖然它需要花超過(guò)5 分鐘的時(shí)間。然而，我們相信，這是由于自動(dòng)化策略的無(wú)效率實(shí)行，而且我們想要在將來(lái)的工作中再實(shí)現(xiàn)它。這些補(bǔ)助定理對(duì)自動(dòng)化對(duì)個(gè)案研究的其他輔助定理的效果是有代表性的。而且，我們已經(jīng)在其他的領(lǐng)域中相對(duì)成功的應(yīng)用了這樣的技術(shù)。

即使執(zhí)行很差勁，調(diào)和這些證明程序以至于輔助定理能被證明是一個(gè)主要的完成。事實(shí)上我們可以用一個(gè)常用的方法提供程序有很好的理論所有的證據(jù)。              

定理名稱              策略行    自動(dòng)操作的策略行    自動(dòng)操作的時(shí)間/秒

theorem3_ nes_Mup _3      28             1                66

theorem3_ nes_ Mup       12             1                24

theorem3_ nes_Mup'       n/a            1                305

7  替代選擇

我們發(fā)展的自動(dòng)化被我們?cè)诎咐�研究中遇�?jiàn)的問(wèn)題所激發(fā)。然而，我們總是能夠完成我們的簡(jiǎn)化組的事實(shí)應(yīng)該是一件幸運(yùn)的事情。大體上我們能期待完成舉例失敗對(duì)于表達(dá)交換性的規(guī)則來(lái)說(shuō)，所以測(cè)試兩個(gè)區(qū)間經(jīng)過(guò)一個(gè)權(quán)威的改寫組的等式。這里有一些處理問(wèn)題的環(huán)境的方法，比如順序改寫交互式的規(guī)則的例子，但是我們想要這個(gè)機(jī)會(huì)考慮替代選擇一般的對(duì)等式處理的途徑。

到現(xiàn)在為止，我們的證明搜尋限制了被考慮的區(qū)間深度�？雌饋�(lái)似乎限制等式推論到一個(gè)共同的區(qū)間子集是很合理的，而且在這里面采用適合終止限制的子集。這些介紹是過(guò)程的不完全。

求證 s= t 使用等式需要的公理，大體上，是任意很大深度的區(qū)間。如果我們限制我們考慮的區(qū)間深度，我們的等式推論將會(huì)是不完全的。舉例來(lái)說(shuō)，假設(shè)我們通過(guò)轉(zhuǎn)移鏈s = u = v = x = y=t來(lái)證明一個(gè)等式s = t。這樣的一個(gè)證明被展示在圖1。如果我們限制我們考慮到 d 或更小的區(qū)間深度，圖可能與圖2相似。 在這個(gè)情況下，等式s= u= v 將會(huì)被獲得，但是等式x= y 和 y= t 將不會(huì)被獲得。 如果沒(méi)有 s= t 的證明存在與被限制的共同區(qū)間里，我們將會(huì)無(wú)法推論得到s=t。

因此在任何給出的我們證明搜尋的階段，我們的等式推論將會(huì)是不完全的。然而，如果我們連續(xù)地增加我們考慮的區(qū)間深度，我們將重新獲得等式推論的完全性。

在這一環(huán)境下，方程式的統(tǒng)一，生產(chǎn)被限制的區(qū)間組，變成可決定的，而且能非常有效率地實(shí)現(xiàn)。

這個(gè)方式的另一個(gè)優(yōu)點(diǎn)是給同等級(jí)別的代表能在一個(gè)使用者特別的習(xí)慣下被選擇。舉例來(lái)說(shuō)，使用者可能選擇同等類型的子句作為代表，或最小的產(chǎn)生一些詞典的路徑命令。這對(duì)使結(jié)果保持易讀有幫助。

這方式的另一個(gè)優(yōu)點(diǎn)是使用者的理解是簡(jiǎn)單的，而且我們?cè)谧C明搜尋的方法密合得很好。聚焦在單個(gè)復(fù)雜性上的衡量，比如區(qū)間深度，在一些程序之上，是一個(gè)統(tǒng)一的步驟。而且，缺點(diǎn)和方式的不完全經(jīng)由完成在這里是不存在的。我們留下這些替代選擇的執(zhí)行給將來(lái)的工作。

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

區(qū)間深度

 

 

 

 

s    u   v   x   y   t

 

區(qū)間

 

圖1: 傳遞性的等式證明

 

 

 

 

 

                               

d

 

 

區(qū)間深度

 

 

 

 

 

 

s     u     v     x    y     t

 

 區(qū)間

 

圖2: 有深度限制的傳遞性等式證明

                    

 

 

8 結(jié)論

我們已經(jīng)呈現(xiàn)我們發(fā)展去抓住一件大的個(gè)案研究的自動(dòng)化。自動(dòng)化被修整到交互式的使用，自動(dòng)化以一個(gè)證明搜尋引擎和簡(jiǎn)單化的整合為基礎(chǔ)，本質(zhì)上依賴于完成。

這節(jié)的貢獻(xiàn)是根據(jù)基本的證明搜尋，和它的簡(jiǎn)單化整合，在一個(gè)交互式假定里解說(shuō)目前自動(dòng)化的失敗。我們的技術(shù)沒(méi)有走出等式術(shù)語(yǔ)邏輯的范疇，不過(guò)甚至在這樣一個(gè)被限制領(lǐng)域，我們遇到了很多的問(wèn)題。另一方面，解決這些問(wèn)題，我們沒(méi)有對(duì)特殊自動(dòng)化領(lǐng)域的需求。我們不否認(rèn)，在線性算術(shù)區(qū)域中，這樣的程序?qū)τ行У淖詣?dòng)化是很有必要的。然而，我們的經(jīng)驗(yàn)表明簡(jiǎn)單化和證明的搜尋是一個(gè)非常有效的組合，這可能是邏輯現(xiàn)象一個(gè)例證 "從一點(diǎn)點(diǎn)開(kāi)始一個(gè)長(zhǎng)的方法"。

在先前的章節(jié)中我們提到一些將來(lái)工作的可能性，我們?cè)谶@里概述。

• 引進(jìn)規(guī)則的完全理論的議題應(yīng)該是被追求的，雖然這不可能有許多實(shí)際的影響。

• 在證明搜尋期間，怎樣合并輔助定理的議題是應(yīng)該追求的。克雷格的插入補(bǔ)助定理意味著以句法的特征為基礎(chǔ)的新奇方式在當(dāng)前目標(biāo)和一個(gè)輔助定理之間被分享：如果一個(gè)輔助定理和當(dāng)前目標(biāo)以不同的語(yǔ)言被表達(dá)，這時(shí)輔助定理為了要證明當(dāng)前目標(biāo)是沒(méi)有什么用的�？死赘竦牟迦胙a(bǔ)助定理為 FOL 支撐，但是把擴(kuò)充的主意到較富有的理論是有可能的。

• 完成可能被擴(kuò)充為完全的完成la Huet。有條件的完成也應(yīng)該被實(shí)現(xiàn)，以便它應(yīng)付通常的情形，而且支持理論應(yīng)該被發(fā)展。更遠(yuǎn)地說(shuō)，為了支持不同的等式概念，完成的執(zhí)行應(yīng)該被一個(gè)等式的概念參數(shù)化，這等式與HOL的嵌入的等式不同。一件額外的工作是整合好自動(dòng)的終止證明器，就像完成程序的 AProVE，所以使用者交互作用是最小化的。

• 自動(dòng)化的連接應(yīng)該被擴(kuò)充，以便使用者不會(huì)因太多的信息而忙得不可開(kāi)交。

• 自動(dòng)化整體上而言為了提高策略的效率，需要再實(shí)現(xiàn)。

• 我們企圖實(shí)行替代選擇的方法和證明的搜尋去處理經(jīng)由合適的關(guān)閉和連接等式

這包括將來(lái)的工作的產(chǎn)生作為這個(gè)工作的直接結(jié)果。我們現(xiàn)在考慮其他沒(méi)有被防備的機(jī)會(huì)。

雖然我們相信我們的方式很大地解決了一個(gè)被給定的輔助定理的證明問(wèn)題，但是輔助定理和定義的選擇主要是一個(gè)技巧的事情。在輔助定理的情況下，我們典型地在理論的邊界上累積它們，然后尋找一般的輔助定理，它包含了幾個(gè)這樣的例子。這些增強(qiáng)是歸納假定的增強(qiáng)的回憶。

我們也發(fā)現(xiàn)在一些領(lǐng)域中,在理論之間有一個(gè)在邊界上的非瑣細(xì)的輔助定理的爆發(fā)，這在推廣上無(wú)法被減少。這典型地普通數(shù)學(xué)對(duì)象的發(fā)生，就像一棵樹(shù)。許多輔助定理直觀上似乎合理的，但是它們的證明時(shí)常包括相當(dāng)多的努力。在這情況下，似乎很難控制子理論的傳播使其進(jìn)入主要的理論，因?yàn)樽永碚摰妮o助定理是如此的普遍被用于主要的理論之中。因此在這里我們有三個(gè)相關(guān)的問(wèn)題，即：

•來(lái)自一個(gè)子理論的重要而獨(dú)立的輔助定理的擴(kuò)展被請(qǐng)求。

•輔助定理的直觀似乎合理的，這很難去證明。

•輔助定理滲入主要理論,減少模組化和使主要的理論很重地依賴在子理論上。

 

這里似乎沒(méi)有方法減少在一些輔助定理里的爆發(fā)。根據(jù)證明，我們注意到困難從需要發(fā)生小心地說(shuō)歸納法補(bǔ)助定理，所以這主要地是歸納證明的一個(gè)自動(dòng)化的失敗。我們也注意在這一個(gè)區(qū)域中的大部份的定義暗示可運(yùn)行,以至于這里有一些模式檢查的形式范圍經(jīng)由定義的執(zhí)行。這依次能用來(lái)告誡一個(gè)歸納的證明器作為事實(shí)或不同的猜測(cè)輔助定理。

我們沒(méi)有提及自動(dòng)化的歸納法，或其他的更高階的功能。我們有更多要說(shuō)關(guān)于在章節(jié)？的介紹。但是能夠說(shuō)這可能像一個(gè)困難的領(lǐng)域。

我們也注意關(guān)于在策略混合的推論方面的困難。我們感覺(jué)到最近的提議朝向微積分學(xué)的策略可以證明是有趣的。我們建議相對(duì)瑣細(xì)的步驟, 就像確定策略手寫體是樹(shù)結(jié)構(gòu)而不是線性的結(jié)構(gòu), 而且在證明經(jīng)在ML水平的有束縛力的λ合并合適參數(shù)的處理。然而, 超過(guò)這個(gè)方法是不清楚的。

這里有很多相關(guān)的工作。自動(dòng)化的定理證明已經(jīng)是一個(gè)巨大的領(lǐng)域，而且我們不能夠希望在合理的空間中觀察它。我們的主要來(lái)源是兩冊(cè)自動(dòng)化推論 [RV01] 的手冊(cè)。我們注意到普遍的理論方法模式在可以執(zhí)行一些有疑問(wèn)的技術(shù)證明理論方法之上，我們的工作的目標(biāo)是在一個(gè)交互式環(huán)境中滿足自動(dòng)化的需要。相關(guān)的是哲學(xué)博士Syme[Sym98]，他滿足了在一個(gè)陳述的環(huán)境下自動(dòng)化的需要。許多的他的結(jié)論應(yīng)用在一個(gè)交談式環(huán)境。我們?cè)趯?duì)一個(gè)交互式環(huán)境的自動(dòng)化問(wèn)題的分析中運(yùn)用了他的工作。