Abstract
We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution (following [10]) into which proofs of Elementary Linear Logic can be interpreted. In order to extend geometry of interaction computation (the so called execution formula) to a wider class of programs in the algebra than just those coming from proofs, we define a variant of execution (called weak execution). Its application to any program of clauses is shown to terminate with a bound on the number of steps which is elementary in the size of the program. We establish that weak execution coincides with standard execution on programs coming from proofs.
