近年の一階論理定理証明プログラムの実際

摘要

In this paper, we survey a first-order equational theorem proving mainly from a viewpoint of practice. Bottom-up theorem proving is a quite appropriate framework for equational inference, so we study its underlying advanced calculi and several technologies of state-of-the-art automated equational theorem proving systems.%本稿では近年発展を遂げてきた一階論理定理証明システム，特に，応用上極めて重要な等号推論システムについて概説を行う．現在までのところ，等号推論の効率化は，上昇型推論戦略上の等号調整法の効率化によって達成されてきた．その基礎となる推論体系と最新の証明システムで使われている種々の工学的技術について概説する．