文献

J-GLOBAL ID：201602006239618516   整理番号：70A0260904

低次の述語計算における分解のための内そう定理

Interpolation theorems for resolution in lower predicate calculus.

著者 (1件)： SLAGLE J R
資料名： J Assoc Comput Mach  (Journal of the Association for Computing Machinery)
巻： 17  号： 3  ページ： 535-542  発行年： 1970年 
JST資料番号： C0267A  ISSN： 0004-5411  CODEN： JACOA   資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 分解原理は一次の述語計算に対する推論規則である。これの完備性の定理は.これまで有限集合の句に対して証明されていた。それを可算集合にまで拡張し.非常に多くの公理を図式化することを容易にする。また.Craigの内そう定理に類似ないくつかの定理を分解による演えき法のために証明する。これらの定理は命題計算には有力なものであり,計算機による自動証明発見,結果発見のためのプログラムの可能性を示唆する。さて完備性の定理を可算集合まで拡張するにはゲーデルの定理を使用する。これによって3つの定理と5つの系が示されている。また2重の内そう定理についても述べられてし,る;参22

準シソーラス用語： 完備性定理 ,  自動定理証明 ,  述語計算 ,  内そう定理

タイトルに関連する用語 (4件)： 述語計算 ,  分解 ,  内そう ,  定理