A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution

DOI10.1093/logcom/7.4.429zbMath0893.03003OpenAlexW2053231467MaRDI QIDQ4351796

No author found.

Publication date: 20 July 1998

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/ee6bd96d6d44c486117484fbf3c93728ab84d148

zbMATH Keywords

temporal logictheorem-provingseparated normal formtemporal descriptions of dynamic systems

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items (14)

First-order temporal verification in practice ⋮ A separation theorem for discrete-time interval temporal logic ⋮ Theorem proving using clausal resolution: from past to present ⋮ Agent deliberation in an executable temporal framework ⋮ Backdoors for linear temporal logic ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ First-order rewritability of ontology-mediated queries in linear temporal logic ⋮ Mechanising first-order temporal resolution ⋮ Alternating automata and temporal logic normal forms ⋮ A clausal resolution method for CTL branching-time temporal logic ⋮ Exploring the future with resource-bounded agents ⋮ A temporal negative normal form which preserves implicants and implicates ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking ⋮ Invertible infinitary calculus without loop rules for restricted FTL

Uses Software

• METATEM

This page was built for publication: A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution