2013 Fiscal Year Final Research Report
A study on a practical consequence finding system
| Project/Area Number |
23700164
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Keywords | 結論発見 / 仮説発見 / 一階述語論理 / 命題論理 / 推論システム / 分割統治 |
|---|
| Research Abstract |
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.
|
