We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory. We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.
CITATION STYLE
Aubert, C., Bagnol, M., Pistone, P., & Seiller, T. (2014). Logic programming and logarithmic space. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8858, pp. 39–57). Springer Verlag. https://doi.org/10.1007/978-3-319-12736-1_3
Mendeley helps you to discover research relevant for your work.