A New Execution Model for the logic of hereditary Harrop formulas
arXiv:1507.01771
Abstract
The class of first-order Hereditary Harrop formulas () is a well-established extension of first-order Horn clauses. Its operational semantics is based on intuitionistic provability. We propose another operational semantics for which is based on game semantics. This new semantics has several interesting aspects: in particular, it gives a logical status to the predicate in Prolog.
6 pages. arXiv admin note: substantial text overlap with arXiv:1211.6535