License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.158
URN: urn:nbn:de:0030-drops-40609
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4060/
Go to the corresponding LIPIcs Volume Portal

Das, Anupam

Rewriting with Linear Inferences in Propositional Logic

pdf-format:
13.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{das:LIPIcs:2013:4060,
  author =	{Anupam Das},
  title =	{{Rewriting with Linear Inferences in Propositional Logic}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{158--173},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4060},
  URN =		{urn:nbn:de:0030-drops-40609},
  doi =		{10.4230/LIPIcs.RTA.2013.158},
  annote =	{Keywords: proof theory, propositional logic, complexity of proofs, deep inference}
}

Keywords: proof theory, propositional logic, complexity of proofs, deep inference
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI