Dynamic algebras and the nature of induction
Dynamic algebras and the nature of induction
复制标题
动态代数和归纳法的本质
DOI：
10.1145/800141.804649
复制
发表时间：
1980
期刊：
影响因子：
--
通讯作者：
V. Pratt
中科院分区：
文献类型：
--
作者：
V. Pratt
动态代数构成了命题动态逻辑的Segerberg公理模型的变种（等式定义类）。我们得到以下结果（在不可分性内）。(i)在任何动态代数中，* 是自反传递闭包。(ii)每个自由动力代数都可以分解为有限动力代数。(iii)每个有限动力代数同构于一个Kripke结构。(ii)（iii）蕴含Segerberg公理的Parikh完备性定理。我们还提出了一种方法来处理动态代数内递归的归纳方面。
Dynamic algebras constitute the variety (equationally defined class) of models of the Segerberg axioms for propositional dynamic logic. We obtain the following results (to within inseparability). (i) In any dynamic algebra * is reflexive transitive closure. (ii) Every free dynamic algebra can be factored into finite dynamic algebras. (iii) Every finite dynamic algebra is isomorphic to a Kripke structure. (ii) and (iii) imply Parikh's completeness theorem for the Segerberg axioms. We also present an approach to treating the inductive aspect of recursion within dynamic algebras.