知性と感性の情報学的討究III : @-calculusに基づく協調システムの検証例-アンサンブル・プログラム

概要

論文の詳細を見る
A verification of cooperative real-timing systems based on @-calculus, which is a more or less small formal system on natural number time, is discussed as the third article in the series on "Intellect and Sensibility Treated in Informatics". As an example, a successful automatic ensemble system that is one of the person-computer cooperative real-timing systems, developed in Psyche Project in Artificial Intelligence Laboratory, University of Tsukuba, is represented and analysed, demonstrating the feasibility of carrying out formal verification or proof in our formalism. In the representation and analysis, program arrays are dealt with rewritable functions, i.e higher-order variables as in ν-conversion. And, moreover, not only one step of executions, close to assembler-language like instructions, but also "higher-level specifications" are represented by program axioms, together with the "timer" whose value changes along with the execution time of the program.
埼玉短期大学の論文
2004-03-31