HOL

HOL is a general theorem proving system developed at the University of Cambridge [11,3] that is based on Church's theory of simple types, or higher-order logic [5]. Although Church developed higher-order logic as a foundation for mathematics, it can be used for reasoning about computational systems of all kinds. Similar to predicate logic in allowing quantification over variables, higher-order logic also allows quantification over predicates and functions, thus permitting more general systems to be described.

Watson also has a relationship to Church's simple theory of types: its logic can be obtained by using polymorphism to collapse a subset of Church's type system.

Like Watson, HOL is not a fully automated theorem prover but is more than simply a proof checker, falling somewhere between these two extremes. HOL has several features that contribute to its use as a verification environment:

1.

Several built-in theories, including booleans, individuals, numbers, products, sums, lists, and trees. These theories build on the five axioms that form the basis of higher-order logic to derive a large number of theorems that follow from them. In Watson, these theories could be built-in for efficiency purposes, however to date we have not chosen to do that. Watson does provide some basic primitive operations for booleans and natural numbers, with additional types being considered.

2.

Rules of inference for higher-order logic. These rules contain not only the eight basic rules of inference from higher-order logic, but also a large body of derived inference rules that allow proofs to proceed using larger steps. The HOL system has rules that implement the standard introduction and elimination rules for Predicate Calculus as well as specialized rules for rewriting terms. This is similar to some of the built-in rules in Watson used for equational reasoning. The difference in the approach of the two systems permits a natural use of deduction in HOL with extra support required for rewriting. In Watson the converse is true with deduction requiring the additional machinery and rewriting being the natural extension.

3.

A large collection of tactics. Examples of tactics include REWRITE_TAC which rewrites a goal according to some previously proven theorem or definition, GEN_TAC which removes unnecessary universally quantified variables from the front of terms, and EQ_TAC which says that to show two things are equivalent, we should show that they imply each other. In Watson, tactics are not ML scripts or operations on the basic theory objects but are represented as equational theorems containing unexecuted applications of theorems (possibly recursive) as discussed earlier.

More than one implementation of propositional and predicate logic is provided in Watson: there is an implementation of Gries's equational system, a sort of "tableau" approach using the case-definition machinery (the style which students typically learn) and recently an implementation of sequent proofs and a goal-directed natural deduction prover implemented as an interactive tactic using the INPUT command. In addition there is a library that provides an automatic tautology checker.

The "native" style of Watson reasoning heavily emphasizes rewriting and relies on deductive power for reasoning by cases with considerable use of reasoning by contradiction. Other styles have been utilized and tactics can be written that support a more deductive approach.

None of these approaches are as sophisticated yet as the HOL proof package but there is no reason to believe that they cannot be upgraded to this level; this is a matter of system maturity. There has been some effort to implement ``HOL tactics'' in Watson.

4.

A proof management system that keeps track of the state of an interactive proof session. The basic HOL system is similar to that of Watson. In addition Watson keeps track of theorem and axiom usage in a manner that permits automatic invalidation of theorems proven using axioms that have been invalidated.

5.

A metalanguage, ML, for programming and extending the theorem prover. Using the metalanguage, tactics can be put together to form more powerful tactics, new tactics can be written, and theorems can be aggregated to form new theories for later use. The metalanguage makes the verification system extremely flexible. Watson is also based on ML, but prefers to utilize its internal language to specify tactics as well as theorems. Watson is also based on ML, but prefers to utilize its internal language to specify tactics as well as the proof scripts for theorems. This may make it easier for users to learn to program in Watson, though the style of programming is unusual. In our experience, development of complex tactics is difficult regardless of the language used. It is our belief that using the same language for proof scripts, specifications, theorems and tactics may simplify the tactic development effort. However, at this time we have no empirical evidence to support this claim.

In general, the core HOL and Watson systems are similar in capabilities and support environment but are developed from a different approach. In HOL, theorem specification and manipulation are based on propositions. A theorem is specified as a predicate that has been reduced to true using the proof structure of HOL. In Watson, all theorems are equations. Although it is trivial to transform predicates into equations and back, the underlying approach used in the system plays a direct role on proof developments. An equational prover, such as Watson, allows the user to specify theorems in a more natural form, X = Y. This leads to a potentially different proof structure. In the HOL system, the user who wishes to prove that X=Y must specify this at the outset and then reduce this to true. In Watson, the user may follow this same approach, resulting the in theorem (X=Y)=true or alternatively they may start with X(Y) and reduce the term to Y(X). The flexibility allows a more general approach to proof development, permitting the use of whichever technique is more appropriate to the specific theorem under development.