Automated theorem proving in a simple meta-logic for LF
- 1 January 1998
- book chapter
- Published by Springer Nature
- p. 286-300
- https://doi.org/10.1007/bfb0054266
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Rules of definitional reflectionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Unification and anti-unification in the calculus of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A logic for reasoning with higher-order abstract syntaxPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automated theorem proving in a simple meta-logic for LFPublished by Springer Nature ,1998
- Pi: An interactive derivation editor for the calculus of partial inductive definitionsPublished by Springer Nature ,1994
- A framework for defining logicsJournal of the ACM, 1993
- An algorithm for testing conversion in type theoryPublished by Cambridge University Press (CUP) ,1991