PRINCIPIA
ProductsSeminarAbout Us

Isabelle によるシーケント計算

定理証明支援ツール Isabelle 上でシーケント計算の推論規則を表現し,それを使って証明をします.

自然演繹とはまた違ったパズルを楽しむことができます.

集合の帰納的定義を使って推論規則を表現する典型的な例です.シーケント計算は命題論理の範囲です.

※ カットの話はしません.

プログラム

セミナー参加の前提条件

前提知識

必要なもの