The main outcome we expect from this research is the definition of the theoretical foundations and the implementation of a theorem prover for logic programs, which uses both resolution and induction for proving declarative program properties. To this aim, we will need to involve higher-order logic. The success of this enterprise would be an argument against the convincement, which most of the recent theorem proving researchers agree with, that the demand for human interaction, illustrated by the Boyer and Moore prover, is inevitable.
On the other hand, staying in the realm of first-order logic, we pursue the formalization of a method which extends some resolution-based integrity checking mechanisms for proving logic program properties. As a byproduct, we could reveal some interesting correspondences between the various forms of loop detection and induction principles.
All these results should be documented by papers on the theory and the design of our theorem provers and reports of their implementation and testing.