Operational Semantics of Resolution and Productivity in Horn Clause Logic

Research output: Contribution to journalArticle

7 Citations (Scopus)
20 Downloads (Pure)

Abstract

This paper presents a study of operational and type-theoretic properties of different resolution strategies in Horn clause logic. We distinguish four different kinds of resolution: resolution by unification(SLD-resolution), resolution by term-matching, the recently introduced structural resolution, and partial (or lazy) resolution. We express them all uniformly as abstract reduction systems, which allows us to undertake a thorough comparative analysis of their properties. To match this small-step semantics, we propose to take Howard’s System as a type-theoretic semantic counterpart. Using System H, we interpret Horn formulas as types, and a derivation for a given formula as the proof term inhabiting the type given by the formula.We prove soundness of these abstract reduction systems relative to System H, and we show completeness of SLD-resolution and structural resolution relative to System H. We identify conditions under which structural resolution is operationally equivalent to SLD-resolution. We show correspondence between term-matching resolution for Horn clause programs without existential variables and term rewriting.
Original languageEnglish
Pages (from-to)453-474
Number of pages22
JournalFormal Aspects of Computing
Volume29
Issue number3
Early online date25 Nov 2016
DOIs
Publication statusPublished - May 2017

Fingerprint Dive into the research topics of 'Operational Semantics of Resolution and Productivity in Horn Clause Logic'. Together they form a unique fingerprint.

Cite this