Auto in agda programming proof search using reflection

Wen Kokke, Wouter Swierstra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

Original languageEnglish
Title of host publicationMathematics of Program Construction
Subtitle of host publication12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings
EditorsJanis Voigtländer, Ralf Hinze
Number of pages26
ISBN (Electronic)9783319197968
Publication statusAccepted/In press - 16 Mar 2015
Externally publishedYes
Event12th International Conference on Mathematics of Program Construction - Konigswinter, Germany
Duration: 29 Jun 20151 Jul 2015
Conference number: 12

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th International Conference on Mathematics of Program Construction
Abbreviated titleMPC 2015
Internet address


Dive into the research topics of 'Auto in agda programming proof search using reflection'. Together they form a unique fingerprint.

Cite this