|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)
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.