Abstract interpretation of resolution-based semantics

Patrick Cousot, Radhia Cousot, Roberto Giacobazzi

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish (US)
Pages (from-to)4724-4746
Number of pages23
JournalTheoretical Computer Science
Volume410
Issue number46
DOIs
StatePublished - Nov 1 2009

Keywords

  • Abstract interpretation
  • Bottom-up semantics
  • Herbrand semantics
  • Logic programming
  • s-semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Abstract interpretation of resolution-based semantics'. Together they form a unique fingerprint.

Cite this