Experience with mathematical content areas

The Watson prover has been used to develop theories of propositional and predicate logic in several styles. An equational style (as exemplified in [12]) is most natural, and theories implementing the propositional and predicate logic chapters of [12] in detail exist. We have also implemented a sequent calculus and a goal driven natural deduction prover. A tableau approach to first-order logic has natural relationships with Watson's built-in logic of case expressions, and a tableau approach to propositional logic has been used to develop a complete tautology checker as a tactic. A goal-directed natural deduction prover has been implemented as an interactive tactic using the INPUT command.

Watson's notation for propositional logic presents no difficulties. Experience leads us to believe that users can readily adapt to the somewhat nonstandard notation for quantifiers. There are few problems with the stratification functions of the prover as long as the boolean type has been declared as strongly cantorian and the propositional connectives and quantifiers made scin or scout as appropriate.

The prover has been used to develop theories of basic arithmetic and algebra needed for the projected computer science applications. Watson readily supports algebraic reasoning; its case expression machinery allows a natural way to handle exceptions to algebraic rules (such as those occasioned by the need to avoid division by zero) which are usually ignored by computer algebra systems, making the typical CAS logically unsound. We have also shown that Watson is a practical environment for carrying out proofs by induction in a development of Peano arithmetic. A theory of program semantics based on [6] is under construction. A student has recently completed a master's project involving the verification of published proofs of security properties of communication protocols using Watson.

For example, students working on this project have been able to develop the following theory files (this list is not exhaustive):

Sets:

Sets are defined as abstractions from boolean terms (predicates), and set membership as a specialization of function application. A library of elementary theorems has been developed covering the topics of set membership, equivalence, complements, unions, intersections, differences, subsets, proper subsets, and disjoint sets. On a more purely mathematical note, the designer used the student work described above in a proof of the Schröder-Bernstein theorem.

NatOrder:

A theory file related to the order properties of natural numbers (requiring proofs by induction).

Bit Values:

A theory file that contains definitions and theorems to assist in the mapping between compositions of Boolean values (bit strings) and natural numbers to be used in hardware circuit specification and verification.

Gates:

A theory of basic gates, including and, or, xor, inv, nand, nor and multiplexors. This also includes a theory covering boolean algebra for the basic logic gates. Specifically this file focuses on the composition and comparison of basic gates including associativity and symmetry laws as well as De Morgan laws for the gates.

Protocols:

With help from the authors, a student has developed a theory of protocol specifications and verification based on the CAPSL specification language [1] and the SvO logic [26]. An interesting aspect of this project was that it required the implementation of a modal logic (of belief) under Watson, which proved possible despite the designer's doubts.

Program Semantics:

The designer and a student have been collaborating on a file which implements a theory of program semantics in the style promoted by Dijkstra and Gries, following [6]. This file has involved extensive use of the higher-order features of the prover, since reasoning about complex function types is involved.

The designer has developed a theory of synthetic combinatory logic, with a variety of different abstraction and reduction tactics, which he hopes to use as a research tool in collaboration with a specialist in this area. The fact that the prover is good for this application area is not surprising, as the development of the control structures of the tactic language was largely driven by the now abandoned attempt to use a synthetic combinatory logic rather than a $\lambda$-calculus as the logic of the prover.