ケンブリッジ大学とミュンヘン工科大学で開発された証明支援言語システムでIsabelle というソフトがあります。このユーザグループにおいて，0除算が検証され，任意のxについてx/0=0が証明されました。またx/0の関数値については0除算算法というローラン展開を用いる方法が使われますが，これについても一部が検証がされました。
私の属する0除算研究グループにおいては0除算は当たり前のものになっていますが，別の独立したグループにより基本的な部分とそれに続く部分の一部ですが正しいと検証されたことの意義は大きいのではないでしょうか。
以下はIsabelleのサイトです。
https://isabelle.in.tum.de/
PR
