From "proof"+"inference" to "query-answering problems" + "equivalent transformation"

2016 Fiscal Year Final Research Report

• Project/Area Number: 26540110
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Intelligent informatics
• Research Institution: Hokkaido University
• Principal Investigator: Akama Kiyoshi 北海道大学, 情報基盤センター, 名誉教授 (50126265)
• Project Period (FY): 2014-04-01 – 2017-03-31
• Keywords: ＫＲロジック / 等価変換 / 証明問題 / 求解問題 / 意味保存スコーレム化 / モデルインターセクション問題 / 関数変数 / 論理構造

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.

Free Research Field

情報科学