A Logical Approach to CTL

We introduce a notion of proof for CTL with respect to a given nite model and show some advantages of using such a notion. This also suggests to de ne a slight extension of CTL, called SCTL, where predicates can have an arbitrary arity.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/hal-00919467
Author Dowek, Gilles, Jiang, Ying
Maintainer CCSD
Last Updated May 7, 2026, 18:59 (UTC)
Created May 7, 2026, 18:59 (UTC)
Identifier hal-00919467
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM) ; Inria Paris-Rocquencourt ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
creator Dowek, Gilles
date 2014-01-17T00:00:00
harvest_object_id 59822a5c-0177-4a06-8c26-fda6b82cb3c4
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-02-26T00:00:00
set_spec type:UNDEFINED