Rewriting theory

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

Anupam Das and Lutz Straßburger. Logical Methods in Computer Science. Special issue of selected papers from RTA and TLCA '15. DOI arXiv PDF

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 this paper we study properties of …

No complete linear term rewriting system for propositional logic

Anupam Das and Lutz Straßburger. In proceedings of RTA '15. DOI PDF

Recently it has been observed that the set of all sound linear inference rules in propositional logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-) linear rewrite rule. This raises the question of whether there is a rewriting system on linear terms of propositional logic that is …

On the relative proof complexity of deep inference via atomic flows

Anupam Das. Logical Methods in Computer Science. Special issue of selected papers of the Turing Centenary Conference: CiE 2012. DOI arXiv PDF

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 polynomial simulation of versions of Resolution, along with some …

The complexity of propositional proofs in deep inference

Anupam Das. PhD thesis. Supervised by Alessio Guglielmi and John Power, University of Bath. PDF

Deep inference is a relatively recent proof methodology whose systems differ from traditional systems by allowing inference rules to operate on any connective appearing in a formula, rather than just the main connective. Its distinguishing feature, from a structural proof theoretic point of view, is that its systems are local : inference steps can be …

Rewriting with linear inferences in propositional logic

Anupam Das. In proceedings of RTA '13. DOI PDF

Linear inferences are sound implications of propositional logic where each variable appears exactly once in the premiss and conclusion. We consider a specific set of these inferences, MS, first studied by Straßburger, corresponding to the logical rules in deep inference proof theory. Despite previous results characterising the individual rules of MS, we show that there …