(计算机系统结构专业论文)answer+set编程及其应用研究.pdf_第1页
(计算机系统结构专业论文)answer+set编程及其应用研究.pdf_第2页
(计算机系统结构专业论文)answer+set编程及其应用研究.pdf_第3页
(计算机系统结构专业论文)answer+set编程及其应用研究.pdf_第4页
(计算机系统结构专业论文)answer+set编程及其应用研究.pdf_第5页
已阅读5页,还剩128页未读, 继续免费阅读

(计算机系统结构专业论文)answer+set编程及其应用研究.pdf.pdf 免费下载

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

摘要 摘要 1 9 8 8 年m g e l f o n d 和vl i f s c h i t z 共同为非单调逻辑编程创建了一种重要的模 型语义一s t a b l e 模型语义,并在1 9 9 1 年将该模型语义扩展并更名为a l :l s w e l s e t 语 义,由此发展出一种重要的非单调逻辑编程技术一a n s w 盯s e t 编程技术。作为该类 编程技术的核心,a n s w e rs e t 语义相对其它非单调逻辑编程语义理论简洁明了,它 充分利用了逻辑编程领域的已有成果,有效地实现了逻辑程序的非单调推理。目 前,a i l c j w e rs e t 编程不仅被公认为一种重要的知识表示工具,而且是逻辑编程与非 单调推理领域的研究热点。 在对a l l s w e rs e t 编程理论进行了探索性研究基础上,取得了如下创新性成果: 1 提出了一种利用基于a r l s w e rs e t 语义的权约束编程实现策略冲突自动消 解的新方法。随着策略的广泛应用,关于其冲突消解的研究愈来愈受到重视。在 目前存在的多种途径中,采用逻辑编程完成冲突消解具有自动化程度高、逻辑严 谨等优点。但是,原有方法却存在被消解的冲突种类受限、优化机制单一等缺点。 为克服以上缺陷,在完成策略语法与语义形式化定义、冲突捕获机制定义、冲突 分类以及冲突消解特性分析的基础上,本文充分利用了权约束编程特有的集合选 择紧凑表示能力以及灵活的优化语句,完成了冲突消解权约束程序建立等工作。 该方法不但扩展了被消解的冲突种类,而且提供了更为合理和灵活的优化机制, 有效地克服了原有方法的缺陷。 2 提出了一种基于事件的w e b 服务组合新方法。随着电子商务的普及,有 关w 曲服务自动组合的研究愈来愈受到重视。目前主要存在基于仙知缸f i c i a li n t e l l i g e n c e ) 规划和诸如u m l ( u m f i c dm o d e l i n gl a n g u a g e ) 技术的两类途径。但是,由于 难以建立服务组合域,加之不完全信息的影响,因而前类方法难以实现,而后者 由于描述能力不足,因此无法满足用户的多样化需求。为获得一种既易于实现又 能满足用户多样化需求的服务组合的有效途径,本文在完成一种基于事件的服务 语言定义、用于描述服务组合的组合方案建立机制以及服务互斥性质分析的基础 上,通过a n s w e rs e t 编程表示组合方案,以获得实现组合服务目标的组合轨迹。 该方法充分利用了策略的动态执行能力和a n s w e rs e t 编程丰富的表示能力,不但 应该具有良好的应用前景而且能够满足用户的多样化需求。 3 利用a n s w e rs e t 编程完成了e r 模型( e n t i t y - r e l a t i o n s h i pm o d e l ) 的逻辑表 摘要 示。e r 模型是一种重要的语义数据模型( s e m a n t i cd a t am o d e l ) ,至今仍被广泛地应 用于数据库设计中。针对e r 模型的改进,目前主要存在基于图形表示和描述性逻 辑表示两种途径,但是,前者缺乏自动推理能力,而后者却存在表示能力弱、与 数据库兼容性不足等缺陷。为克服以上缺陷,本文在完成e r 模型分类研究、e r 模式语义与语法形式定义的基础上,利用a n s w e rs e t 编程完成了e r 模式的逻辑表 示。该方法不但为e r 模型提供了一种新的逻辑表示途径,而且有效地克服了基于 描述性逻辑表示途径的缺陷。更为重要的是,它还为利用e r 模式实现异构数据库 之间的语义协作提供了理论基础。 关键词a i l s w e l s e t ,语法,语义,冲突消解,服务组合,e l l 模型 i i a b s t r a c t a b s 眦c t m g e l f o n da n dv l i f s c h i t zc o l l a b o r a t i v e l ye s t a b l i s h e da ni m p o r t a n tk i n do fm o d e l s e m a n t i c s - - s t a b l em o d e ls e m a n t i c sf o rn o n m o n o t o n i cl o g i cp r o g r a m m i n gi n19 8 8 ,a n d e x p a n d e dt h i sm o d e ls e m a n t i c sa n dr e n a m e di ta sa n s w e rs e ts e m a n t i c si n19 9 1 b a s e d o nt h i ss e m a n t i c s ,a ni m p o r t a n tk i n do fn o n m o n o t o n i cl o g i cp r o g r a m m i n gt e c h n o l o g y - - - a n s w e rs e tp r o g r a m m i n gt e c h n o l o g yw a sd e v e l o p e d c o n s t r a s t e d 、砘t l lo t h e rs e m a n t i c s t h e o r i e so fn o n m o n o t o n i cl o g i cp r o g r a m m i n g ,a n s w e rs e ts e m a n t i c s ,t h ek e r n e lo f a n s w e rs e tp r o g r a m m i n gt e c h n o l o g y , i sc o n c i s ea n ds i m p l e ,a n df u l l yu t i l i z e st h ef r u i t s a c q u i r e db yt h el o g i cp r o g r a m m i n gc o m m u n i t y , a n de f f e c t i v e l yr e a l i z e sn o n m o n o t o n i c r e a s o n i n go ft h el o g i cp r o g r a m n o w a d a y s ,a n s w e rs e tp r o g r a m m i n gi sn o to n l yw i d e l y a c c e p t e da sa ni m p o r t a n tt o o lo fk n o w l e d g er e p r e s e n t a t i o nb u ta l s oar e s e a r c hf o c u so f t h el o g i cp r o g r a m m i n ga n dt h en o n m o n o t o n i cr e a s o n i n gc o m m u n i t i e s b a s e d0 1 1t h ei n v e s t i g a t i o no fa n s w e rs e tp r o g r a m m i n gt h e o r y , t h ei n n o v a t i v e c o n t r i b u t i o n si n c l u d e di nt h i st h e s i sa r cs u m m a r i z e da sf o l l o w s : 1 an e wm e t h o dw h i c hu t i l i z e sw e i g h tc o n s t r a i n tp r o g r a m m i n gb a s e do na n s w e rs e t s e m a n t i c st oa m o m a t i c a u yr e s o l v et h ep o l i c yc o n f l i c ti sp r o p o s e d a sp o l i c yb e i n gw i d e l y a p p l i e d , m o l ea n dm o 犯a t t e l l t i o ni sp a i dt ot h ep o k e yc o n f l i c tr e s o l u t i o n a m o n gc u r r e n t l y e x i s t i n ga p p r o a c h e s , t h ec o n f l i c tr e s o l u t i o nm e t h o d sb a s e do nl o g i cp r o g r a m m i n gh a v em e r i t so f l o g i c a lp l c c i s c n c s s ,h i g ha u t o m a t i z a t i o n , c t c w h e r e a s ,t h em e t h o d sm e n t i o n e da b o v eh a v e s h o r t c o m i n g s , s u c ha sl i m i t e dk i n d so fr e s o l v e dc o n f l i c t sa n dm o n o t o n i co p t i m i z a t i o n m e c h a n i s m t oo v e r c o m et h e s es h o r t c o m i n g sa b o v e , b a s e do na c c o m p l i s h m e n t so ft h ef o r m a l d e f i n i t i o no fs y n t a xa n ds e m a n t i c s0 fp o l i 瞩t h ed e f i n i t i o no fc o n f l i c tc a p t u r em e c l m i s m , t h e c o n f l i c tc l a s s i f i c a t i o na n dt h ea n a l y s i so fc o n f l i c tr e s o l u t i o nc b 锄c t e 瞩t h i st h e s i sf u l l yu t i l i z e s t h ec o m p a c tr e p r e s e n t a t i o nc a p a b i l i t yo fs e ts e l e c t i o na n df l e r d b l eo p t i m i t _ 痂o ns e n t e n c e so f w e i g h tc o n s t r a i n tp r o g r a n u n i n g , t oa c c o m p l i s ht h ec r e a t i o no fw e i g h tc o n s t r a i n tp r o g r a m s w h i c h 淝u s e dt or e s o l v ec o n f l i c t , e t c r n l i sm e t h o dn o to n l ye x p a n d st h ek i n d so fr e s o l v e d c o r r f l i c t sb u ta l s os u p p l i e sf l e x i b l ea n dm u l t i p l eo p t i m i z a t i o nm e c h a n i s m s , t h u si te f f e c t i v e l y o v e r c o m e st h es h o r t c o m i n g so f t h ep r e v i o u sm e t h o d s 2 an e ww r e bs e r v i c e sc o m p o s i t i o nm e t h o db a s e do i le v e n t si sp r o p o s e d 舡位 h l a b s t r a c t p r e v a l e n e eo fe l e c t r o n i cb u s i n e s s , m o r ea n dm o f ea t t e n t i o ni sp a i dt o t h ew e bs 硎c e s a u t o m a t i cc o m p o s i 6 0 nr e s e a r c h n o w a d a y s , t h e r ea r et w om a i na p p l o a c h e sa b o u tw e bs e l v i c 鹤 c o m p o s i t i o r lo n e i sb a s e do na i ( 蜥丘d a li n t e l l i g e n c e ) p l a n n i n ga n dt h eo t h e ri sb a s e d o nt h et e c h n o l o g i e s ,s u c ha su m lf o r t i f i e dm o d e l i n gl a n g u a g e ) w h e r e a s ,t h ef o r m e r i sh a r d l yr e a l i z e df o rt h ed i m c u l t yo fr e p r e s e n t a t i o no fs e r v i c e sc o m p o s i t i o nd o m a i n , a n dt h ei n f l u e n c eo fi n c o m p l e t ei n f o r m a t i o n t h el a t t e rc a l ln o ts a t i s f yt h em u l t i p l e r e q u i r e m e n t so f u s e r sf o rt h ei n s u f f i c i e n td e s c r i p t i o nc a p a b i l i t y t oo b t a i na ne f f e c t i v e a p p r o a c ht h a ti sa b l et os a t i s f yt h em u l t i p l er e q u i r e m e n t so f t h eu s e r sa n dc a l lb ee a s i l y r e a l i z e d ,b a s e do na c c o m p l i s h m e n t so fas e l v i c el a n g u a g eb a s e do ne v e n t s , t h em e c h a n i s mt o c r e a t et h ec o m p o s i t es c h e m aw h i c hi su s e dt od e s c n q o ec o m p o s i t es e l v i c 鹤a n dt h ea n a l y s i so f t h ee x c l u s i v es e r v i c e s d o p e r f i e s , t h i st h e s i su t i l i z e sa n s w e rs e tp r o g r a r r a n i n gt or e p r e s e n tt h e c o m p o s i t es c h e m at oo b t a i nt h ec o m p o s i t et r a j e c t o r yw h i c hr e a l i z e st h eo b j e c to fc o m p o s i t e s e r v i c e s t h i sm e t h o df u l l yu t i l i z e st h ed y :晌嘶c a 晦e x e c u t i n gc a p a b i l i t yo ft h ep o l i c ya n dt h e 翻p 磺;时v er e p r e s e n t a t i o nc a p a b i l i t yo fa n s w e rs e tp r o g r a n m a i n g , t h u s i ts h o u l dh a v ea9 0 0 d a p p l i c a t i o np r o s p e c ta n d c a ns a t i s f ym u l t i p l er e q u i r e m e n t so ft h eu s a 瞎 3 t h el o g i cr e p r e s e n t a t i o no f e rm o d e l ( e n t i t y - r e l a t i o n s h i pm o d e l ) i sa c c o m p l i s h e d b y a n s w e rs e tp f o 掣雒n r n j 】唔e rm o d e li saw e l l - k n o w ns e a r n a n t i od a t am o d e la n d y e tw i d e l y a p p l i e dt o t h ed a t a b a s ed e s i g n o m e n f l yt h e r e 锄t w om a i na p p r o a d l c sa b o u tt h e i m p r o v e m e n t sf o re r m o d e l o n ei sb a s 。do l lt h eg r a p h i c a lr e p r e s e n t a t i o na n dt h eo t h e ri sb a s e d o nt h ed e s c r i p t i o nl o g i cr e p r e s e n t a t i o n w h e r e , t h ef o r m e rh a sn o ta u t o m a t i or e a s o n i n g c a p a b i l i t y , t h e l a t t e rh a ss h o r t c o m i n g s , s u c h 勰t h ew e a kr e | 阻胬即c a p a b i l i t ya n d i n s u f f i c i e n tc o m p a t a s f l i t yw i t hd a t a b a s 已t oo v e r c o m e 峨幽0 f t o 蛐终b a s e do l l a c c o m p l i s h m e n t so f r e s e a r d a0 1 1t h ee r m o d e lc l a s s i f i c a t i o n , t h ef o r m a ld e f i n i t i o no f s y n t a xa n d s e m a n t i c so fe rs c h e m a , t h i st h e s i su t i l i z e sa n s w e rs e tp r o g r 锄m i n gt or e p r e s e n te rs c h e m a 1 1 l i sm e i l :l o dn o to n l ys u p p l i e sai 跏l o 百cr e p r e s 伽t a t i o na p p r o a c hf o re rm o d e l , b u ta l s o e f f e c t i v e l yo v e r e x ) m e st h es h o r t c o m i n g so ft h ea p p r o a c hb a s e do nt h ed e s c r i p t i o nb g i c r q x e s 踟t a t i o n m o r ei m p o r t a n t l y , t h i sw o r k sa b o v es u p p l yt h et h o o l x 五cb a s ef o ra p p l y i n ge r & 勃锄at 0 托a l i z et h es e m a n t i ci n t 删i l i t ya m o n gh e t e r o g e n e o u sd a t a b a s e 8 k e y w o r d :a n s w e rs e t , s y n t a x ,s e m a n t i c s ,c o n f l i c tr e s o l u t i o n , s e r v i c e sc o m p o s i t i o n , e r m o d e l i v 主要符号表 符号 u n 彗 彳b i 彳i a ( 盘l ,a 。) 或 v 1 n o t 3 v j 乒 c ( n ,后) 口 主要符号表 含义 集合并 集合交 集合包含 属于 不属于 集合b 相对彳的补集 集合a 的基数 空集 甩元元组 笛卡尔积 合取 析取 否定 缺省否定 蕴含 全称量词 存在量词 满足 不满足 组合数 语义等价 空目标 v i i i 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知,除了文中特别加以标注和致谢的地 方外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明 确的说明并表示谢意。 签名:痉叁日期:矿罗年石月罗日 关于论文使用授权的说明 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定,有权保留并向国家有关部门或机构送交论文的复印件和磁 盘,允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索,可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名:垃导师签名超! 璐 日期:d 罗年歹月罗日 第一章绪论 1 1 理论朔源 第一章绪论 a n s w e rs e t 编程【1 1 2 】【3 】是一种重要的非单调逻辑编程( n 伽m o n o t o i l i cl o g i c p r o g r a m m i n g ) 4 】【5 】【6 1 技术,而非单调逻辑编程是在融合逻辑编程( l o g i c p r o g r a m m i n g ) 7 】【8 】【9 1 与非单调推理科o n m o n o t i d i l i cr e a s o n i n g ) 1 0 1 1 1 理论基础上发展 而来的。 1 1 1 逻辑编程 & k o w a l s k i 1 2 】最早提出了基于逻辑的编程语言思想,世界上第一种逻辑编程 语言解释器被称为p r o l o g ( p r o g r a m m i n gi nl o g i c ) t 】,它是由八c o l m e r a u e r 及 其学生开发的,因此也可用p r o l o g 通指逻辑编程【1 4 1 。为区别诸如非单调逻辑编 程、析取逻辑编程( d i s j u n c t i v el o g i cp r o g r a m m i n g ) 1 5 1 6 1 以及演绎数据库( d e d u c t i v e d a t a b a s e ) 1 。7 】【1 8 】等逻辑编程技术,通常称由k o w a l s k i 等人创建的且基于h o r n 子 句( h o r nc l a u s e ) 的逻辑编程类型为h o r n 编程,相应的逻辑程序也被称为h o m 程序。 h o r n 子句也称为d e f i n i t e 子句( d e f i n i t ec l a u s e ) t 5 】【9 】,因此h o r n 编程也称为d e f i n i t e 编程。 更明确地说,初期逻辑编程中的逻辑应是数理逻辑( m a t h e m a t i c a li x ) g i c ) ,数理 逻辑也被称为符号逻辑( s y m b o l i cl o g i c ) 或现代逻辑( m o d e ml o g i c ) t 8 】【1 9 1 。为区别最 近几十年发展出来的多种逻辑,如多值逻辑( m u l t i v a l u e dl o g i c ) t 2 0 1 、模态逻辑 ( m o d a ll o g i c ) t 2 1 】【2 2 】以及认知逻辑( e p i 蜘i cl o g i c ) 【2 1 胆】等,人工智能( a r t i f i c i a l i n t e l l i g e n c e , a i ) 领域也往往称数理逻辑为经典逻辑( c l a s s i c a lt d g i c ) t s l t 6 】【8 】。 经典逻辑的起源最早可追溯到古希腊时期的亚里士多德( a r i s t o t l e ) 古典形式逻 辑和欧几里得( e u c l i d ) 几何,但其核心思想,即运用数学方法研究思维规律,却是 由莱布尼茨( gl e i b n i z ) 最早提出的。此后的近两百年为其初期发展阶段,在该阶段 中,取得的重要成果有逻辑代数、关系逻辑等,代表人物有布尔( gb o o l e ) 以及德 摩根( a d em o r g a n ) 等人。 从1 9 世纪中叶到1 9 4 0 年代是经典逻辑发展历史中极为关键的阶段。在该阶 电子科技大学博士学位论文 段,经典逻辑逐渐成长为- r j 新的独立学科,取得的重要成果可概括为以下五个 方面:( 1 ) 康托尔( gc a n t o r ) 集合论的创建,这为经典逻辑的发展奠定了坚实的理论 基础。( 2 ) 公理方法的发展,其代表是希尔伯特( d h i l b e r t ) 的几何基础。( 3 ) 逻辑 演算的建立。1 8 7 9 年弗雷格( f f r e g e ) 仓l j 建了谓词演算系统,并通过皮亚诺( q p e a n o ) 、罗素( b r u s s e l l ) 和怀特海( a w h i t e h e a d ) 等人的工作,建立了完整的古典形 式逻辑演算、命题演算和谓词演算系统。( 4 ) 证明论的提出和歌德尔( kg 6 d e l ) 定理。 1 9 3 0 年歌德尔提出了著名的完全性定理,该定理说明了形式系统可以从一阶谓词 演算中得到足够的基本工具。( 5 ) 语义理论的建立。1 9 3 4 年塔斯基( a t a r s k i ) 仓l j 建了 语义理论,并通过根岑( qg e n t z e n ) 等人的工作,为经典逻辑建立了完整的形式语 义理论。 在该阶段,还取得了两项对计算机科学有着重要意义的成果。 其一是h e r b r a n d 定理【2 3 2 4 。虽然h e r b r a n d 定理没有歌德尔定理有名,但是它 对自动推理理论却有着更为直接的意义。该定理明确指出对于任何不被满足的斯 柯伦范式( s k o l e mn o r m a lf o r t n t d a ) e 2 3 1 ( 或v 前束范式【1 9 】【2 4 】) ,总能够找到一个有限 的命题集是不可满足的,从而建立起了谓词演算与命题演算之间的内在联系。 其二是著名的丘奇一图灵定理( c h u r c h t u r i n gt h e o r e m ) t 2 3 1 。在1 9 3 6 年,丘奇 和图灵分别独立完成了希尔伯特判定问题的研究工作。希尔伯特判定问题可以描 述为:对于谓词演算中的任意一个语句( s e n t e n c e ) 0 7 和语句集r ,能否建立一个具 有正确判断国是否是r 逻辑结果( l o g i c a lc o n s e q u e n c e ) 能力的算法。丘奇一图灵定 理否定了该算法的存在,该定理指出,即使存在一个能够正确判断出国是r 逻辑结 果的所有情况的证明过程,但是却不存在一个能够正确判断出国不是r 逻辑结果的 所有情况的类似算法。另外,文献 2 5 】将丘奇一图灵定理称为塔斯基一丘奇一图灵 定理,并将该定理更为简洁地表述为“没有一种切实可靠的方法总能区分开真的数 论语句和假的数论语句”。丘奇一图灵定理意味着,设计万能计算机的想法只能是 徒劳,人们能够做到的是,找到那些既可判定的又有意义的语句子类。 自上世纪5 0 年代中期起,随着计算机的普及,研究人员开始从事谓词定理证 明过程的可计算性研究与实验。为解决其中的指数级空间复杂度问题,研究证明 只可能从以下两种途径出发: 1 简化谓词演算的表达式,并完成从面向人类逻辑到面向机器逻辑的转换。 首先,语法的简化无疑可降低计算复杂度。其次,以前的谓词演算形式是 为方便逻辑学家研究而定义的,这并不适合机器的计算特性。所以计算机 科学家们发展出了一种形式更为简洁的谓词演算一子句演算( c l a u s e 2 第一章绪论 c a l c u l u s ) t 8 2 6 1 。 2 加强推理规则的能力。早在1 9 6 0 年,m p r a w i t z 2 7 】就强调了合一 ( u n i f i c a t i o n ) 对谓词定理证明的重要性,但有效应用合一并产生深远影响 的则是j a r o b i n s o n 在1 9 6 5 年创建的消解限e 鲥嘶o n ) 推理机制【2 8 】( 2 9 】( 消 解也被译为归结【3 0 】) 。在消解机制中,基本推理规则如下: 二元消解g v p , h v l q ( g vj j l ) 盯 正因子 星2 垡 ( q v p ) o - 其中,仃是原子公式( a t o m i cf o r m u l a ) p 和g 的最一般合一者( m o s t g e n e r a lu n i f i e r , m g u ) 2 s 】【3 l 】。其基本推理方式是,对于任意一个不被满足 子句集,不断应用消解推理规则直到搜索到矛盾( 即空子句) 为止。 h e r b r a n d 定理确保了以上消解反演过程的完备性,即不断应用消解推理 规则总能够从一个不满足的子句集推导出矛盾。为提高效率,消解还采 用了重写( r e w r i t e ) 技术,文献【3 2 】对该方面知识作了全面的介绍。 r k o w a l s k i 1 1 1 、a c o l m e r a u e r 1 2 1 以及r o u s s e l 3 3 1 等人在上世纪7 0 年代开创 了一种重要的编程种类一逻辑编程。首先,与传统的过程式( p r o c e d u r a l ) 编程语言 不同,逻辑编程是陈述式的( d e c l a r a t i v e ) 。其次,逻辑编程体现了r k o w a l s k i 一贯 所倡导的“算法= 逻辑+ 控制的思想【1 1 】【蚓。最后,初期的逻辑编程- h o m 编程是基 于h o r n 子句的,而h o r n 子句( 即至多只包含一个否定文字的子句) 是一种子句 的简化形式,这就使得采用一种简化且高效的消解机制完成h o r n 程序推理成为可 能。 h o r n 编程研究领域的主要贡献可归纳为以下四个方面: 1 确定了语法结构。无论是h o r n 程序,还是非单调逻辑程序,所有类型的 逻辑程序均是由形如“胁耐卜占d 方力的规则构成的有限集。在 h e a d 卜b o a y 中,b o d y 是规则体( b o d yo f r u l 0 ,h e a d 是规则头( h e a do f r u l e ) ,符号“卜”表示逻辑蕴含。 2 建立了h o r n 程序的完整语义理论,并为逻辑编程语义研究奠定了理论分 析框架。1 9 7 6 年v a ne m d e n 和r k o w a l s k i 3 5 】完成了h o r n 程序的模型论 语义( m o d e l - t h e o r e t i cs e m a n t i c s ) 、不动点语义( f i x p o i n ts e m a n t i c s ) 和执行 语义( o p e r a t i o n a ls e m a n t i c s ) - - - 种语义定义,而且不仅揭示了以上三种语义 3 电子科技大学博士学位论文 的一致性,同时还证明了执行语义与证明论的一致性。至今,基于以上方 法的语义分析仍是逻辑编程的基本方式。 3 提出了s l d r e s o l u t i o n ( s l - r e s o l u t i o n 1 f o rd e f i n i t ec l a u s e s ) 推理机制 【5 】【8 】【9 】【3 7 1 。s l d r e s o l u t i o n 源自r h i l l 的l u s h r e s o l u t i o n ( l i n e a rr e s o l u t i o n 谢t hu n r e s t r i c t e ds e l e e t i o nf u n c t i o nb a s e do nh o r nc l a u s e ) 推理系绀3 8 】, 19 8 2 年经k a p t 和v a ne m d e n 提议【3 刀改为现名。s l d r e s o l u t i o n 是基于 r o b i n s o n 消解机制的,它不仅为实现h o r n 程序的执行语义提供了一种面 向目标的( g o a l - o r i e n t e d ) 、自顶而下的、切实有效的途径,而且也是多种 非单调逻辑编程理论的基础。 4 建立了p r o l o g 解释器并制定编程规范标准。 显然,h o r n 编程可看作一种谓词演算子系统,它是单调的( m o n o t o n i c ) ,其 s l d - r c s o l u t i o n 也只能推导出肯定结果( p o s i t i v ec o n c l u s i o n ) 。这就使得逻辑编程不 具备不完全信息( i n c o m p l e t ei n f o r m a t i o n ) 或不完全知识( i n c o m p l e t ek n o w l e d g e ) 的表 示与推理能力,其主要表现在以下两方面:( 1 ) 无否定( n e g a t i o n ) 或否定知识 ( n e g a t i v ek n o w l e d g e ) 表示与推理能力。例如,不具有从火车时刻表中推导出其中 隐含的否定信息( 即不存在某时某刻由a 地到达b 地的某次列车) 的能力;( 2 ) 无 析取结果表示与推理能力。例如,无法表示以下情况:张三可能是和尚也可能是 修道士,但总之他肯定未婚。因此,为增强逻辑编程的表示与推理能力,自上世 纪7 0 年代末,在h o r n 编程基础上逐渐发展出了非单调逻辑编程。 1 1 2 非单调推理 非单调推理的研究始于1 9 7 0 年代末。在m 领域中,一个被要求具有人类思 维能力的智能体( i n t e l l i g e n t a g e n t ) 必须能够处理关于其所在世界的不同形式的知识 与信念( b e l i e f ) ,并具备从已有信息中推断出更多新信息的能力,以做出决策、制 定规划以及采取行动等。因此,与逻辑学不同,a i 认可所有“合理的”( p l a u s i b l e ) 而 不是“无错的”( i n f a l l i b l e ) 推理方式。 更进一步地说,虽然逻辑学家坚持认为人类的推理应该服从经典逻辑的方式, 然而计算机科学家们却已经证明经典逻辑并未强壮到能够充分满足人类的推理方 式,即人类并不总是按照经典逻辑的方式推理,而往往是按照常识推理 ( c o m m o n s e n s er e a s o n i n g ) 跳到结果上( l e a pt oc o n c l u s i o n ) 的。按照常识推理,人们 1 s l r e s o l u t i o n ( l i n e a rr e s o l u t i o nw i t hs e l e c t i o nf u n c t i o n ) 3 6 1 。 4 第章绪论 往往倾向于诸如“没有更好的理由不相信这”或者“经验告诉我必是这样的”的陈述, 亦即人们往往是在不完全信息或不完全知识的状况下做出判断的。非单调逻辑的 目标就是建立一种能够模仿人类常识行为方式的推理系统。因而,它必须具有以 下两种能力:( 1 ) 能够跳到结果上;( 2 ) 当获得新信息或知识时,能够收 团( r e t r a c t ) 或废止( d e f e a t ) 已得结果。 常识推理思想是j m c c a r t h y 【3 9 】首先提出的,在1 9 6 9 年j m c c a r t h y 和p h a y e s 删通过情景演算( s i t u a t i o nc a l c u l u s ) 初步完成了常识推理的形式化工作,并提 出了著名的框架问题( f r a m ep r o b l e m ) 。概括地说,框架问题就是当作用只限于有限 对象的行动发生时,如何明确表示世界中那些未受影响的对象。例如,当打开吊 一灯时,该如何表示并未因此而改变的客厅颜色呢? 一种有效的途径是通过定义如 下缺省规则: 如果在情景s 中性质p 成立,则在s 中执行行动彳后的情景中p 也典型成立 ( t y p i c a l l yh o l d s ) 1 4 1 】 以解决框架问题。注意以上缺省规则中的结果是“典型成立”而不是“成立”。在经典 逻辑中,只能够完成对“成立”的表示与推理,而不可能完成“典型成立”的表示与推 理。因为“典型成立”意味着在新的情景中可能收回原有结果,即变为“非典型成立”, 而经典逻辑的一致性要求使得其不可能收回已得结果。 应该说p h a y e s l 4 2 】是最早认识到非单调推理存在的必要性的,但是最为明确且 系统地提出该问题的却是m m i n s k y 在其著名的af r a m e w o r kf o rr e p r e s e n t i n g k n o w l e d g e 【4 3 】一文中完成的。在该文中,m m i n s k y 揭示了这样一种重要现象: 当遇到一个新的情景( 或认识到现有问题发生了足够的改变后) 时,人们首先是 从记忆中选择一个足以称为框架的结构,并将之作为基本记忆结构( 或缺省知识) , 通过改变其中必要的细节以适应现实情景。关于利用经典逻辑解决框架问题,m m i n s k y 批判到:“逻辑推理( 即经典逻辑推理) 并不足以灵活到可以作为思考的基 础;我更愿意将它作为启发式方法的集合,只在应用于简单的规划中才有效。通 常逻辑( 即经典逻辑) 所绝对要求的一致性并不是有用的,甚至可能不是人们所 要的,因为一致性系统太弱。下文以r r e i t e r 著名的关于鸟的知识表示为例,进 一步说明以上思想。 首先,常识性概念鸟并不是一个数学概念,也就是说,它是不可能通过经典 的充分和必要条件完成定义的。如果将鸟定义为: 5 电子科技大学博士学位论文 v x ( b i r d ( x ) 暑a n i m a l ( x ) av e r t e b r a t e ( x ) b i p e d ( x ) a f e a t h e r e d ( x ) af l y ( x ) c h i r p ( x ) a ) 显然,该定义会被普遍存在的意外情况所推翻,例如,断了腿的猎鹰,再如,根 本就不具有飞翔能力的鸵鸟、企鹅等。其次,根据常识,人们会认为鸟应该是一 种脊椎动物、具有两条腿、能够飞翔等,即人们会缺省假设以上性质为真,这也 就是m m i n s k y 所说的框架。因此,可为鸟定义如下必要条件: i fb i r d ( x ) t h e na n i m a l ( x ) i fb i r d ( x ) t h e nv e r t e b r a t e ( x ) i fb i r d ( x ) t h e nt y p i c a l l yb i p e d ( x ) i fb i r d ( x ) t h e nt y p i c a l l yf l y ( x ) 注意,以上定义中,前两个性质是所有鸟

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论