• Patrick Cousot and Radhia Cousot.
  Abstract Interpretation of Resolution-Based Semantics.
  Worshop on Logic and energy: A visionary inspirator. A tribute to Giorgio Levi for forty years of research, Pisa, Italy. October 23^rd, 2009.
• Abstract:
       We extend the abstract interpretation point of view on context-free grammars by Cousot and Cousot to resolution-based logic programs and proof systems.
       Starting from a transition-based small-step operational semantics of Prolog programs (akin to the Warren Machine), we consider maximal finite derivations for the transition system from most general goals.
       This semantics is abstracted by instantiation to terms and furthermore to ground terms, following the so-called c- and s-semantics approach.
       Orthogonally, these sets of derivations can be abstracted to SLD-trees, call patterns and models, as well as interpreters providing effective implementations (such as Prolog). These semantics can be presented in bottom-up fixpoint form.
       This abstract interpretation-based construction leads to classical bottom-up semantics (such as the s-semantics of computed answers, the c-semantics of correct answers of Keith Clark, and the minimal-model semantics of logical consequences of Maarten van Emden and Robert Kowalski).
       The approach is general and can be applied to infinite and top-down semantics in a straightforward way.

• Keywords:
  Bottom-up semantics; Herbrand semantics; Logic programming; s-semantics.
• Slides of the 30 mn presentation: .pdf (13.1 MB) to be used with Acrobat Reader.
• The corresponding paper is published in TCS 410(46):4724—4746, 2009
• Bibliographic reference:

  \bibitem{Cousot-Giorgio-Levi-2009-10-23}
  P.~Cousot and R.~Cousot.
  \newblock Abstract interpretation of resolution-based semantics.
  \newblock Workshop on \emph{Logic and energy: A visionary inspirator. A tribute 
            to Giorgio Levi for forty years of researc}, Pisa, Italy.
            October 23${^\mathrm{rd}}$ 2009.
  
  @inProceedings{Cousot-Giorgio-Levi-2009-10-23
     author =    {Cousot, P{.} and Cousot, R{.}},
     title =     {Abstract Interpretation of Resolution-Based Semantics},
     booktitle = {Workshop on Logic and energy: A visionary inspirator. 
                  A tribute to Giorgio Levi for forty years of research},
     address =   {Pisa, Italy},
     month =     {23 October},
     year =      {2009},
  }
  

Copyright notice
Last modified: Friday, 01-Jan-2010 16:12:07 CET