On Merging Resolution and Induction

概要

論文の詳細を見る
In this paper, we deal with the old problem of merging resolution and induction from a new perspective. Unlike most works on inductive theorem proving in logic programming, where implicational formulas are proved by computation induction, we use the simple induction schema on natural numbers and make induction by a simple method similar to loop detection. In order to increase the power of the induction schema, we introduce a higher order language having recursion terms and functional variables together with the unification procedure that copes with those constructs and some arithmetic computations. We also point out that the notion of constraint can further enrich our framework.
一般社団法人情報処理学会の論文
1996-03-26