eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-06-24
158
173
10.4230/LIPIcs.RTA.2013.158
article
Rewriting with Linear Inferences in Propositional Logic
Das, Anupam
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 polynomial-time 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol021-rta2013/LIPIcs.RTA.2013.158/LIPIcs.RTA.2013.158.pdf
proof theory
propositional logic
complexity of proofs
deep inference