Document Open Access Logo

No complete linear term rewriting system for propositional logic

Authors Anupam Das, Lutz Straßburger

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.127.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Anupam Das
Lutz Straßburger

Cite As Get BibTex

Anupam Das and Lutz Straßburger. No complete linear term rewriting system for propositional logic. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 127-142, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.127

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.

Subject Classification

Keywords
  • Linear rules
  • Term rewriting
  • Propositional logic
  • Proof theory
  • Deep inference

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Denis Bechet, Philippe de Groote, and Christian Retoré. A complete axiomatisation of the inclusion of series-parallel partial orders. In H. Common, editor, Rewriting Techniques and Applications, RTA 1997, volume 1232 of LNCS, pages 230-240. Springer, 1997. Google Scholar
  2. Kai Brünnler and Alwen F. Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors, LPAR 2001, volume 2250 of LNCS, pages 347-361. Springer, 2001. Google Scholar
  3. Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic, 10(2):1-34, 2009. Article 14. Google Scholar
  4. Michael Chein. Algorithmes d'écriture de fonctions booléennes croissantes en sommes et produits. Revue Française d’Informatique et de Recherche Opérationnelle, 1:97-105, 1967. Google Scholar
  5. Stephen Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC '71, pages 151-158, New York, NY, USA, 1971. ACM. Google Scholar
  6. Stephen Cook and Robert Reckhow. On the lengths of proofs in the propositional calculus (preliminary version). In Proceedings of the 6th annual ACM Symposium on Theory of Computing, pages 135-148. ACM Press, 1974. Google Scholar
  7. Yves Crama and Peter L Hammer. Boolean functions: Theory, algorithms, and applications. Cambridge University Press, 2011. Google Scholar
  8. Anupam Das. On the proof complexity of cut-free bounded deep inference. In K. Brünnler and G. Metcalfe, editors, Tableaux 2011, volume 6793 of LNAI, pages 134-148, 2011. Google Scholar
  9. Anupam Das. Rewriting with linear inferences in propositional logic. In Femke van Raamsdonk, editor, RTA'13, volume 21 of LIPIcs, pages 158-173, 2013. Google Scholar
  10. Nachum Dershowitz and Jieh Hsiang. Rewrite methods for clausal and non-clausal theorem proving. In Automata, Languages and Programming, pages 331-346. Springer, 1983. Google Scholar
  11. Moshe Dubiner and Uri Zwick. Amplification by read-once formulas. SIAM Journal on Computing, 26(1):15-38, 1997. Google Scholar
  12. A. Guglielmi and L. Straßburger. Non-commutativity and MELL in the calculus of structures. In L. Fribourg, editor, CSL 2001, volume 2142 of LNCS, pages 54-68, 2001. Google Scholar
  13. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1):1-64, 2007. Google Scholar
  14. V. A. Gurvich. Repetition-free boolean functions. Uspekhi Matematicheskikh Nauk, 32(1):183-184, 1977. Google Scholar
  15. V. A. Gurvich. On the normal form of positional games. In Soviet math. dokl, volume 25, pages 572-574, 1982. Google Scholar
  16. Rafi Heiman, Ilan Newman, and Avi Wigderson. On read-once threshold formulae and their randomized decision tree complexity. In Theoret. Comp. Science, pages 78-87, 1994. Google Scholar
  17. Lisa Hellerstein and Marek Karpinski. Computational complexity of learning read-once formulas over different bases. Technical report, University of Bonn, 1990. Google Scholar
  18. Jieh Hsiang. Refutational theorem proving using term-rewriting systems. Artificial Intelligence, 25(3):255-300, 1985. Google Scholar
  19. Aleksandr Vasilevich Kuznetsov. Non-repeating contact schemes and non-repeating superpositions of functions of algebra of logic. Trudy Matematicheskogo Instituta im. VA Steklova, 51:186-225, 1958. Google Scholar
  20. Leonid A. Levin. Universal sequential search problems. Problemy Peredachi Informatsii, 9(3):115-116, 1973. Google Scholar
  21. Rolf H. Möhring. Computationally tractable classes of ordered sets. In I. Rival, editor, Algorithms and Order, pages 105-194. Kluwer Acad. Publ., 1989. Google Scholar
  22. Christian Retoré. Réseaux et Séquents Ordonnés. PhD thesis, Université Paris VII, 1993. Google Scholar
  23. Lutz Straßburger. A characterisation of medial as rewriting rule. In Franz Baader, editor, RTA 2007, volume 4533 of LNCS, pages 344-358. Springer-Verlag, 2007. Google Scholar
  24. Lutz Straßburger. Extension without cut. Ann. Pure Appl. Logic, 163(12):1995-2007, 2012. Google Scholar
  25. Terese. Term rewriting systems. Cambridge University Press, 2003. Google Scholar
  26. L. G. Valiant. Short monotone formulae for the majority function. Journal of Algorithms, 5(3):363 - 366, 1984. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact