Abstract interpretation based semantics of sequent calculi

Abstract

In the field of logic languages, we try to reconcile the proof theoretic tradition, characterized by the concept of uniform proof, with the classic approach based on fixpoint semantics. Hence, we propose a treatment of sequent calculi similar in spirit to the treatment of Horn clauses in logic programming. We have three different semantic styles (operational, declarative, fixpoint) that agree on the set of all the proofs for a given calculus. Following the guideline of abstract interpretation, it is possible to define abstractions of the concrete semantics, which model well known observables such as correct answers or groundness. This should simplify the process of extending important results obtained in the case of positive logic programs to the new logic languages developed by proof theoretic methods. As an example of application, we present a top-down static analyzer for properties of groundness which works for full intuitionistic first order logic. © Springer-Verlag Berlin Heidelberg 2000.