Anupam Das ; Lutz Straßburger - On linear rewriting systems for Boolean logic and some applications to proof theory

lmcs:2621 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 4 -
On linear rewriting systems for Boolean logic and some applications to proof theoryArticle

Authors: Anupam Das ORCID; 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 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.

    Volume: Volume 12, Issue 4
    Published on: April 27, 2017
    Accepted on: December 28, 2016
    Submitted on: May 5, 2016
    Keywords: Computer Science - Logic in Computer Science,F.4.1,I.2.3

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1480 times.
    This article's PDF has been downloaded 708 times.