Programming in logic without logic programming

TL;DR

This paper explores a logic-based framework for reactive computation, focusing on operational semantics that efficiently execute actions to satisfy reactive rules, and characterizes reactive models without relying on logic programming.

Contribution

It characterizes reactive models and proves the operational semantics can generate exactly these models, omitting the logic programming component for clarity.

Findings

Operational semantics is sound but incomplete.

Reactive models are fully characterized.

Framework excludes logic programming for focus.

Abstract

In previous work, we proposed a logic-based framework in which computation is the execution of actions in an attempt to make reactive rules of the form if antecedent then consequent true in a canonical model of a logic program determined by an initial state, sequence of events, and the resulting sequence of subsequent states. In this model-theoretic semantics, reactive rules are the driving force, and logic programs play only a supporting role. In the canonical model, states, actions and other events are represented with timestamps. But in the operational semantics, for the sake of efficiency, timestamps are omitted and only the current state is maintained. State transitions are performed reactively by executing actions to make the consequents of rules true whenever the antecedents become true. This operational semantics is sound, but incomplete. It cannot make reactive rules true by preventing their antecedents from becoming true, or by proactively making their consequents true before their antecedents become true. In this paper, we characterize the notion of reactive model, and prove that the operational semantics can generate all and only such models. In order to focus on the main issues, we omit the logic programming component of the framework.