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.
| Original language | English |
|---|---|
| Title of host publication | 26th International Conference on Rewriting Techniques and Applications (RTA 2015) |
| Editors | Maribel Fernandez |
| Publisher | Schloss Dagstuhl |
| Pages | 127-142 |
| Number of pages | 16 |
| ISBN (Electronic) | 9783939897859 |
| DOIs | |
| Publication status | Published - 17 Jun 2015 |
| Event | 26th International Conference on Rewriting Techniques and Applications, RTA 2015 - Warsaw, Poland Duration: 29 Jun 2015 → 1 Jul 2015 |
Publication series
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 36 |
| ISSN (Print) | 1868-8969 |
Conference
| Conference | 26th International Conference on Rewriting Techniques and Applications, RTA 2015 |
|---|---|
| Country/Territory | Poland |
| City | Warsaw |
| Period | 29/06/15 → 1/07/15 |
Keywords
- Deep inference
- Linear rules
- Proof theory
- Propositional logic
- Term rewriting
ASJC Scopus subject areas
- Software