关键词：dynamic logic propositional quantifi 

摘要：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

心智与计算杂志要求:

{1}作者和通讯作者的姓名、工作单位科室、电话、详细通讯地址、邮编和Email。

{2}自稿件发出3个月届满时未接到稿件采用通知的，可自行处理稿件。

{3}稿件用三级标题顶格排序。

{4}论文中引用他人的观点及材料时，须将参考文献按正文中出现的先后次序列于文后。

{5}来稿请附中英文摘要，中文摘要限500字以内。英文摘要宜控制在300实词以内。

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社