Interactive theorem proving with temporal logic

DOI10.1006/JSCO.1996.0094MaRDI QIDQ1355780zbMATH OpenOpenAlexFDO

Authors Laurent Théry, Amy P. Felty

Publication date 13 October 1997

Published in Journal of Symbolic Computation (Search for Journal in Brave)

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

zbMATH Keywords

linear temporal logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Recommendations

• A proof system for a unified temporal logic
• A sound and complete proof system for a unified temporal logic
• PTL sequent calculus system
• scientific article; zbMATH DE number 1476493

Cited in

(3)

• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• Logics in Artificial Intelligence
• A sound and complete proof system for a unified temporal logic

Describes a project that uses

Uses Software

• STeP
• Isabelle

This page was built for publication: Interactive theorem proving with temporal logic

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