coq-comp-dec-modal.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "christian.doczkal@inria.fr"
version: "dev"

homepage: "https://github.com/coq-community/comp-dec-modal"
dev-repo: "git+https://github.com/coq-community/comp-dec-modal.git"
bug-reports: "https://github.com/coq-community/comp-dec-modal/issues"
doc: "https://coq-community.github.io/comp-dec-modal/"
license: "CECILL-B"

synopsis: "Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse"
description: """
This project presents machine-checked constructive proofs of
soundness, completeness, decidability, and the small-model property
for the logics K, K*, CTL, and PDL (with and without converse).

For all considered logics, we prove soundness and completeness of
their respective Hilbert-style axiomatization. For K, K*, and CTL,
we also prove soundness and completeness for Gentzen systems (i.e.,
sequent calculi).

For each logic, the central construction is a pruning-based
algorithm computing for a given formula either a satisfying model of
bounded size or a proof of its negation. The completeness and
decidability results then follow with soundness from the existence
of said algorithm.
  """

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.16"}
  "coq-mathcomp-ssreflect" {>= "2.0"}
  "coq-hierarchy-builder" {>= "1.6.0"}
]

tags: [
  "category:Mathematics/Logic/Modal logic"
  "keyword:modal logic"
  "keyword:completeness"
  "keyword:decidability"
  "keyword:Hilbert system"
  "keyword:computation tree logic"
  "keyword:propositional dynamic logic"
  "logpath:CompDecModal"
]
authors: [
  "Christian Doczkal"
]