A logical calculus for controlled monotonicity

In this paper we introduce a new deductive framework for analyzing processes displaying a kind of controlled monotonicity. In particular, we prove the cut-elimination theorem for a calculus involving series-parallel structures over partial orders which is built up from multi-level sequents, an interesting variant of Gentzen-style sequents. More broadly, our purpose is to provide a general, syntactical tool for grasping the combinatorics of non-monotonic processes.     

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.     

Bunched sequential information

It is known that the logic BI of bunched implications is a logic of resources. Many studies have reported on the applications of BI to computer science. In this paper, an extension BIS of BI by adding a sequence modal operator is introduced and studied in order to formalize more fine-grained resource-sensitive reasoning. By the sequence modal operator of BIS, we can appropriately express “sequential information” in resource-sensitive reasoning. A Gentzen-type sequent calculus SBIS for BIS is introduced, and the cut-elimination and decidability theorems for SBIS are proved. An extension of the Grothendieck topological semantics for BI is introduced for BIS, and the completeness theorem with respect to this semantics is proved. The cut-elimination, decidability and completeness theorems for SBIS and BIS are proved using some theorems for embedding BIS into BI.