Search

• < Previous
• 1
• Next >

---

On Nested Sequents for Constructive Modal Logics

Lutz Strassburger ; Anupam Das ; Ryuta Arisaka.

We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our&nbsp;[&hellip;]

---

On the relative proof complexity of deep inference via atomic flows

Anupam Das.

We consider the proof complexity of the minimal complete fragment, KS, of standard deep inference systems for propositional logic. To examine the size of proofs we employ atomic flows, diagrams that trace structural changes through a proof but ignore logical information. As results we obtain a&nbsp;[&hellip;]

---

On linear rewriting systems for Boolean logic and some applications to proof theory

Anupam Das ; Lutz Straßburger.

Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-)linear rewrite rule. In&nbsp;[&hellip;]

---

On the logical complexity of cyclic arithmetic

Anupam Das.

We study the logical complexity of proofs in cyclic arithmetic ($\mathsf{CA}$), as introduced in Simpson '17, in terms of quantifier alternations of formulae occurring. Writing $C\Sigma_n$ for (the logical consequences of) cyclic proofs containing only $\Sigma_n$ formulae, our main result is that&nbsp;[&hellip;]

---

A Functional (Monadic) Second-Order Theory of Infinite Trees

Anupam Das ; Colin Riba.

This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability ("Rabin's Tree Theorem") is one of the most powerful known results concerning the decidability of logics. By a complete axiomatization&nbsp;[&hellip;]

---

Enumerating Independent Linear Inferences

Anupam Das ; Alex Rice.

A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for&nbsp;[&hellip;]

---