日々の流転

λ. 『HELLSING (9)』 by 平野 耕太

HELLSING 9 (ヤングキングコミックス)(平野 耕太) を読んだ。 10巻で完結らしいし、最後に向けて盛り上がってきたなあ。

λ. SPASS を試す

SPASS: An Automated Theorem Prover for First-Order Logic with Equality という一階述語論理の定理証明機を見つけたので、ちょっと試してみる。

Smullyan's drinkers' paradox

まずは、こないだ20070828#p02でAgdaで証明を書いた Smullyan's drinkers' paradox を試してみる。

begin_problem(Drinker).

list_of_descriptions.
name({* Smullyan's drinkers' paradox *}).
author({* Masahiro Sakai *}).
status(unsatisfiable).
description({* Smullyan's drinkers' paradox *}).
end_of_list.

list_of_symbols.
predicates[(Drink,1)].
end_of_list.

list_of_formulae(axioms).
end_of_list.

list_of_formulae(conjectures).
formula(exists([x], implies(Drink(x), forall([y], Drink(y))))).
end_of_list.

end_problem.

Webから試せるようになっているので、これを-DocProofオプションと共に与えると何やら証明らしきものが得られるが、読み方が良くわからない。

パースの論理式(Peirce's formula)

命題論理の例として、先日20070814#p01でHaskellで証明したパースの論理式(Peirce's formula)を試してみる。当然何の問題もない。

begin_problem(Peirce).

list_of_descriptions.
name({* Peirce's formula *}).
author({* Masahiro Sakai *}).
status(unsatisfiable).
description({* Peirce's formula *}).
end_of_list.

list_of_symbols.
predicates[(P,0), (Q,0)].
end_of_list.

list_of_formulae(axioms).
end_of_list.

list_of_formulae(conjectures).
formula(implies(implies(implies(P, Q), P), P)).
end_of_list.

end_problem.

様相論理の例 (2007-11-23追記)

命題様相論理の論理式は、「世界」の集合を個体領域とする一階述語論理の論理式に変換することが出来る。 そのため一階述語論理の定理証明器等を様相論理に対して使うことが出来る。 そして、SPASSには様相論理を扱う機能があり*1、変換を自動的に行って証明をしてくれる。

以下の例は、到達可能性関係が反射的であることを仮定して、□A→A を証明する例。 ここでは反射的であることを明示的に公理としているが、オプションで -EMLTheory=2 を指定すれば全ての様相の到達可能性関係が反射的であることは自動的に仮定される。 その方が効率は良いかも。

begin_problem(Reflexivity).

list_of_descriptions.
name({* T from Reflexivity *}).
author({* Masahiro Sakai *}).
status(satisfiable).
description({* T from Reflexivity *}).
end_of_list.

list_of_symbols.
predicates[ (R, 2), (r, 0), (A, 0) ].
translpairs[ (r, R) ]. % r is interpreted as R
end_of_list.

list_of_special_formulae(axioms, eml).
formula( forall([x], R(x, x)) ).
end_of_list.

list_of_special_formulae(conjectures, eml).
prop_formula( implies(box(r, A), A) ). % T
end_of_list.

end_problem.