@inproceedings{70b5aa62dfd344c7815325a520312e40,
title = "Unary resolution: Characterizing PTIME",
abstract = "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.",
keywords = "Geometry of interaction, Implicit complexity, Logic programming, Memoization, Proof theory, Pushdown automata, Saturation, Unary queries",
author = "Cl{\'e}ment Aubert and Marc Bagnol and Thomas Seiller",
note = "Funding Information: This work was partly supported by the ANR-14-CE25-0005 Elica , the ANR-11-INSE-0007 Rever , the ANR-10-BLAN-0213 Logoi, the ANR-11-BS02-0010 Recr{\'e} , the ANR 12 JS02 006 01 project Coquas and the European Union{\textquoteright}s Marie Sk{\l}odowska-Curie Individual Fellowship (H2020-MSCA-IF-2014) 659920 - ReACT. Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2016.; 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",
year = "2016",
doi = "10.1007/978-3-662-49630-5_22",
language = "English (US)",
isbn = "9783662496299",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "373--389",
editor = "Christof L{\"o}ding and Bart Jacobs",
booktitle = "Foundations 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, Proceedings",
}