Titre:
Induction as Deduction Modulo
Conférencier:
Dr. Claude Kirchner ,
LORIA & INRIA Nancy, France
Lieu:
Concordia University, Department of Electrical & Computer Engineering ,
Room H961-14
Date et heure:
lundi le 18 septembre 2000 de
10:00 à 00:00
Résumé: Proof by induction is a fundamental proof method in mathematics. Since the emergence of computer science, it has been studied and used as one of the fundamental concept that allows to build mathematical proofs in a mechanized way. In the rising era of proved software it plays a fundamental role in systems allowing to search for formal proofs. Therefore proofs by induction have a critical role in proof assistants and automated theorem provers. In proof assistants induction is viewed as a user guided inference rule while in automated theorem proving, it is viewed as an automatically applied computation rule, often via term rewriting. We will show in this talk how the two points of view can be understood in a unified way by using the general combination of deduction and computation called "deduction modulo". As a consequence, we offer a new understanding of the rewrite based induction methods, sometimes called "induction less induction