Skip to content

Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using https://github.com/agda/agda-categories

Notifications You must be signed in to change notification settings

iwilare/categorical-qtl

Repository files navigation

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

About

Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using https://github.com/agda/agda-categories

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages