A carregar...
Publicação
Intuitionistic Metric Temporal Logic
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 819.57 KB | Adobe PDF |
Orientador(es)
Resumo(s)
We develop Intuitionistic Metric Temporal Logic (IMTL) that extends prior work on intuitionistic temporal logics in two ways: (1) it generalizes discrete time to dense time with intervals so it can, for example, express the duration of signals, and (2) every proof corresponds to a temporal computation. Our main technical result is a syntactic proof of cut elimination for IMTL, which entails logical consistency and ensures that every proof executes while respecting the flow of time. Cut reductions in IMTL correspond to temporal interactions, although we do not fully develop a programming language in this paper. Beyond the metatheory of IMTL, we illustrate the computational meaning of IMTL proofs by developing examples and a small case study where we apply IMTL to well-timed digital circuit design.
Descrição
Publisher Copyright: © 2023 Owner/Author.
Palavras-chave
Human-Computer Interaction Computer Networks and Communications Computer Vision and Pattern Recognition Software
Contexto Educativo
Citação
Editora
ACM - Association for Computing Machinery