日々の流転

λ. IDPで数独を解く

数独をParadoxとDarwinとMaceで解いてみたので、ついでにIDPでも試してみた*1。

• 入力ファイル sudoku-idp.idp
• ログ sudoku-idp.txt

IDPの特徴は帰納的定義が出来ることのようだ(普通の一階述語論理では帰納的な定義は出来ない)。 具体的には { R(t1,…,tn) <- 論理式. } 等と書けて、論理式の中でRを使うことで、関係Rを帰納的に定義出来る。 帰納的定義が出来るということは、例えば推移閉包を公理化出来るので、グラフが関係してくるようなパズルを解くのには向いていそうだ。

あと、記述言語では例によって、感嘆符「!」と疑問符「?」がそれぞれ全称量化子と存在量化子として用いられている。