[B! logic] [2ページ] petite_blueのブックマーク

シークエント計算 - Wikipedia

シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。

petite_blue 2007/10/03

リンク

ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (1) 宣言

The Coq Proof Assistant A Tutorial を参考にしつつ，Coq について勉強していこうと思っています．まずは，Windows を使っている人は，ここから， coq-8.0pl3-win.exeをダウンロードして，ダブルクリックして Coq (IDE 付き) をインストールしておいてください． Coq は Calculuc of Inductive Constructions という論理体系に基づいた，定理証明支援系なのだそうです．対話的に形式的な証明を構成していくことができて，さらにそれを，そのまま関数型プログラムの仕様として扱うことができるとのこと．このチュートリアルでは Gallina と呼ばれる基本的な言語仕様だけを扱うそうで，発展的な情報は Coq Reference Manual とか Coq'Art を参照せよ，とのこと．とりあえず，C:\

petite_blue 2007/10/01

coq

リンク

Getting started

The Coq Proof Assistant A Tutorial Version 1 Gérard Huet, Gilles Kahn and Christine Paulin-Mohring LogiCal Project 1This research was partly supported by IST working group “Types” Getting started Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs