Gentzen sequent calculi for some intuitionistic modal logics

Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

Elimination of network intrusions via a resource oriented BDI architecture

We propose a resource-oriented architecture of a rational agent for a network intrusion detection system. This architecture describes the behavior of a rational agent after detection of unwanted network activities. We describe the creation of countermeasures to ward off detected threats. Examples are created based on the proposed architecture, describing the process during a rational agent detection. We have described these examples by linear BDI logic behavioral formulæ, that have been proven by Gentzen sequent calculus.

Lower bounds to the size of constant-depth propositional proofs

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set of depth d sequents of total size O(n3+d) which are refutable in LK by depth d + 1 proof of size exp(O(log2n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets express a weaker form of the pigeonhole principle.

The deduction rule and linear and near-linear proof simulations

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof.A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by “nearly linear” is meant the ratio of proof lengths is O(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O(n . α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O(n log n).