一階論理上の等号推論：理論と実際

摘要

本稿では近年発展を遂げてきた一階論理上の等号推論について，理論と実際の両面について解説を行う．近年の等号推論技術の進化は，上昇型推論戦略上の等号調整の高度化によって達成されてきた．本稿ではまず，基礎となる等号推論体系を解説し，次に最新の定理自動証明システムを支える種々の工学的技術について概説する．また下降型定理証明における等号推論技術の最近の幾つかの進展についても解説を加える．