English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper presents a study of operational and type-theoretic properties ofdifferent resolution strategies in Horn clause logic. We distinguish fourdifferent kinds of resolution: resolution by unification (SLD-resolution),resolution by term-matching, the recently introduced structural resolution, andpartial (or lazy) resolution. We express them all uniformly as abstractreduction systems, which allows us to undertake a thorough comparative analysisof their properties. To match this small-step semantics, we propose to takeHoward's System H as a type-theoretic semantic counterpart. Using System H, weinterpret Horn formulas as types, and a derivation for a given formula as theproof term inhabiting the type given by the formula. We prove soundness ofthese abstract reduction systems relative to System H, and we show completenessof SLD-resolution and structural resolution relative to System H. We identifyconditions under which structural resolution is operationally equivalent toSLD-resolution. We show correspondence between term-matching resolution forHorn clause programs without existential variables and term rewriting.

Operational Semantics of Resolution and Productivity in Horn Clause Logic