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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01422611
Contributeur : Lutz Straßburger <>
Soumis le : lundi 26 décembre 2016 - 14:31:51
Dernière modification le : jeudi 10 mai 2018 - 02:06:07

Lien texte intégral

Identifiants

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

Citation

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〉

Partager

Métriques

Consultations de la notice

260