David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Logic, Language and Information 5 (2):193-208 (1996)
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
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 downloads5 ( #226,513 of 1,101,088 )
Recent downloads (6 months)3 ( #116,335 of 1,101,088 )
How can I increase my downloads?