This paper introduces a logical system, called BV , which extends multiplicative linear logic by a non-commutative self-dual logical operator. This extension is particularly challe...
System BV is an extension of multiplicative linear logic (MLL) with the rules mix, nullary mix, and a self-dual, non-commutative logical operator, called seq. While the rules mix ...
Density elimination by substitutions is introduced as a uniform method for removing applications of the Takeuti-Titani density rule from proofs in firstorder hypersequent calculi....
We propose a setting in which the search for a proof of B or a refutation of B (a proof of ¬B) can be carried out simultaneously: this is in contrast to the usual approach in aut...
We introduce the calculus of structures: it is more general than the sequent calculus and it allows for cut elimination and the subformula property. We show a simple extension of m...