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

DOI10.1093/LOGCOM/7.4.429MaRDI QIDQ4351796zbMATH OpenOpenAlexFDO

Authors

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

separated normal formtemporal descriptions of dynamic systemstemporal logictheorem-proving

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1348464
• Past–future separation and normal forms in temporal predicate logic specifications
• Normal form expressions of propositional projection temporal logic
• A temporal negative normal form which preserves implicants and implicates

Cited in

(23)

• Exploring the future with resource-bounded agents
• 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
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• Mechanising first-order temporal resolution
• Alternating automata and temporal logic normal forms
• Invertible infinitary calculus without loop rules for restricted FTL
• Theorem proving using clausal resolution: from past to present
• Normal form expressions of propositional projection temporal logic
• Temporal normal form for linear temporal logic formulae
• Past–future separation and normal forms in temporal predicate logic specifications
• A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic
• scientific article; zbMATH DE number 1348464 (Why is no real title available?)
• A clausal resolution method for CTL branching-time temporal logic
• A temporal negative normal form which preserves implicants and implicates
• scientific article; zbMATH DE number 1538010 (Why is no real title available?)
• Agent deliberation in an executable temporal framework
• A separation theorem for discrete-time interval temporal logic
• A simple rewrite system for the normalization of linear temporal logic
• SAT meets tableaux for linear temporal logic satisfiability
• On the expressive power of the normal form for branching-time temporal logics
• First-order temporal verification in practice

Describes a project that uses

Uses Software

• METATEM

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

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