Unary resolution: Characterizing PTIME

Clément Aubert, Marc Bagnol, Thomas Seiller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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.

Original languageEnglish (US)
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, Proceedings
EditorsChristof Löding, Bart Jacobs
PublisherSpringer Verlag
Pages373-389
Number of pages17
ISBN (Print)9783662496299
DOIs
StatePublished - Jan 1 2016
Event19th 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 - Eindhoven, Netherlands
Duration: Apr 2 2016Apr 8 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9634
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other19th 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
CountryNetherlands
CityEindhoven
Period4/2/164/8/16

Fingerprint

Unary
Rewriting
Logic Programs
Polynomial time
Polynomials
Pushdown Automata
Cut-elimination
Linear Logic
Logic programming
Semiring
Term
Soundness
Logic Programming
Algebraic Structure
Completeness
Encoding
Query
Restriction
First-order
Geometry

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Aubert, C., Bagnol, M., & Seiller, T. (2016). Unary resolution: Characterizing PTIME. In C. Löding, & B. Jacobs (Eds.), 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 (pp. 373-389). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634). Springer Verlag. https://doi.org/10.1007/978-3-662-49630-5_22

Unary resolution : Characterizing PTIME. / Aubert, Clément; Bagnol, Marc; Seiller, Thomas.

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. ed. / Christof Löding; Bart Jacobs. Springer Verlag, 2016. p. 373-389 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Aubert, C, Bagnol, M & Seiller, T 2016, Unary resolution: Characterizing PTIME. in C Löding & B Jacobs (eds), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9634, Springer Verlag, pp. 373-389, 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, Eindhoven, Netherlands, 4/2/16. https://doi.org/10.1007/978-3-662-49630-5_22
Aubert C, Bagnol M, Seiller T. Unary resolution: Characterizing PTIME. In Löding C, Jacobs B, editors, 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. Springer Verlag. 2016. p. 373-389. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-49630-5_22
Aubert, Clément ; Bagnol, Marc ; Seiller, Thomas. / Unary resolution : Characterizing PTIME. 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. editor / Christof Löding ; Bart Jacobs. Springer Verlag, 2016. pp. 373-389 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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",
year = "2016",
month = "1",
day = "1",
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",

}

TY - GEN

T1 - Unary resolution

T2 - Characterizing PTIME

AU - Aubert, Clément

AU - Bagnol, Marc

AU - Seiller, Thomas

PY - 2016/1/1

Y1 - 2016/1/1

N2 - 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.

AB - 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.

KW - Geometry of interaction

KW - Implicit complexity

KW - Logic programming

KW - Memoization

KW - Proof theory

KW - Pushdown automata

KW - Saturation

KW - Unary queries

UR - http://www.scopus.com/inward/record.url?scp=84961752375&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84961752375&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-49630-5_22

DO - 10.1007/978-3-662-49630-5_22

M3 - Conference contribution

AN - SCOPUS:84961752375

SN - 9783662496299

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 373

EP - 389

BT - 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

A2 - Löding, Christof

A2 - Jacobs, Bart

PB - Springer Verlag

ER -