Published in

Springer Verlag, Lecture Notes in Computer Science, p. 373-389

DOI: 10.1007/978-3-662-49630-5_22



Export citation

Search in Google Scholar

Unary Resolution: Characterizing Ptime

Book chapter published in 2016 by Clément Aubert ORCID, Marc Bagnol, Thomas Seiller ORCID
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO


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 saturation method 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.