Automated proof search in non-classical logics : efficient matrix proof methods for modal and intuitionistic logics

＜図書＞
Automated proof search in non-classical logics : efficient matrix proof methods for modal and intuitionistic logics

責任表示	Lincoln A. Wallen
シリーズ	The MIT Press series in artificial intelligence
データ種別	図書
出版者	Cambridge, Mass. : MIT Press
出版年	c1990
本文言語	英語
大きさ	239 p. : ill. ; 24 cm
概要	This book develops and demonstrates efficient matrix proof methods for automated deduction within an important and comprehensive class of first order and intuitionistic logics. Traditional techniques ...or the design of efficient proof systems are abstracted from their original setting which allows their application to a wider class of mathematical logic. The logics discussed are used throughout computer science and artificial intelligence. Contents: Introduction I. Automated Deduction in Classical Logic. Proof search in classical sequent calculi. A matrix characterization of classical validity. II. Automated Proof Deduction in Modal Logics. The semantics and proof theory of modal logics. Proof search in modal sequent calculi. Matrix characterizations of modal validity. Alternative proof methods for modal logics. Matrix based proof search. III. Automated Deduction in Intuitionistic Logic. A Matrix proof method. Conclusions. Lincoln A. Wallen is a B.P. Venture Research Fellow at the University of Texas at Austin Automated Deduction in Nonclassical Logics is included in the Artificial Intelligence series, edited by Patrick Winston Michael Brady, and Daniel Bobrow. 続きを見る

状態	巻次	所蔵場所	請求記号	刷年	文庫名称	資料番号	コメント	予約・取寄	複写申込	自動書庫
		理系図1F 開架	410.1/W 36	1990		068252190009806		予約・取寄			予約・取寄

別書名	背表紙タイトル:Automated deduction in nonclassical logics
一般注記	Bibliography: p. [228]-234 Includes indexes
著者標目	*Wallen, Lincoln A.
件　名	LCSH:Proof theory LCSH:Modality (Logic) LCSH:Intuitionistic mathematics
分　類	LCC:QA9.54 DC20:511.3 NDC7:410.12
書誌ID	1001048136
ISBN	0262231441
NCID	BA0786395X
巻冊次	ISBN:0262231441
登録日	2009.09.17
更新日	2009.09.17