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.