dale@linc.cis.upenn.edu.UUCP (01/20/87)
Penn Math/CS Logic Seminar 26 January Presenting Intuitive Deductions Frank Pfenning (pfenning@theory.cs.cmu.edu) Carnegie-Mellon University A deduction of a theorem may be viewed as an explanation why the theorem holds. Unfortunately the automated theorem proving community has concentrated almost exclusively on determining whether a proposed theorem is provable - the proofs themselves were secondary. We will explore how convincing explanations may be obtained from almost any kind of machine proof. This extends work by Dale Miller and Amy Felty (who present deductions in the sequent calculus) to a natural deduction system. Also, our deductions will generally not be normal, that is, they make use of lemmas which are so frequent in mathematical practice and everyday reasoning. We will also briefly discuss possible applications of the methods in the field which may be called "Inferential Programming". Math Seminar Room, 4th floor Math/Physics Building, 11:00am