Chaining techniques for automated theorem proving in many-valued logics
Harald Ganzinger, Viorica Sofronie-Stokkermans · 2002
We apply chaining techniques to automated theorem proving in many-valued logics. In particular, we show that superposition specializes to a refined version of the many-valued resolution rules introduced by Baaz and Fermuller, and that ordered chaining can be specialized to a refutationally complete inference system for regular clauses.