制約問題を解くためのモデル生成型定理証明系の新実装法

A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multienvironment problem by using restoration lists for destructively modified data structures. Furthermore, w... View More