No complete linear term rewriting system for propositional logic

Anupam Das 1 Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : 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 sound and complete for the set of all such rewrite rules. We show in this paper that, as long as reduction steps are polynomial-time decidable, such a rewriting system does not exist unless coNP = NP. We draw tools and concepts from term rewriting, Boolean function theory and graph theory in order to access the 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 propositional logic. 1998 ACM Subject Classification F.4 Mathematical Logic and Formal Languages
Type de document :
Communication dans un congrès
26th International Conference on Rewriting Techniques and Applications (RTA 2015), Jun 2015, Warsaw, Poland. 26th International Conference on Rewriting Techniques and Applications (RTA 2015), 2015, 26th International Conference on Rewriting Techniques and Applications (RTA 2015). 〈http://drops.dagstuhl.de/opus/volltexte/2015/5193/〉. 〈10.4230/LIPIcs.RTA.2015.127〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01236948
Contributeur : Lutz Straßburger <>
Soumis le : mercredi 2 décembre 2015 - 13:59:48
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : samedi 29 avril 2017 - 00:20:04

Fichier

13.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Anupam Das, Lutz Straßburger. No complete linear term rewriting system for propositional logic. 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Jun 2015, Warsaw, Poland. 26th International Conference on Rewriting Techniques and Applications (RTA 2015), 2015, 26th International Conference on Rewriting Techniques and Applications (RTA 2015). 〈http://drops.dagstuhl.de/opus/volltexte/2015/5193/〉. 〈10.4230/LIPIcs.RTA.2015.127〉. 〈hal-01236948〉

Partager

Métriques

Consultations de la notice

134

Téléchargements de fichiers

42