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.