1986 Fiscal Year Final Research Report Summary
Design of a System Description Language based on a Temporal-Spatiol Modal Logic and its Application to Automated Circuit Synthesis Problems.
| Project/Area Number |
60580016
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | YAMAGATA University |
|---|
Principal Investigator |
HARAO Masateru Faculty of Eng. Yamagata Univ., Professor, 工学部, 教授 (00006272)
|
|---|
| Project Period (FY) |
1985 – 1986
|
| Keywords | temporal and spatial modal logic / Specification logic / Circuit realization language / Automated circuit synthesis / Resolution algorithm / Theorem Proving / Knowledge representation / 回路レイアウト |
|---|
| Research Abstract |
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.
|
