Published in

Springer Verlag, Lecture Notes in Computer Science, p. 39-57

DOI: 10.1007/978-3-319-12736-1_3



Export citation

Search in Google Scholar

Logic Programming and Logarithmic Space

Proceedings article published in 2014 by Clément Aubert ORCID, Marc Bagnol, Paolo Pistone, Thomas Seiller ORCID
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO


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 multi-head finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.