Paper Info
Title
Combining interactive and automatic reasoning in first order theories of functional programs
Abstract
We propose a new approach to the computer-assisted verification of functional programs. We work in first order theories of functional programs which are obtained by extending Aczel's first order theory of combinatory formal arithmetic with positive inductive and coinductive predicates. Rather than building a special purpose system we implement our theories in Agda, a proof assistant for dependent type theory which can be used as a generic theorem prover. Agda provides support for interactive reasoning by encoding first order theories using the formulae-as-types principle. Further support is provided by off-the-shelf automatic theorem provers for first order logic which can be called by a program which translates Agda representations of first order formulae into the TPTP language understood by the provers. We show some examples where we combine interactive and automatic reasoning, covering both proof by induction and coinduction.
Year
DOI
Venue
2012
10.1007/978-3-642-28729-9_7
FoSSaCS
Keywords
Field
DocType
generic theorem prover,dependent type theory,interactive reasoning,functional program,order theory,agda representation,off-the-shelf automatic theorem provers,automatic reasoning,order logic,order formula
Discrete mathematics,Programming language,Computer science,Automated theorem proving,Order theory,Mathematical induction,Type theory,Coinduction,First-order logic,Agda,Proof assistant
Conference
Volume
ISSN
Citations 
7213
0302-9743
3
PageRank 
References 
Authors
0.40
19
3
Name
Order
Citations
PageRank
Ana Bove119814.43
Peter Dybjer254076.99
Andrés Sicard-Ramírez360.78