Counterpart-based quantified temporal logics

DOI10.1016/J.JLAMP.2025.101082MaRDI QIDQ6879442zbMATH OpenFDO

Authors Fabio Gadducci, Andrea Laretto, Davide Trotta

Publication date 30 December 2025

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2025.101082

Mathematics Subject Classification ID

Temporal logic (03B44) Categorical logic, topoi (03G30) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A presheaf semantics for quantified temporal logics
• A tableau construction for finite linear-time temporal logic
• A Temporal Graph Logic for Verification of Graph Transformation Systems
• Adjointness in Foundations
• Alternating-time temporal logic in the calculus of (co)inductive constructions
• An algebraic construction of predicate transformers
• An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
• Auto in Agda. Programming proof search using reflection
• Correct Hardware Design and Verification Methods
• Counterpart semantics for a second-order -calculus
• Expressiveness and complexity of graph logic
• scientific article; zbMATH DE number 4072929 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Lax presheaves and exponentiability
• Metric temporal graph logic over typed attributed graphs
• Modal logics withn-ary connectives
• Monadic second-order incorrectness logic for GP 2
• Monodic fragments of first-order temporal logics: 2000--2001 A.D.
• Optimistic and pessimistic on-the-fly analysis for metric temporal graph logic
• Real-time policy enforcement with metric first-order temporal logic
• Relational and partial variable sets and basic predicate logic
• Sesqui-Pushout Rewriting
• Specification and verification of a linear-time temporal logic for graph transformation
• The Lean 4 theorem prover and programming language
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Types for Proofs and Programs
• Verifying graph programs with monadic second-order logic

Cited in

(1)

• NWTP 2022 - special issue

This page was built for publication: Counterpart-based quantified temporal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6879442)