Two Core Systems of Dynamic Logic
關鍵詞：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實詞以內。
注：因版權方要求，不能公開全文，如需全文，請咨詢雜志社
