meta.yml

---
fullname: Completeness and Decidability of Modal Logic Calculi
shortname: comp-dec-modal
organization: coq-community
community: true
action: true
coqdoc: true
doi: 10.22028/D291-26649

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.
    
publications:
- pub_title: A Machine-Checked Constructive Metatheory of Computation Tree Logic
  pub_url: https://www.ps.uni-saarland.de/static/doczkal-diss/index.php
  pub_doi: 10.22028/D291-26649
- pub_title: Completeness and decidability of converse PDL in the constructive type theory of Coq
  pub_url: https://hal.archives-ouvertes.fr/hal-01646782/
  pub_doi: 10.1145/3167088
    
authors:
- name: Christian Doczkal
  initial: true

maintainers:
- name: Christian Doczkal
  nickname: chdoc

opam-file-maintainer: christian.doczkal@inria.fr

opam-file-version: dev

license:
  fullname: CeCILL-B
  identifier: CECILL-B

supported_coq_versions:
  text: 8.16 or later
  opam: '{>= "8.16"}'

tested_coq_opam_versions:
- version: 'coq-dev'
  repo: 'mathcomp/mathcomp-dev'
- version: '2.2.0-coq-8.19'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
  repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
  repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.16'
  repo: 'mathcomp/mathcomp'

# “At 01:42 on Sunday.”
ci_cron_schedule: '42 1 * * 0'

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{>= "2.0"}'
  description: |-
    [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
- opam:
    name: coq-hierarchy-builder
    version: '{>= "1.6.0"}'
  description: |-
    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later

namespace: CompDecModal

keywords:
- name: modal logic
- name: completeness
- name: decidability
- name: Hilbert system
- name: computation tree logic
- name: propositional dynamic logic

categories:
- name: Mathematics/Logic/Modal logic

coqdoc_index: "docs/latest/coqdoc/toc.html"

documentation: |-
  ## Documentation
  
  The developments for the individual logics are described in the
  publications listed above. The developments on K, K*, and CTL are
  described in the author's PhD thesis titled "A Machine-Checked
  Constructive Metatheory of Computation Tree Logic". The developments
  on PDL and PDL with converse are described in the CPP'18 paper.

  ### Structure

  - The directory `libs` contains infrastructure shared between the
    developments. This includes:
    - `fset.v`: a library for finite sets over types with a choice operator (a precursor of [finmap](https://github.com/math-comp/finmap)).
    - `fset_tac.v`: rudimentary automation for the above (originally implemented by [Alexander Anisimov](https://www.ps.uni-saarland.de/~anisimov/bachelor.php)).
    - `modular_hilbert.v`: a library for constructing proofs in Hilbert axiomatizations for modal logics.
    - `sltype.v`: generic lemmas for alpha/beta decomposition of modal-logic formulas.
  - the remaining directories contain the formalizations for the respective logics.
---