Design of a System Description Language based on a Temporal-Spatiol Modal Logic and its Application to Automated Circuit Synthesis Problems.

本文研究了电路描述语言的设计和基于定理证明技术的自动电路综合系统的开发问题。具体主题如下：(1)能够描述时间和空间特征的逻辑系统的研究；(2)逻辑框架内的推理和验证机制的研究；(3)利用定理证明技术开发自动化电路综合系统。(4)电路布置图系统的开发。对于(1)，我们得到了ETSL的完备性和决策过程等理论结果，以及作为电路描述语言和模态逻辑的知识表示语言的几个结果。对于(2)，我们表明，通过将其语法限制为Horn模态子句，改进的解析算法可用于模态谓词逻辑。对于(3)，我们设计了一种基于模态逻辑的电路描述语言，称为电路实现语言。采用递归方程作为电路说明语言，将自动电路综合问题形式化为递归方程到电路实现语言的转换。转换过程分别由与基本电路元件和转换规则相对应的公理和推理规则构成一个逻辑系统。基于这种方法的原型是使用Prolog构建的。对于(4)，通过接受以电路实现语言编写的任何输入来输出电路布置图的布图系统。根据目前所获得的结果，我们可以得出结论，本研究提出的方法是高级语言自动电路合成的有希望的方法之一。

This research treats the problems of designing a circuit description language and of developing a automated circuit synthesis system based on theorem proving techniques. The concrete themes are the followings:(1) Studies on logical systems which are able to describe both of the temporal and spatial features, (2) Studies on inference and verification mechanisms whithin the framework of logics, (3) Development of an automated circuit synthesis system using theorem proving techniques. (4) Development of a circuit layout system.For (1), we obtained the theoretical results such that the completenes and decision procedure of ETSL etc., and several results as a circuit description language and a knowledge represention language of modal logics.For (2), we showed that a modified resolution algorithm is available to our modal predicate logic by restricting its syntax as the Horn modal clauses.For (3), we designed a circuit description language based on a modal logic which is called the circuit realization language. By adopting the recursive equations as the circuit specification language, we formalized the automated circuit synthesis problem as a transformation from recursive equations to the circuit realization language. The transformation procedures are formulated to a logical system with the axioms and the inference rules corresponding to the basic circuit elements and the transformation rules, respectively. A prototype based on this approach is constructed using Prolog.For (4), a layout system which outputs the circuit layout drowings by accepting any inputs written in the circuit realization language. According to these results obtained until now, we are able to conclude that the appoach proposed in this research is one of the hopeful methods for the automated circuit synthesis from high level languages.