A Search-Based Approach to Induction Automation in Dependently
Typed Proof Assistants
-----------------------------------
          
ABSTRACT
-----------------------------------
Proof assistants such as Coq, Isabelle/HOL, or Simplify, are
used increasingly to discharge proof obligations produced by
program verifiers, such as Krakatoa. One important obstacle in
the complete automation of this process is the fact that many
proof obligations, especially those that encode data structure
properties, require inductive proofs, which are notoriously hard
to automate. In this talk, we present a novel approach for automating
inductive proofs in dependent type-based proof assistants. Our
approach uses search-based techniques to generate a proof tree.
This tree can be seen as a term in a dependently typed lambda
calculus and, in accordance with the Curry-Howard isomorphism,
can be subjected to atype-checking procedure to decide the validity
of the proof. Standard search optimization techniques, such as
backward and forward learning, can be applied to make the proof
process more efficient.
          
SPEAKER(S)
-----------------------------------
dr. Razvan VOICU
National University of Singapore
Singapore
-----------------------------------
Dr. Razvan Voicu is a lecturer in the Computer Science Department
of the National University of Singapore. His research interests
are in program verification and automated theorem proving.
URL http://www.comp.nus.edu.sg/~razvan
-----------------------------------