VAL@SAIL.STANFORD.EDU (Vladimir Lifschitz) (04/09/88)
AUTOMATED INDUCTIVE REASONING ABOUT LOGIC PROGRAMS Charles Elkan (elkan@iving.cs.cornell.edu) Department of Computer Science Cornell University Friday, April 1, 3:15pm MJH 252 David McAllester and I have developed a prototype theorem prover that applies induction in a new way to prove properties of logic programs. The soundness of the proof rules of our system follows directly from the standard minimal model semantics of logic programs. I shall describe the perspective on inductive theorem proving that gave rise to our system, and then its architecture and proof rules, using some varied examples of what it can prove. Then I shall raise for discussion various plans for future work, both theoretical and practical.