Clausal Tableaux for Hybrid PDL

DOI10.1016/j.entcs.2011.10.009zbMath1347.03045WikidataQ113318197 ScholiaQ113318197MaRDI QIDQ2825411

Mark Kaminski, Gert Smolka

Publication date: 7 October 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2011.10.009

zbMATH Keywords

hybrid logic; dynamic logic; tableau systems; decision procedures

Mathematics Subject Classification ID

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

03B70: Logic in computer science

03B35: Mechanization of proofs and logical operations

Related Items

Clausal Tableaux for Hybrid PDL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• From regular expressions to deterministic automata
• An essay in combinatory dynamic logic
• PDL with data constants
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Clausal Tableaux for Hybrid PDL
• An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
• Terminating Tableaux for Hybrid Logic with Eventualities