Logic Programming Revisited

15 pagesThe so famous Prolog paradigm is based on the refutation of a goal, i.e. inferring the empty clause by means of the resolution principle. Switching to sequent calculus, this reduces to a cut-free proof search of the empty formula using the program clauses and the negation of the goal as hypotheses. It has already been applied to full Linear Logic. In this survey, we switch from sequent calculus to graph computation by means of bipolar modules. We explain in which extent the use of such structures in the framework of Linear Logic helps to enlarge logic programming towards a distributed backward and forward computation paradigm