Clausal Tableaux for Hybrid PDL

DOI10.1016/j.entcs.2011.10.009zbMath1347.03045OpenAlexW2015560379WikidataQ113318197 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 logicdynamic logictableau systemsdecision procedures

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35)

Related Items (1)

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

This page was built for publication: Clausal Tableaux for Hybrid PDL