更新。 sympy_matrix_tools。バージョン 0.2.4。…

jrf> 更新。

sympy_matrix_tools。バージョン 0.2.4。

述語論理の証明ができるように resolve_implications を作り、rename_bound_symbols_uniquely や conditional_apply といった補助ツールも作った。

昔、Isabelle を用いて「研究」していたころのことを思い出しながら作った。昔取った杵柄。

ただ、Isabelle と違い、meta logic があるわけでもなく、対象論理だけで proofstate を作るのにちょっととまどった。また meta variable のリフティングに相当するものはこの前作った Apply 系を Wild シンボルと組み合わせることで無理矢理実現していたりする。

そのため、本気で使うにはかなり苦しい仕様となっている。できた定理が公理的に作った論理式と type で区別できるというわけでもない。だから、実験・お遊び以上のものではない。私の過去の「栄光」を懐かしむためだけに作ったといっても過言ではない。