| 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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2013: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2011: ¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
|
|---|
| 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.
|
