| Budget Amount *help |
¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Outline of Final Research Achievements |
Histrically, logic has been centered around proof problems and inference has been mainly used for computation. We have extended such proof-centered logic to create a new theory of logic and computation. The new logic is called KR-Logic, and has quantification of function variables. We invented a new large class of logical problems, called model-intersection problems, which is a superset of the class of proof problems and the one of query-answering problems. Equivalent transformation rules are the main computation components. A general schema of solving model intersection problems by equivalent transformation has been proposed, which guarantees the correctness of computation and potentially generates a varieties of procedures including traditional inference-based procedures such as resolution proof procedure. It is expected that this theory gives a new theoretical foundation of logic and computation.
|
