A decision procedure for combinations of propositional temporal logic and other specialized theories

DOI10.1007/BF02432150MaRDI QIDQ1097264zbMATH OpenOpenAlexFDO

Authors David A. Plaisted

Publication date 1986

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf02432150

zbMATH Keywords

fixed pointsdecision procedurediscrete linear time propositional temporal logicquantifier-free theoriesreasoning about concurrent programsspecialized theory

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 3974944
• scientific article; zbMATH DE number 3871318
• Propositional temporal logics: decidability and completeness
• scientific article; zbMATH DE number 149521
• An efficient decision procedure for propositional projection temporal logic

Cites work

• scientific article; zbMATH DE number 3755912 (Why is no real title available?)
• scientific article; zbMATH DE number 3767031 (Why is no real title available?)
• Deciding full branching time logic
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Synthesis of Communicating Processes from Temporal Logic Specifications
• The Total Correctness of Parallel Programs
• The complexity of propositional linear temporal logics
• The propositional dynamic logic of deterministic, well-structured programs
• Using branching time temporal logic to synthesize synchronization skeletons

Cited in

(7)

• scientific article; zbMATH DE number 149521 (Why is no real title available?)
• A decidability result for the model checking of infinite-state systems
• Combining temporal logic systems
• A Cookbook for Temporal Conceptual Data Modelling with Description Logics
• scientific article; zbMATH DE number 3974944 (Why is no real title available?)
• TABLEAUX: A general theorem prover for modal logics
• Efficient decision procedure for propositional projection temporal logic

This page was built for publication: A decision procedure for combinations of propositional temporal logic and other specialized theories

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