JAR
2010
13 years 2 months ago
2010
Abstract. We present a declarative language inspired by the pseudonatural language used in Matita for the explanation of proof terms. We show how to compile the language to proof t...
JAR
2002
13 years 4 months ago
2002
We formalise natural deduction for first-order logic in the proof assistant Coq, using De Bruijn indices for variable binding. The main judgement we model is of the form d [:] , ...
TPHOL
2000
IEEE
13 years 8 months ago
2000
IEEE
Abstract. This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and re...