>自然言語の意味を論理学に引き寄せて扱おうとする「形式意味論」っていう分野があって、（応用を知りたい人には少し興味が違うかもしれませんが）田中拓郎「形式意味論」とかが入門的な気がします！

>

> 応用例だと、

> たとえば東ロボくんは統計的手法と形式論理的手法両方を用いていた気がしますが、記憶が定かではありません...

>

> 他のお湯用例だと

> Coq（証明支援システム）という証明支援システムがあって、これは数学的な証明問題を自動/手動を組み合わせて解くものです。

>

> 「証明を思いついて書き連ねるのは人がやって、証明が正しいことは機械にチェックさせる」みたいなイメージでだいたい正しそうです

> Inriaという研究所がその分野だと有名です

>

> ググりワードを羅列すると

> - 自動定理証明

> - (自然言語の)形式意味論

> - 数理論理学

> - formal semantics

> - 形式手法

>

> とか、そこらへんで検索すると関連分野がぞろぞろ引っかかると思います！

> — ゆーちき (@yuchiki1000yen) January 10, 2021