Skip to content

Latest commit

 

History

History
15 lines (9 loc) · 709 Bytes

README.md

File metadata and controls

15 lines (9 loc) · 709 Bytes
Raw

Categorical semantics for counterpart-based temporal logics

This repository contains the Agda presentation of the categorical semantics for a quantified linear temporal logic QLTL based on counterpart semantics in the sense of Lewis.

We use the agda-categories library as a practical foundation to construct the models of our logic by means of relational presheaves.

Positive normal form

Some results on a positive normal form of this logic in the case of linear trace-like models can be found at https://github.com/iwilare/qltl-pnf/.

Requirements

  • agda-categories 1.7
  • agda-stdlib 1.7.1
  • agda 2.6.2.2