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

Anupam Das, Lutz Strassburger

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)
100 Downloads (Pure)


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 systems consisting only of linear inferences. Our main result is that the length of any 'nontrivial' derivation in such a system is bound by a polynomial. As a consequence there is no polynomial-time decidable sound and complete system of linear inferences, unless coNP = NP. We draw tools and concepts from term rewriting, Boolean function theory and graph theory in order to access some required intermediate results. At the same time we make several connections between these areas that, to our knowledge, have not yet been presented and constitute a rich theoretical framework for reasoning about linear TRSs for Boolean logic.

Original languageEnglish
Article number9
Pages (from-to)1-27
Number of pages27
JournalLogical Methods in Computer Science
Issue number4
Early online date28 Dec 2016
Publication statusPublished - 27 Apr 2017

Bibliographical note

Special Issue: Selected papers of the joint 26th International Conference on "Rewriting Techniques and Applications" and 13th International Conference on "Typed Lambda Calculi and Applications" RTA/TLCA 2015


  • Boolean logic
  • Linear rewriting
  • Proof theory

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'On linear rewriting systems for Boolean logic and some applications to proof theory'. Together they form a unique fingerprint.

Cite this