广义和与递归定义型的合成定理及其应用

理论计算机科学电子笔记123（2005）209-211www.elsevier.com/locate/entcs广义和与递归定义型亚历山大·拉比诺维奇特拉维夫大学计算机科学学院特拉维夫，以色列电子邮件地址：rabinoa@post.tau.ac.il组合定理是一种工具，它将对复合数据结构的推理简化为对它们的部分的推理。 例如，一个关于两个结构的笛卡尔积的句子的真值可以简化为关于该积的分量的句子的真值合成定理的一个开创性的例子是费费曼-沃特定理[2]。Feferman和Vaught介绍了一个广义的产品建设，其中包括许多代数结构的数学结构。他们的主要定理将广义乘积的一阶理论简化为因子的一阶理论和指数结构的一元二阶理论。Shelah [24]定义了广义和的概念，并提供了合成定理，该定理将广义和的一元二阶理论简化为被加数及其索引结构的一元二阶理论。广义和的一个重要例子是线性序集的序和。在[24]中，线性序的合成定理是获得线性序的一元理论的显著可判定性结果的主要工具之一。文[6]给出了树上一元二阶逻辑的几个合成定理。合成方法在代数和逻辑中的两个重要应用是：1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.04.049210A. Rabinovich/Electronic Notes in Theoretical Computer Science 123（2005）209决定性。这里的方法作为一个非常强大的工具，以获得新的结果，以及简化其他可判定性证明[2，24，3，6，8，1，12]。可表达性。 分析一阶和一元二阶语言的表达能力。合成方法对于证明表达能力的限制[7，8，9，15，16]和证明表达能力的积极结果[10，14，15，16，5，18，19]都是有用的Gurevich[4]和Thomas [26]在综述中描述了线性序的合成定理;在那里，它被说明为序的一元逻辑的可判定性，作为由Bu？hi提出的自动机理论方法的替代。尽管存在着复杂性，但这种复杂性方法仍然在很大程度上被理论计算机科学界所忽视。W. Thomas在[26]中调查了Shelah偏好是（仍然是）自动机理论方法.因为它不涉及令人恐惧的逻辑技术，因为人们在[24]中发现了它们。因此，有一种倾向，即模型理论方法的优点被忽视。这是不幸的，因为它排除了一些有趣的应用程序。在这次演讲中，除了调查经典的合成结果外，我的主要技术贡献如下：(i) 广义和上一阶逻辑的一个复合定理[20](ii) 递归定义类型的复合定理[21]。引用[1] J.P. Burges，Y.古列维奇时态逻辑的决策问题。Notre Dame J. Formal Logic，26（1985）115-128.[2] S. Feferman和R.L.Vaught（1959）.代数系统乘积的一阶性质Fundamenta Mathematica47：57-103.[3] Y. Gurevich（1979年）。短链理论Ⅰ。Journal of Symbolic Logic44：481-490.[4] Y. Gurevich（1985年）。一元二阶理论在模型理论逻辑中，（J. Barwise和S. Feferman，eds.），479-506，Springer出版社[5] Y. Gurevich和A.拉宾诺维奇可定义性和不可定义性，以真实秩序为背景。Journal of SymbolicLogic 65（2）（2000），946-958.[6] Y. Gurevich和S. Shelah（1979年）。短链理论2。 Journal of Symbolic Logic44：491-502.[7] Y. Gurevich和S. Shelah（1979年）。拉宾的统一化问题。 Journal of Symbolic Logic48：1105-1119.[8] Y. Gurevich和S. Shelah（1985年）。分支时间逻辑的判定问题。Journal of Symbolic Logic50（3）：668-681.−A. Rabinovich/Electronic Notes in Theoretical Computer Science 123（2005）209-211211[9] Y. Gurevich和S.希拉在解释方法的力量。符号逻辑杂志，54：305[10] T. Hafer和W. Thomas（1987）.二叉树的一元理论中的计算树逻辑CTL计数器在ICALP'87会议录中[11] Y. Hirshfeld和A.拉宾诺维奇可判定度量逻辑的框架。在ICALP 99，LNCS第1644卷，第422-432页，Springer Verlag 1999中。[12] W. Hodges（1993）. 模型理论 北京大学出版社.[13] N. Immerman（1998年）。描述性复杂性，Springer Verlag，1998。[14] S. Lifsches和S.希拉皮亚诺算术在一元序理论中可能无法解释。Journal of Symbolic Logic，62（3）：848[15] S. Lifsches和S.希拉树类中的一致化、选择函数与井序Journal of Symbolic Logic，61：1206[16] S. Lifsches和S.希拉树类中的一致化与Skolem函数。 Journal of Symbolic Logic，63：103[17] J.A. Feferman-Vaught定理的Makowsky数学方面2003年。[18] F. Moller和A.拉宾诺维奇关于CTL* 的表达能力。LICS 1999，360-369.[19] F. Moller，A.拉宾诺维奇计算CTL*：论一元路径逻辑的表达能力信息与计算184（2003）147-159..[20] A.拉宾诺维奇广义和的合成定理。《技术报告》，特拉维夫大学www.cs.tau.ac.il/，1998年。[21] A.拉宾诺维奇递归定义结构的合成定理。技术报告，1999年。[22] A.拉宾诺维奇论组合性及其局限性。技术报告，爱丁堡大学，2001年。[23] E.拉维使用翻译方案分解数据库。博士论文，Technion，以色列理工学院，1998年。[24] S. Shelah（1975年）。一元秩序论数学年鉴102：379-419。[25] S. Shelah（1996年）。关于有阶随机图的很弱0 - 1律。 Journal of Logic and Computation6：137-159.[26] W. Thomas（1997年）。序数词的游戏、合成方法与一元理论。 逻辑与计算机科学结构：纪念A。Escheren feucht，Lecture Notes in Computer Science1261：118-143，Springer-Verlag。[27] S. 泽特曼组成方法。博士韦恩州立大学博士论文，1994年。