Propositional Logic, Invariance Groups for Boolean Functions, and Parallel Higher Type Functionals

这个项目集中在命题证明系统，布尔复杂度，并行/顺序可计算函数的高等类型。该项目特别关注：(1)在各种组合命题的证明中符号数的上界和下界，这些命题的扩展被称为切割平面，起源于运筹学，以及相关的介词逻辑（近似推理逻辑或阈值逻辑、双条件逻辑、模块化计数门逻辑等）；(2)语言L的并行复杂度与L对应的所谓不变群和扩展不变群的代数结构之间的关系（正则语言和上下文无关语言的不变群结构、快速并行可计算语言的扩展不变群结构、单调布尔函数与非单调布尔函数的不变群、与Krohn-Rhodes半群理论的关系）；(3)研究了有界原始递归格式的变体在高阶泛函（其参数可以是函数的函数）中的应用，以及并行可计算实值函数的研究。本研究应用了复杂性理论、证明理论（数理逻辑）、组合学和有限群论的技术。扩展不变性群的初步实验研究将使用并行计算机进行。这项研究的目的是增加我们对低水平并行复杂性和相关逻辑的理解，这些逻辑与逻辑编程、数据库更新方法、VLSI设计和编程语言设计中的长期可能应用有关。

This project concentrates on propositional proof systems, Boolean complexity, and parallel/sequential computable functionals of higher types. The project specifically concerns: (1) upper and lower bounds for the number of symbols in proofs of various combinatorial statements for an extension of resolution called cutting planes, originating in operations research, as well as for related prepositional logics (logics of approximate reasoning or threshold logics, logics with the bi-conditional, with modular counting gates, etc.); (2) the relation between the parallel complexity of a language L and the algebraic structure of so-called invariance groups and extended invariance groups corresponding to L (structure of invariance groups of regular and context free languages, structure of extended invariance groups of fast parallel computable languages, invariance groups of monotonic versus non-monotonic boolean functions, relation to Krohn-Rhodes semi-group theory); and (3) the study of variants of the scheme of bounded primitive recursion applied to higher type functionals (functions whose arguments may be functions), and the study of parallel computable real valued functions. This research applies techniques from complexity theory, proof theory (mathematical logic), combinatorics and finite group theory. Initial experimental studies of extended invariance groups will be done using a parallel computer. The goal of this research is to increase our understanding of low level parallel complexity and associated logics with long term possible applications in logic programming, database update methods, VLSI design, and programming language design.