Dynamic Logic (DL) is a formal system for reasoning on the input/output behaviors of programs. Hoare Logic (HL) is the precursor of all dynamic logics known today. Two core systems of DL are Propositional Dynamic Logi...Dynamic Logic (DL) is a formal system for reasoning on the input/output behaviors of programs. Hoare Logic (HL) is the precursor of all dynamic logics known today. Two core systems of DL are Propositional Dynamic Logic (PDL) and Quantificational Dynamic Logic (QDL). PDL is an extension of propositional logic with programs and is the appropriate place to begin investigating DL. QDL can be viewed as the first-order version of PDL. Predicate Dynamic Logic (DPL) is a subsystem of QDL and can be regarded as the most basic of a hierarchy of formulas-as-programs languages. These systems constitute the main topic of this essay. The authors’ elaboration here is very brief and sketchy and with the aim of providing the readers with only the most essence of the topic on the basis of other researchers’ works. The last part is the important one in which the authors summarize the approaches of extending Dynamic Logic. The conclusions are as follows: variants of DL are obtained by reinterpreting some constructs as something else, and/or by adding rules or operators, and/or by restricting or extending or revising some constructs, and/or combining a kind of logic with another one, and/or using a comprehensive way which insights from other disciplines according to its application in various domains. In all these cases, the authors give examples to illustrate the conclusion. It is generally proposed that sometimes the introduction of a new operator or rule or construct, or the introduction of reinterpretation or restriction or extension or revision of some constructs will increase expressive power and sometimes not; sometimes it has effect on the complexity of deciding satisfiability and sometimes not. Finally, the authors sum up major aspects which we should consider during investigating a specific variant of DL. The researchers should focus on the well-formed expressions and on the validity of expressions about it with respect to standard, non-standard and syntactically motivated classes of Kripke models. Other important seman展开更多
基金supported by the Postdoctoral Foundation of China(Grant No.2012M510101)
文摘Dynamic Logic (DL) is a formal system for reasoning on the input/output behaviors of programs. Hoare Logic (HL) is the precursor of all dynamic logics known today. Two core systems of DL are Propositional Dynamic Logic (PDL) and Quantificational Dynamic Logic (QDL). PDL is an extension of propositional logic with programs and is the appropriate place to begin investigating DL. QDL can be viewed as the first-order version of PDL. Predicate Dynamic Logic (DPL) is a subsystem of QDL and can be regarded as the most basic of a hierarchy of formulas-as-programs languages. These systems constitute the main topic of this essay. The authors’ elaboration here is very brief and sketchy and with the aim of providing the readers with only the most essence of the topic on the basis of other researchers’ works. The last part is the important one in which the authors summarize the approaches of extending Dynamic Logic. The conclusions are as follows: variants of DL are obtained by reinterpreting some constructs as something else, and/or by adding rules or operators, and/or by restricting or extending or revising some constructs, and/or combining a kind of logic with another one, and/or using a comprehensive way which insights from other disciplines according to its application in various domains. In all these cases, the authors give examples to illustrate the conclusion. It is generally proposed that sometimes the introduction of a new operator or rule or construct, or the introduction of reinterpretation or restriction or extension or revision of some constructs will increase expressive power and sometimes not; sometimes it has effect on the complexity of deciding satisfiability and sometimes not. Finally, the authors sum up major aspects which we should consider during investigating a specific variant of DL. The researchers should focus on the well-formed expressions and on the validity of expressions about it with respect to standard, non-standard and syntactically motivated classes of Kripke models. Other important seman
