| Project/Area Number |
03680027
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology,Hokuriku |
|---|
Principal Investigator |
YONEZAKI Naoki Japan Advanced Institute of Science and Technology,Hokuriku School of information science,Professor, 情報科学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TOKUDA Takehiro Tokyo Institute of Technology Department of Computer Science,Associate professor, 工学部情報工学科, 助教授 (30111644)
|
|---|
| Project Period (FY) |
1991 – 1992
|
| Project Status |
Completed (Fiscal Year 1992)
|
| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 1992: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 1991: ¥1,600,000 (Direct Cost: ¥1,600,000)
|
|---|
| Keywords | Specification / Theorem proving / Object Base / Executable specification / Unification / Realizability / 様相論理 / 定理自動証明 / 定理証明 / オブジェクトベ-ス / 実行可能仕様 / 統一化 |
|---|
| Research Abstract |
Application of non-standard logic to software development is our main concern.
(1) Multi-modal logic for specification of reactive objects: We have developed multi modal logic (MML) which has temporal modality and object modality as well. Formalization of object modalities reflecting has a and is a relations was one of our main concern. For the temporal aspects, we developed a new decidable temporal logic which is more expressive than the usual temporal logics in the sense that we can describe the relation on the number of event occurrences so that we can define more sophisticated fairness notion.
(2)Automated reasoning in non-standard logic: Theorem proving methods for non-standard logic was studied. For the various kind of modal logic, we developed a general theorem prover which utilizes modal unification. We discovered some unification schema which drastically deduce the number of steps of proofs. This schema incorporate cyclic unification so called self-unification. We also developed a resolution style theorem prover for linear logic as a basis of new computation paradigm.
(3) Verification and synthesis of programs: A transformation system from specifications to reactive system programs was developed based on the tableau based model generation system. We introduced several realizability concepts and their decision procedures with which we can design a helpful method for getting proper specifications from those with failure or incompleteness.
(4) Model for work process specification: Planning, scheduling, enacting and evaluating human activity is framework of our daily working process. To describe this, we are developing a model for this kind of work process specifications. The first class objects of the model are Tasks, Agents and Products (TAP). This model has several dimensions i.e. meta-object, abstract-instance, structural hierarchy and temporal dimensions.
|
