Skip to Main content Skip to Navigation
Journal articles

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

Anupam Das 1, 2 Lutz Straßburger 3
2 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
3 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Complete list of metadata
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Monday, December 26, 2016 - 2:31:51 PM
Last modification on : Thursday, January 20, 2022 - 5:31:51 PM

Links full text


  • HAL Id : hal-01422611, version 1
  • ARXIV : 1610.08772


Anupam Das, Lutz Straßburger. On linear rewriting systems for Boolean logic and some applications to proof theory. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016. ⟨hal-01422611⟩



Les métriques sont temporairement indisponibles