A study on a practical consequence finding system

点击翻译按钮获取中文摘要

SOLAR is a first-order consequence finding system. To improve the scalability, we proposed a divide-and-conquer strategy for SOL tableau calculus, developed a new consequence finding system based on best-first search, and introduced various kinds of the pruning techniques for the system. For propositional cases, we developed a prototype of a consequence finding system based on SAT technologies. The new first-order SOLAR system showed superior performance compared to the old one, and the developed SAT solver, called GlueMiniSat, which is used as a inference engine of the propositional system, got 1st and 2nd places of SAT 2011 and 2013 competitions in Applications UNSAT category, respectively.