JAR
2010
13 years 10 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 12 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
14 years 4 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...