A temporal negative normal form which preserves implicants and implicates

DOI10.1080/11663081.2000.10510999zbMath1033.03507OpenAlexW2044668636MaRDI QIDQ4443401

Pablo Cordero, Manuel Enciso, Inma P. de Guzmán

Publication date: 11 January 2004

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.2000.10510999

zbMATH Keywords

temporal logicautomated theorem provingfuture fragmenttemporal negative normal form

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Fast subsumption checks using anti-links
• A structure-preserving clause form translation
• Characterizing diagnoses and systems
• CNF and DNF considered harmful for computing prime implicants/implicates
• A temporal logic for proving properties of topologically general executions
• Temporal Verification of Reactive Systems: Response
• The complexity of propositional linear temporal logics
• A new algebraic semantic approach and some adequate connectives for computation with temporal logic over discrete time
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• The complexity of probabilistic verification
• Verification of temporal properties