BSL
1999
13 years 11 months ago
1999
We consider a classical (propositional) version, CBI, of O'Hearn and Pym's logic of bunched implications (BI) from a model- and prooftheoretic perspective. We present a c...
CSL
2002
Springer
13 years 11 months ago
2002
Springer
Abstract. We show that Gentzen's sequent calculus admits generalization of semi-terms of particularly simple form. This theorem extends one of the main results in [BS95] to la...
MSCS
2006
13 years 11 months ago
2006
We define a sequent calculus corresponding to the logic of strongly compact closed categories with biproducts. Based on this calculus, we define a proof-net syntax with ly normali...
ENTCS
2008
13 years 11 months ago
2008
Deep inference is a proof theoretical methodology that generalizes the traditional notion of inference in the sequent calculus: in contrast to the sequent calculus, the deductive ...
ENTCS
2008
13 years 11 months ago
2008
The interactive theorem prover developed in the KeY project, which implements a sequent calculus for JavaCard Dynamic Logic (JavaCardDL) is based on taclets. Taclets are lightweig...
APAL
2008
13 years 11 months ago
2008
Abstract. We provide an alternative proof of the sequentialisation theorem for proof nets of multiplicative linear logic. Namely, we show how a proof net can be transformed into a ...
CSL
2010
Springer
14 years 18 days ago
2010
Springer
We investigate a modification of the sequent calculus which s a first-order proof into its abstract deductive structure and a unifier which renders this structure a valid proof. We...
IJCAI
1993
14 years 25 days ago
1993
SEQUEL is a new-generation functional programming language, which allows the specification of types in a notation based on the sequent calculus. The sequent calculus notation suff...
AIML
2008
14 years 29 days ago
2008
abstract. We investigate an alternative presentation of classical and positive modal logic where the coalgebraic cover modality is taken as primitive. For each logic, we present a ...
FLOPS
2008
Springer
14 years 1 months ago
2008
Springer
In this paper, we present an extension of the scheme HH(C) (Hereditary Harrop formulas with Constraints) with a suitable formulation of negation in order to obtain a constraint ded...