Temporal logic programming in Clojure core.logic
1 min read

Temporal logic programming in Clojure core.logic

An extended title would read “temporal logic programming with explicit discrete time”. Temporal logics allow reasoning about time-varying propositions. By using a relational arithmetic implementation of time, we can to a limited extent express the core temporal operators in core.logic:

  1. next P, which means P is true at the next moment of time

  2. eventually P, which means P is true now or at some time in the future

  3. hereon P, which means P is true now and at any time in the future

While I have used explicit time, I hope it is clear to the interested reader that this could readily be made into a miniKanren extension where all relations have implicit time. Some non-relational operators have been used for the examples, but an actual implementation involving the three temporal operators can be made relational, respecting some restrictions of context. The examples and the implementation was inspired by Templog, which is a temporal Prolog variant.

Source code.