Co-operative research on theoretical foundations of computer programs

由于每位研究人员的努力，本研究项目的课题都取得了良好的研究成果。1.逻辑：SA理论可判定性的形式化推导，直觉线性逻辑的扩展，BCK和BCIW的有限模型性质，谓词逻辑的代数语义，子结构逻辑的可判定性和有限模型性质，Feferman系统的一种新形式化，自动证明中的自然证明，知识谓词的有效性验证。2.程序理论：同构分析等价理论，用数值变换和时态运算两种方法分析软/硬件系统中的真实的时间问题，并发逻辑程序设计环境中的文字依赖网，一种类型化的实例证明演算，一种动态尺寸制表的变换方法，实例编程。数据类型专门化的等待时间分析、有效使用流水线和高速缓存的编程技术、无分数处理器的计算决定因素的效率。4.图论：5.人工智能：从facs中发现机器的数学理论，平面图的形式化，音乐表演中的分析方法和表达工具。

Owing to each of research fellows, good research results are established on subjects of this research project. Some of them are listed in the following.1.Logic : a formal derivation of the decidability of the theory SA,extending intuitionistic linear logic, the finite model property for BCK and BCIW,algebraic semantics for predicate logic, decidability and finite model property of substructural logics, a new formalization of Feferman's system, natural proofs in automated proving, validity verification of knowledge predicats.2.Theory of programs : locomorphism analytical equivalence theory, analysis of a real time problem in a software/hardware system in two ways using nu-conversion and by tense arithmetic, literal dependence net in concurrent logic programming environment, a typed lambda-calculus of proving-by-example, a transformation method for dynamic-sized tabulation, programming by example.3.Programming : biding time analysis for data type specialization, programming techniques for effective use of pipe-line and cache, efficiency of computing determinants by a fraction-free processor.4.Graph theory : graph decomposition with prescribed vertices, twist number of complete bipartite praphs.5.Artificial inteligence : a mathematical theory of machine discovery from facs, formalization of planar graphs, analysis methods and tools of expression in music performances.