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

DOI10.1007/BF02432150zbMath0635.03026OpenAlexW2074163046MaRDI QIDQ1097264

David Alan 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

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

Related Items

A Cookbook for Temporal Conceptual Data Modelling with Description Logics ⋮ A decidability result for the model checking of infinite-state systems ⋮ TABLEAUX: A general theorem prover for modal logics

Cites Work

• Unnamed Item
• Unnamed Item
• The propositional dynamic logic of deterministic, well-structured programs
• Using branching time temporal logic to synthesize synchronization skeletons
• Synthesis of Communicating Processes from Temporal Logic Specifications
• Deciding full branching time logic
• The complexity of propositional linear temporal logics
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• The Total Correctness of Parallel Programs

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