Unary resolution: characterizing PTIME

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

  • Clément Aubert
  • Marc Bagnol
  • Thomas Seiller

We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring, whose elements can be understood as logic programs or sets of rewriting rules over first-order terms. This construction stems from an interactive interpretation of the cut-elimination procedure of linear logic known as the geometry of interaction . This framework is restricted to terms (logic programs, rewriting rules) using only unary symbols, and this restriction is shown to be complete for polynomial time computation by encoding pushdown automata. Soundness w.r.t. Ptime is proven thanks to a saturationmethod similar to the one used for pushdown systems and inspired by the memoization technique. A Ptime-completeness result for a class of logic programming queries that uses only unary function symbols comes as a direct consequence.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures : 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings
EditorsBart Jacobs, Christof Löding
Number of pages17
PublisherSpringer
Publication date2016
Pages373-389
DOIs
Publication statusPublished - 2016
Event19th International Conference on Foundations of Software Science and Computation Structures - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016
Conference number: 19

Conference

Conference19th International Conference on Foundations of Software Science and Computation Structures
Nummer19
LandNetherlands
ByEindhoven
Periode02/04/201608/04/2016
SeriesLecture notes in computer science
Volume9634
ISSN0302-9743

    Research areas

  • Geometry of interaction, Implicit complexity, Logic programming, Memoization, Proof theory, Pushdown automata, Saturation, Unary queries

ID: 167553667