The use of a negation rule (the NAI rule) different from the classical negation as failure in the definition of the integrity checker is the major novelty of the first approach. It will allows us to correctly deal with goals of the form which typically occur during the query evaluation process.

The innovative aspect of the second approach is the idea of using both resolution and induction for reasoning about program properties. Such systems should be able to perform inductive proofs by making use of higher-order quantification. There have already been attempts to define second order theorem provers. The Boyer and Moore theorem prover, [7], (very used for proving properties of Lisp programs) is strongly based on induction and does not use resolution. It is an `interactive' theorem prover, where the user is constantly required to provide the system with the appropriate ``lemmas" that make it able to apply some inductive arguments.

We aim rather at defining a genuine higher order theorem prover by using a language which extends the traditional logic programming languages by replacing first-order terms with simply-typed -terms and first-order unification with higher order unification (the Huet higher order unification algorithm).

Thu Jun 20 09:47:49 BST 1996