A Tool for Automated Theorem Proving in Agda
- 1 January 2006
- conference paper
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 154-169
- https://doi.org/10.1007/11617990_10
Abstract
No abstract availableThis publication has 7 references indexed in Scilit:
- Connecting a Logical Framework to a First-Order Logic ProverLecture Notes in Computer Science, 2005
- Higher-Order Unification and MatchingPublished by Elsevier BV ,2001
- Classical Type TheoryPublished by Elsevier BV ,2001
- Optimized encodings of fragments of type theory in first-order logicJournal of Logic and Computation, 1998
- Automated theorem proving in a simple meta-logic for LFLecture Notes in Computer Science, 1998
- A Complete Proof Synthesis Method for the Cube of Type SystemsJournal of Logic and Computation, 1993
- Inductive sets and families in Martin-Löf's type theory and their set-theoretic semanticsPublished by Cambridge University Press (CUP) ,1991