Standard
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. ed. / Bart Jacobs; Christof Löding. Springer, 2016. p. 373-389 (Lecture notes in computer science, Vol. 9634).
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
Aubert, C, Bagnol, M & Seiller, T 2016,
Unary resolution: characterizing PTIME. in B Jacobs & C Löding (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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. Springer, Lecture notes in computer science, vol. 9634, pp. 373-389, 19th International Conference on Foundations of Software Science and Computation Structures, Eindhoven, Netherlands,
02/04/2016.
https://doi.org/10.1007/978-3-662-49630-5_22APA
Aubert, C., Bagnol, M., & Seiller, T. (2016).
Unary resolution: characterizing PTIME. In B. Jacobs, & C. Löding (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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings (pp. 373-389). Springer. Lecture notes in computer science Vol. 9634
https://doi.org/10.1007/978-3-662-49630-5_22Vancouver
Aubert C, Bagnol M, Seiller T.
Unary resolution: characterizing PTIME. In Jacobs B, Löding C, 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, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. Springer. 2016. p. 373-389. (Lecture notes in computer science, Vol. 9634).
https://doi.org/10.1007/978-3-662-49630-5_22Author
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. editor / Bart Jacobs ; Christof Löding. Springer, 2016. pp. 373-389 (Lecture notes in computer science, Vol. 9634).
Bibtex
@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",
address = "Switzerland",
note = "null ; Conference date: 02-04-2016 Through 08-04-2016",
}
RIS
TY - GEN
T1 - Unary resolution
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 -
