Rewriting with linear inferences in propositional logic

A. Das

Research output: Chapter or section in a book/report/conference proceedingChapter or section

11 Citations (SciVal)


Linear inferences are sound implications of propositional logic where each variable appears exactly once in the premiss and conclusion. We consider a specific set of these inferences, MS, first studied by Straßburger, corresponding to the logical rules in deep inference proof theory. Despite previous results characterising the individual rules of MS, we show that there is no polynomialtime characterisation of MS, assuming that integers cannot be factorised in polynomial time. We also examine the length of rewrite paths in an extended system MSU that also has unit equations, utilising a notion dubbed trivialisation to reduce the case with units to the case without, amongst other observations on MS-rewriting and the set of linear inferences in general.
Original languageEnglish
Title of host publication24th International Conference on Rewriting Techniques and Applications (RTA 2013)
EditorsF. van Raamsdonk
Place of PublicationDagstuhl, Germany
PublisherLeibniz International Proceedings in Informatics
Number of pages16
ISBN (Print)9783939897538
Publication statusPublished - 14 Jun 2013

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs


Dive into the research topics of 'Rewriting with linear inferences in propositional logic'. Together they form a unique fingerprint.

Cite this