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).