6 citations · 9 across the 6 of their papers we have counts for
6 papers
Unification and Logarithmic Space
Clément Aubert, Marc Bagnol
We present an algebraic characterization of the complexity classes Logspace and Nlogspace, using an algebra with a composition law based on unification. This new bridge between uni…
Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees
Marc Bagnol
Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics,…
Memoization for Unary Logic Programming: Characterizing PTIME
Clément Aubert, Marc Bagnol, Thomas Seiller
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 pr…
MALL proof equivalence is Logspace-complete, via binary decision diagrams
Marc Bagnol
Proof equivalence in a logic is the problem of deciding whether two proofs are equivalent modulo a set of permutation of rules that reflects the commutative conversions of its cut-…
Logic Programming and Logarithmic Space
Clément Aubert, Marc Bagnol, Paolo Pistone +1
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 characterizat…
Unification and Logarithmic Space
Clément Aubert, Marc Bagnol
We present an algebraic characterization of the complexity classes Logspace and NLogspace, using an algebra with a composition law based on unification. This new bridge between uni…