Terminating Tableaux for Hybrid Logic with Eventualities

x-free and employs a novel clausal form that abstracts away from propositional reasoning. It comes with an elegant correctness proof. We discuss some optimizations for decision procedures.

• Type: Journal
• Year: 2010
• Where: CADE
• Authors: Mark Kaminski, Gert Smolka
• Keywords: CADE 2010, Decision Procedures, Elegant Correctness Proof, Logical Reasoning, Propositional Reasoning