Unary Resolution: Characterizing Ptime

4 years 3 months ago
Unary Resolution: Characterizing Ptime
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), a construction stemming from an interactive interpretation of the cut-elimination procedure of linear logic known as the geometry of interaction. We restrict this framework to terms (logic programs, rewriting rules) using only unary symbols and prove the restriction complete for polynomial time computation using an encoding of pushdown automata. Soundness w.r.t. Ptime is proven thanks to a saturation method close the one used for pushdown systems and inspired by the memoization technique. As a direct consequence, we get a Ptime-completeness result for a class of logic programming queries that uses only unary function symbols.
Clément Aubert, Marc Bagnol, Thomas Seiller
Related Content
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Authors Clément Aubert, Marc Bagnol, Thomas Seiller
Comments (0)