Graduate studies at Western
Journal of Logic, Language and Information 5 (2):193-208 (1996)
|Abstract||In this paper we show that it is possible to eliminate the converse operator from the propositional dynamic logic CPDL (Converse PDL), without compromising the soundness and completeness of inference for it. Specifically we present an encoding of CPDL formulae into PDL that eliminates the converse programs from a CPDL formula, but adds enough information so as not to destroy its original meaning with respect to satisfiability, validity, and logical implication. Notably, the resulting PDL formula is polynomially related to the original one. This fact allows one to build inference procedures for CPDL, by encoding CPDL formulae into PDL, and then running an inference procedure for PDL.|
|Keywords||Propositional dynamics logics logics of programs modal logics decision procedures|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Pierre Le Morvan (1999). The Converse Consequence Condition and Hempelian Qualitative Confirmation. Philosophy of Science 66 (3):448-.
Stéphane Demri & Hans De Nivelle (2005). Deciding Regular Grammar Logics with Converse Through First-Order Logic. Journal of Logic, Language and Information 14 (3):289-329.
Mark Kaminski & Gert Smolka (2009). Terminating Tableau Systems for Hybrid Logic with Difference and Converse. Journal of Logic, Language and Information 18 (4):437-464.
Luca Moretti (2003). Why the Converse Consequence Condition Cannot Be Accepted. Analysis 63 (4):297–300.
Sven Ove Hansson (1990). Preference-Based Deontic Logic (PDL). Journal of Philosophical Logic 19 (1):75 - 93.
Stefan Göller, Markus Lohrey & Carsten Lutz (2009). PDL with Intersection and Converse: Satisfiability and Infinite-State Model Checking. Journal of Symbolic Logic 74 (1):279-314.
Added to index2009-01-28
Total downloads2 ( #246,187 of 723,067 )
Recent downloads (6 months)0
How can I increase my downloads?