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.

• Type: Journal
• Year: 2016
• Where: FOSSACS
• Authors: Clément Aubert, Marc Bagnol, Thomas Seiller
• Keywords: FOSSACS 2016, Software Engineering