IANDC
2010
13 years 8 months ago
2010
The Curry-Howard correspondence connects derivations in natural deduction with the lambdacalculus. Predicates are types, derivations are terms. This supports reasoning from assump...
AML
1998
13 years 11 months ago
1998
A natural deduction system NDIL described here admits normalization and has subformula prop
JUCS
2007
13 years 11 months ago
2007
: This paper introduces the notion of pedagogical natural deduction systems, which are natural deduction systems with the following additional constraint: all hypotheses made in a ...
IGPL
2007
13 years 11 months ago
2007
Pandora is a tool for supporting the learning of first order natural deduction. It includes a help window, an interactive context sensitive tutorial known as the ‘‘e-tutor’â...
JAPLL
2006
13 years 11 months ago
2006
Hybrid logics are a principled generalization of both modal logics and description logics, a standard formalism for knowledge representation. In this paper we give the first const...
APAL
2008
13 years 11 months ago
2008
This paper proves strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. By them, this paper...
CADE
2008
Springer
14 years 1 months ago
2008
Springer
It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a va...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent...
CSL
2003
Springer
14 years 4 months ago
2003
Springer
System SKS is a set of rules for classical propositional logic presented in the calculus of structures. Like sequent systems and unlike natural deduction systems, it has an explici...
CSL
2005
Springer
14 years 5 months ago
2005
Springer
We give a Natural Deduction formulation of an adaptation of G¨odel’s functional (Dialectica) interpretation to the extraction of (more) efficient programs from (classical) proof...