**Speaker:**
Marco Bozzano, DISI, Univ. di Genova
**Title:**
A Bottom-up Semantics for LO

**Abstract.**
The operational semantics of linear logic programming languages is
usually given in terms of goal-driven sequent calculi.
The proof-theoretic presentation is the natural counterpart
of the top-down semantics of traditional logic programs.
In this talk we present the theoretical foundation of an alternative
operational semantics based on a bottom-up evaluation of linear
logic programs via a fixpoint operator. The bottom-up fixpoint semantics
is important in applications
like active databases, and, more in general, for program analysis
and verification, and it has been extensively studied in classical logic
programming contexts. As a first case-study, we consider Andreoli and
Pareschi's LO enriched with the constant 1.
We give an algorithm to compute a single application of the
fixpoint operator where constraints are used to represent
in a finite way possibly infinite sets of provable goals, and
we show that in the case of propositional LO without 1 the semantics
is finitely computable.
We discuss applications and related work. Among these, we present the
relations between LO and disjunctive logic programming.
DLP fixpoint semantics can be viewed as an abstraction of our semantics
for LO.
We prove that the resulting abstraction is correct and complete
for an interesting class of LO programs encoding Petri-nets.