Formalising Sequential Game Theory
The OTS/CafeOBJ method can be used to make a formal model of a system as
an observational transition system, or an OTS, specify the OTS in CafeOBJ,
an algebraic specification language, and verify that the OTS has some
desired properties with the help of the CafeOBJ system. The usefulness of
the method has been confirmed by applying it to non-trivial applications
such as distributed algorithms and security protocols. In this talk, a
small example is used to describe the OTS/CafeOBJ method.
Term rewriting systems for modular algebraic specification languages
モジュラーな代数仕様言語であるOBJ言語族は，
モジュールをベースとした仕様記述スタイルを提供しており，
組み込みのモジュールや過去に記述したモジュールの再利用などにより
大規模で複雑なシステムの仕様記述に効果的である．
一方，等式の集合を公理とするOBJ言語族の検証は，
等式を書き換え規則と見なす項書き換えシステムによる
等式推論をベースに行われるが，
モジュールシステムによる洗練された仕様記述に比べ，
仕様検証ではモジュールシステムの利点が活かされているとは言えない．
本論文では，モジュラーな代数仕様言語の検証エンジンに相応しい
モジュラーな検証システムを提案する．
提案するモジュラーな検証システムでは，
組み込みモジュールや等価述語などの通常の項書き換えシステムでは
Formalising Sequential Game Theory
We will present Coq-formalised proofs of two famous results in
(sequential) game theory: Kuhn's and Aumann's Theorems. The proofs are
conducted LCF-style, i.e., by computational means over inductive
structures, and are very simple. Aumann's Theorem, in particular, is
traditionally proved by model-theoretic means and the alternative view
offered by our approach straightforwardly clarifies some open issues.