A New Execution Model for the logic of hereditary Harrop formulas

TL;DR

This paper introduces a game semantics-based operational model for hereditary Harrop formulas, providing a new logical interpretation for Prolog's read predicate and extending the understanding of $fohh$ logic.

Contribution

It proposes a novel game semantics for $fohh$, offering a different perspective from traditional provability-based semantics and clarifying the logical status of the read predicate.

Findings

Game semantics offers a new interpretation for $fohh$.

Provides a logical foundation for the read predicate in Prolog.

Enhances understanding of hereditary Harrop formulas' operational behavior.

Abstract

The class of first-order Hereditary Harrop formulas ($fohh$) is a well-established extension of first-order Horn clauses. Its operational semantics is based on intuitionistic provability. We propose another operational semantics for $fohh$ which is based on game semantics. This new semantics has several interesting aspects: in particular, it gives a logical status to the $read$ predicate in Prolog.