On linear rewriting systems for Boolean logic and some applications to proof theory
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 thi...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2017-04-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2621/pdf |
| _version_ | 1797268614871515136 |
|---|---|
| author | Anupam Das Lutz Straßburger |
| author_facet | Anupam Das Lutz Straßburger |
| author_sort | Anupam Das |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:17Z |
| format | Article |
| id | doaj.art-2fdcd8809e30471b89df06d0ffd814b5 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:17Z |
| publishDate | 2017-04-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-2fdcd8809e30471b89df06d0ffd814b52024-03-08T09:45:41ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742017-04-01Volume 12, Issue 410.2168/LMCS-12(4:9)20162621On linear rewriting systems for Boolean logic and some applications to proof theoryAnupam Dashttps://orcid.org/0000-0002-0142-3676Lutz StraßburgerLinear 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.https://lmcs.episciences.org/2621/pdfcomputer science - logic in computer sciencef.4.1i.2.3 |
| spellingShingle | Anupam Das Lutz Straßburger On linear rewriting systems for Boolean logic and some applications to proof theory Logical Methods in Computer Science computer science - logic in computer science f.4.1 i.2.3 |
| title | On linear rewriting systems for Boolean logic and some applications to proof theory |
| title_full | On linear rewriting systems for Boolean logic and some applications to proof theory |
| title_fullStr | On linear rewriting systems for Boolean logic and some applications to proof theory |
| title_full_unstemmed | On linear rewriting systems for Boolean logic and some applications to proof theory |
| title_short | On linear rewriting systems for Boolean logic and some applications to proof theory |
| title_sort | on linear rewriting systems for boolean logic and some applications to proof theory |
| topic | computer science - logic in computer science f.4.1 i.2.3 |
| url | https://lmcs.episciences.org/2621/pdf |
| work_keys_str_mv | AT anupamdas onlinearrewritingsystemsforbooleanlogicandsomeapplicationstoprooftheory AT lutzstraßburger onlinearrewritingsystemsforbooleanlogicandsomeapplicationstoprooftheory |