Coq と定理証明
Menu Menu
一階述語論理
一階述語論理は、プログラムとほとんど同じ。
変数 x 1,2 や "a", 'a' などの値を持つ
関数 f(x) 入力から出力が決まる。出力は値や真理値
1>x 入力から真理値が決まる
∃x あるx (普通は型を指定する)
∀x すべての可能な x (普通は型を指定する)
P 真偽を値に持つ変数、または、論理式
P(x) 変数 x を持つ論理式
P∧Q PかつQ
P∨Q PまたはQ
¬P Pでない
P→Q PならばQ ( ¬ P ならば真であることに注意 )
t 真
f 偽
∃x や、∀x は、ローカル変数を定義している。量化記号と言う。量化記号のついてない変数を自由変数という。
プログラムと違って、変数は書き換えられない。Haskell と同じ。関数も、入力が同じなら出力は常に同じ。
閉じた論理式
論理式に出てくる変数がすべて、∃x や、∀x の形ならば、その論理式は閉じていて、真か偽がどちらかになる(はず)。
充足性
閉じてない論理式について、
1>x は x = 0 ならば正しい。1>x は充足可能。Satisfiable 0>x*x x に何を入れても正しくならない。充足不能。Unsatisfiable 0<=x*x x に何を入れても正しい。恒真。Valid論理式の自由変数への値の割り当てを interpretation という。論理式を真にする interpretation を model という。
モデル検証
要求された論理式で記述された仕様Pを、実装 I が満たすことを調べたい。I → ¬P が Unsatisfiable であれば良い。Satisfiable ならば、反例があることになる。
実装と論理式の変数の値のすべての組み合わせを調べて、 I → ¬P の真理値を調べることをモデル検証という。
実際には、時間の概念を入れた論理を用いて、実装は Finite Automaton で記述したものを用いる。
□P いつも P ◇P いつか P = ¬□¬ Pdebugger や Java Pathfinder はモデル検証手法の一つ。
証明
モデル検証は、論理式の変数の割り当てを調べて、反例を探す。定理証明では、公理(恒真だとわかっている論理式)から、推論規則(論理式の変形規則) を使って、与えられた論理式が恒真であることを示す。
推論の形式には、Natural deduction 自然演繹と Sequent Calculus シーケント代数の二種類がよく使われている。
ここでは Sequent Calculus を使う。
論理
論理式の構成の方法、恒真である公理の集合、推論の方法が論理を決定する。論理式の構成法は既に述べた。推論規則のほとんどは、論理記号の導入(introduciton)と削除(elimination)である。
論理記号を制限すると、論理式の論理記号を上から削除していくだけで自動的に公理まで分解できる場合がある。こういう場合は、その論理は決定手続きがあるという。
論理式が恒真であれば証明がある時にその論理は完全(complete)であるという。
証明があれば、その論理式が恒真である時に、その論理は安全(sound)であるという。
一階述語論理は sound and copmlete であることが知られている。しかし、一般的に決定手続きは存在するとは限らない。