Sciweavers

Share
IANDC
2010
121views more  IANDC 2010»
8 years 18 days ago
Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
The Curry-Howard correspondence connects derivations in natural deduction with the lambdacalculus. Predicates are types, derivations are terms. This supports reasoning from assump...
Murdoch James Gabbay, Dominic P. Mulligan
AML
1998
93views more  AML 1998»
8 years 2 months ago
Normal deduction in the intuitionistic linear logic
A natural deduction system NDIL described here admits normalization and has subformula prop
Grigori Mints
JUCS
2007
102views more  JUCS 2007»
8 years 3 months ago
Pedagogical Natural Deduction Systems: the Propositional Case
: 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 ...
Loïc Colson, David Michel
IGPL
2007
113views more  IGPL 2007»
8 years 3 months ago
Pandora: A Reasoning Toolbox using Natural Deduction Style
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’...
Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, Ale...
JAPLL
2006
112views more  JAPLL 2006»
8 years 3 months ago
Intuitionistic hybrid logic
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...
Torben Braüner, Valeria de Paiva
APAL
2008
78views more  APAL 2008»
8 years 3 months ago
Strong normalization of classical natural deduction with disjunctions
This paper proves strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. By them, this paper...
Koji Nakazawa, Makoto Tatsuta
CADE
2008
Springer
8 years 5 months ago
Focusing in Linear Meta-logic
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...
Vivek Nigam, Dale Miller
CSL
2006
Springer
8 years 7 months ago
A Sequent Calculus for Type Theory
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...
Stéphane Lengrand, Roy Dyckhoff, James McKi...
CSL
2003
Springer
8 years 8 months ago
Atomic Cut Elimination for classical Logic
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...
Kai Brünnler
CSL
2005
Springer
8 years 8 months ago
Light Functional Interpretation
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...
Mircea-Dan Hernest
books