Unary resolution: characterizing PTIME

Clément Aubert; Marc Bagnol; Thomas Seiller

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

Unary resolution: characterizing PTIME

Clément Aubert, Marc Bagnol, Thomas Seiller^*

^*Corresponding author af dette arbejde

Datalogisk Institut

3 Citationer (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.

Originalsprog	Engelsk
Titel	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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings
Redaktører	Bart Jacobs, Christof Löding
Antal sider	17
Forlag	Springer
Publikationsdato	2016
Sider	373-389
DOI	https://doi.org/10.1007/978-3-662-49630-5_22
Status	Udgivet - 2016
Begivenhed	19th International Conference on Foundations of Software Science and Computation Structures - Eindhoven, Holland Varighed: 2 apr. 2016 → 8 apr. 2016 Konferencens nummer: 19

Konference

Konference	19th International Conference on Foundations of Software Science and Computation Structures
Nummer	19
Land/Område	Holland
By	Eindhoven
Periode	02/04/2016 → 08/04/2016

Navn	Lecture notes in computer science
Vol/bind	9634
ISSN	0302-9743

Adgang til dokumentet

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

Andre filer og links

Link to publication in Scopus

Citationsformater

Aubert, C., Bagnol, M., & Seiller, T. (2016). Unary resolution: characterizing PTIME. I B. Jacobs, & C. Löding (red.), 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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings (s. 373-389). Springer. Lecture notes in computer science Bind 9634 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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. red. / Bart Jacobs; Christof Löding. Springer, 2016. s. 373-389 (Lecture notes in computer science, Bind 9634).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Aubert, C, Bagnol, M & Seiller, T 2016, Unary resolution: characterizing PTIME. i B Jacobs & C Löding (red), 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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. Springer, Lecture notes in computer science, bind 9634, s. 373-389, 19th International Conference on Foundations of Software Science and Computation Structures, Eindhoven, Holland, 02/04/2016. https://doi.org/10.1007/978-3-662-49630-5_22

Aubert C, Bagnol M, Seiller T. Unary resolution: characterizing PTIME. I Jacobs B, Löding C, red., 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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. Springer. 2016. s. 373-389. (Lecture notes in computer science, Bind 9634). doi: 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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. red. / Bart Jacobs ; Christof Löding. Springer, 2016. s. 373-389 (Lecture notes in computer science, Bind 9634).

@inproceedings{753859cc86cd4eb2a0f46b4303751ecb,

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",

doi = "10.1007/978-3-662-49630-5_22",

language = "English",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "373--389",

editor = "Bart Jacobs and Christof L{\"o}ding",

booktitle = "Foundations of Software Science and Computation Structures",

note = "19th International Conference on Foundations of Software Science and Computation Structures ; Conference date: 02-04-2016 Through 08-04-2016",

}

TY - GEN

T1 - Unary resolution

T2 - 19th International Conference on Foundations of Software Science and Computation Structures

AU - Aubert, Clément

AU - Bagnol, Marc

AU - Seiller, Thomas

N1 - Conference code: 19

PY - 2016

Y1 - 2016

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

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

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

M3 - Article in proceedings

AN - SCOPUS:84961752375

T3 - Lecture notes in computer science

SP - 373

EP - 389

BT - Foundations of Software Science and Computation Structures

A2 - Jacobs, Bart

A2 - Löding, Christof

PB - Springer

Y2 - 2 April 2016 through 8 April 2016

ER -

Unary resolution: characterizing PTIME

Abstract

Konference

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater