（计算机科学与技术专业论文）区间逻辑的证明技术与工具.pdf

摘要 的深入，用于控制的计算机系统也越来越复杂。有一类系统，包括 制系统等，我们通常称之为妥全攸关系统( s a f e t yc r i t i c a ls y s t e m s ) ， 因为这些系统一旦发生故障必将导致灾难。然而，这些系统对实时性的要求很高，系统 的设计也十分复杂。正确地设计这些系统无疑是一巨大挑战。 形式化方法一将数学方法应用于软硬件的设计过程，被认为是一种行之有效的减少 设计错误的方法。其中很重要的个流派就是逻辑方法。在这种方法中，系统的需求和设计 都被描述为相应的逻辑公式。为了验证设计符合需求规范，我们只需证明形如“d e s 辛r e q ” 的蕴含式是逻辑系统的定理。但虽然如此，如果没有个有效的工具支持，仅借助于纸、 笔进行推导，则这样一项工作是既枯燥又易犯错的。实用工具的缺乏，限制了形式化方 法的更广泛的应用。这一点已为越来越多的学者所承认。 近年来，在实时系统的形式化规范和验证领域，一族实时区间逻辑，包括：m o s z k o w s k i 的区间时序逻辑的一个实时版本，周巢尘等的邻域逻辑、均值演算及时段演算等，正引 起人们越来越多的重视。这些逻辑采用了线性实区间作为基本的时间模型，可以很方便 地描述系统的时序上下文性质，具有很强的表达能力。然而这些逻辑在提出时均只给出 了公理系统，相关的适于机械化实现的证明系统却十分缺少。由于实时区间逻辑固有的 特点，传统的针对经典一阶逻辑和模态逻辑的证明理论和技术均不能有效地应用于这些 逻辑中。为了实现高效实用的形式化验证工具，对这些逻辑的定理证明技术的研究因而 成了形式化方法中个紧迫的课题：r 本文提出了新的带标记的相继式演算作为实时匿避翌鸳的藿奎适骂丞统e 它们的主 要特点在于：其基本对象已不再是单纯的公式，而是附加了标记信息的公式。此外，标 记相继式演算实质上包含了两部分：即布尔公式的推理系统和代数约束的推理系统。与 传统的相继式演算一样，它们只有很少的( 两条) 公理和一组非常结构化的规则。四种区 间逻辑的标记相继盎邃簋均只在少数基本算子的规则和代数约束的理论部分有稍微的差 别，这与它们彼此迥异的公理系统成了一个鲜明的对比。 、 f 标记相继式演算可以以目标制导的方式应用。在证明过程中，任何时候都可以根据 相继式公式最外层算子选择下一步的证明规则，将复杂公式分解为更简单的子公式。此 外由于伴随相继式的证明过程布尔公式和算术公式会逐渐分离，这使得我们可以应用最 适合各自特点的证明技术来验证它们。论文特别考察了一些算术约束公式类的自动判定 算法，并指出：标记相继式演算所涉及的绝大多数约束推理均可自动判定。上述事实都 意味着，利用标记相继式演算可以实现一个自动化程度相当高的定理证明工具。 论文的第二部分讨论了本文作者所实现的区间逻辑证明工具d c p 。d c p 是在个 通用的高阶逻辑框架中采用语义编码方式实现的，即用基逻辑来描述区间逻辑的语义， 区间逻辑中的公理和推导规则因而成为基逻辑中的可证的定理。采用语义编码技术而非 从头构造个全新定理证明工具的主要原因是，一则我们可以较快地得到一个可靠性有 用控应站机电算核着测叁 r e 保障的原型系统，- - n 我们可以将注意力更多地放在逻辑的证明系统和相关自动化技术 上。 为克服语义编码技术的缺点，我们实现了一组强有力的证明命令从而使得在d c p 中进行定理证明时不必下降到基逻辑而维持在区间逻辑的思维层次，产生的证明因而也 易于理解。尽管d c p 并非是全自动的证明工具，但它包含了很多实用技术以提高定理 证明的自动化程度。例如，d c p 采用了g e n t z e n 风格相继式演算作为基本证明系统，一 阶逻辑部分的证明很大程度上被自动化；d c p 中包含了很大的一个自动重写定理库， 大多数平凡的定理可以被自动证明，d c p 中还嵌入了实线性算术判定算法、逻辑子集 自动判定算法等，这大大方便了用户对实时系统的验证。通常用户只须在高层作一些决 策，其它大蠹琐碎的细节则由d c ：p 自动完成。借助于d c p ，我们验证了若干有趣的 应用实例，其中包括著名的煤气燃烧炉案例。这一实例本身尽管并不十分复杂，但对它 的验证却涉及了关于切割算子、积分算子的很多性质以及d c 归纳规则。 最后对论文的主要贡献作了总结，并探讨了一些可能的后续研究工作 i i a b s t r a c t n o w a d a y s ，c o m p u t e rc o n t r o l l e ds y s t e m sb e c o m ev e r yp o p u l a ri n o u re v e r y d a yl i f et h e c o m p l e x i t yo ft h e s es y s t e m sv a r i e s ：w h i l es o m e ( e g s i m p l ew a s h i n gm a c h i n e ) m a yb ev e r y s i m p l e ，s o m eo t h e r sa r es oc o m p l e xt h a t i tj s v e r yd i f f i c u l t t o g e t ad e s i g nw i t h o u te r r o r s a m o n gt h e ma r es a f e t yc r i t i c a ls y s t e m s t y p i c a le x a m p l e sa r en u c l e a rp o w e rs t a t i o nc o n t r o l s y s t e m s ，r o b o t s ，a i rt r a f f i cm o n i t o r i n gs y s t e m s ，a n ds 0o n a sa ni n c o r r e c to p e r a t i o no fs u c h s y s t e m sm a yp r o b a b l yc a u s eg r e a td a m a g e s o re v e nd i s a s t e r s t h ed e s i g no ft h e s es y s t e m st h e n p o s e ss e v e r ec h a l l e n g et ot h ec o m m u n i t y o f c o m p u t e rs o f t w a r es c i e n c e f o r m a lm e t h o d s a p p l y i n gm a t h e m a t i c a lm e t h o d st ot h el i f ec y c l eo fs o , w a r e ( a n dh a r d - w a r e ) a r ew i d e l 3 ra c k n o w l e d g e d a su s e f u lt o o l si nm i n i m i z i n gt h ee r r o r sd u r i n gt h ed e s i g np h a b e o n ei m p o r t a n ts c h o o lr a s e sl e 。g i ca 8ab a s i c t 0 0 1 i nt h i ss c h 0 0 1 b o t hr e q u i r e m e n t sa n dd e s i g n a r ed e s c r i b e da sl o g i cf o r m u l a s ，t h u s ，i no r d e rt oc h e c kw h e t h e rad e s i g ns a t i s f i e sr e q u i r e m e n t s ， o n eo n l yn e e d st op r o v et h a tt h ef o r m u l ao ft h ef o r m “d e s = r e q i sat h e o r e m h o w e v e r ，i n t h ea b s e n c eo fa r i g o r o u sv e r i f i c a t i o ne n v i r o n m e n t ，t h e o r e mp r o v i n g w i l lb eav e r yt e d i o u sa n d e r r o r - p r o n ew o r k i ti st h e l a c ko fp r a c t i c a lt o o l st h a th a sl i m i t e dt h ew i d e a p p l i c a t i o no ff o r m a l m e t h o d s r e c e n t l y i nt h ef i e l do ff o r m a ls p e c i f i c a t i o na n dv e r i f i c a t i o n ，af a m i t 3 7o fr e a l - t i m el a t e r - v a ll o g i c s ，i n c l u d i n gar e a lt i m ev e r s i o no fm o s z k o w s k i si n t e r v a lt e m p o r a ll o g i c ，z h o ue t c ：s n e i g h b o u r h o o dl o g i c ，m e a nv a l u ec a l c u l u s ，a n dd u r a t i o nc a l c u l u sa r eg i v e nm o r ea n dm o r e a t t e n t i o n t h e s el o g i c sh a v ea d o p t e d 。i n t e r v a l so fr e a l sa st h eb a s i ct i m em o d e la n dt h u sh a v e s t r o n ge x p r e s s i v e n e s s e s p e c i a l l y , t h e ya r eg o o da td e s c r i b i n gp r o p e r t i e sr e l a t e dw i t ht e m p o r a l c o n t e x t sw i t hm e a s u r e s h o w e v e r ，f o rt h e s ef o u rl o g i c s ，o n l ya x i o m a t i c ( o rh i l b e r t - s t y l e ) p r o o f s y s t e m sa r eg i v e nw h i c ha r ew e l l - k n o w nn o ts u i t a b l ef o rm e c h a n i c a lv e r i f i c a t 、i o nt o o l s o nt h e o t h e rh a n d ，d u et ot h e i ri n h e r e n tf e a t u r e s ，t h et r a d i t i o n a lp r o o ft h e o r ya n dt e c h n i q u e sd e v e - o p e df o rc l a s s i c a lf i r s to r d e rl o g i co rm o d a ll o g i cc a nn o tb ed i r e c t l ya p p l i e dt ot h e m h e n c e ，i t b e c o m e sa ni m p o r t a n tr e s e a r c hs u b j e c tt od e v e l o pp r o o ft e c h n i q u e ss p e c i a l l yf o rt h e s ei n t e r v a l l o g i c s i nt h i st h e s i s ，as e to fn e w l a b e l e d ( g e n c z e ns t y l e ) s e q u e n tc a l c u l ia r ep r e s e n t e df o rt h e s e l o g i c s t h e i rm a j o ri d e ai s t oc o n s i d e rl a b e l e df o r m u l a si n s t e a do fp u r eo n e sa sb a s i co b j e c t s t h el a b e l e dc a l c u l ie s s e n t i a l l yc o n t a i nt w ok i n d so fd i f f e r e n tr e a s o n i n gm e c h a n i s m s ，i e ，t h o s e f o rb o o l e a nf o r m u l a sa n da r i t h m e t i cf o f i n u l a sr e s p e c t i v e l y a si ss a m ew i t ht r a d i t i o n 缸s e q u e n t c a l c u l i ，t h e yc o n t a i nf e w ( t w o ) a x i o m sa n da s e to fs t r u c t u r e dr u l e s i nc o n t r a s tt ot h ed i 矗e r e n t a x i o m a t i cs y s t e m s t h ef o u rc a l c u l ih a v eo n l ym i n o rd i f f e r e n c ei nt h er u l e so fb a 矗j e 曩寰蠹b 羞酗o r a l g e b r a l ec o n s t r a i n tt h e o r i e s i i i l a b e l e ds e q u e n tc a l c u l im a yb eu s e di ng o a l - d i r e c t e dma ：u n e r a ta n yt i m e , t h ec u r r e n t p r o o fr u l em a yb ec h o s e ns i m p l ya c c o r d i n gt ot h eo u t e r - m o s to p e r a t o ro fs o m el a b e l e df o r m u l a d u r i n gt h ep r o o fp r o c e s s ，c o m p l e xf o r m u l a sw i l lb eb r o k e ni n t os i m p l e rs u b - f o r m u l a s + a l s o ， a r i t h m e t i cf o r m u l a s v i l lf i n a l l yb es e p a r a t e do u tf r o mt h eb o o l e a no n e s t h u sw ec a nl l s et h e m o s ts u i t a b l et e c h n i q u e st ov e r i f ye a c h m o r e o v e r as e to fa u t o m a t i cd e c i s i o np r o c e d u r e sh a v e b e e ns e l e c t e df o rc l a s s e so fa r i t h m e t i cc o n s t r a i n t s a 1 1t h e s ef e a t u r e si n d i c a t et h a tw i t hl a b e l e d s e q u e n tc a l c u l iw e c a n d e v e l o pq u i t ee f f i c i e n tm e c h a n i c a lt h e o r e mp r o v e r sf o ri n t e r v a ll o g i c s i nt h es e c o n dp a r to ft h et h e s i s ，w ed i s c u s st h ed u r a t i o nc a l c u l u sp r o v e r ( d c p ) t h a tw e h a v ed e v e l o p e da tu n u i i s t d c pi sam e c h a n i c a lv e r i f i c a t i o na s s i s t a n tf o rt h ef o u ri n t e r v a l l o g i c sm e n t i o n e da b o v e i ti si m p l e m e n t e du s i n gt h es e m a n t i ce n c o d i n ga p p r o a c hi nah i g h e r - o r d e rl o g i cf r a m e w o r kc a l l e dp v s t om a k ed c pp r a c t i c a l l yu s e f u l ，as e to fc u s t o m i z e dp r o o f c o m m a n d sa l ei m p l e m e n t e d w i t ht h e s ee o h i p a a l l 幽，l m e r s i d e a sa r em a i n t 出e di nt h ei n t e r v a l l o g i c sl e v e l ，a n dt h ep r o o f sg e n e r a t e da r es 谳i d rt ot h o s ep e n c i l - a n d - p a p e ro n e sa n dt h u se a s i l y r e a d a b l e ，t h o u g hd c pi sn o tf i d l ya u t o m a t i c ，m a n y u s e f u lp r o o f t e c h n i q u e sh a v eb e e na p p l i e d t oi m p r o v ei t sa u t o m a t i o n f o re x a m p l e ，ag e n t z e n s t y l ep r o o fs y s t e mi sa d o p t e dt h u sp r o o f so f t h e o r e m si nt h ef i r s to r d e rl o g i ca r eg r e a t l ys i m p l i f i e d t h a n k st ot h ea u t o m a t i ct e r mr e w r i t i n g t e c h n i q u e ，m a n yt r i v i a lt h e o r e m ss , r ea u t o m a t i c a l l yp r o v e do rs i m p l i f i e d m o r e o v e r ，t h ed e c i s i o n p r o c e d u r e sf o rt h el i n e a rr e a la r i t h m e t i ca n dt h ed e c i d a b l es u b s e to fd u r a t i o nc a l c u l u sa r e i n t e g r a t e d t h u su s e r su s u a u yo n l yn e e dt og i v ep r o o fs t r a t e g i e s 血t h eh i g hl e v e l w h i l et h el e f t p r o o fs t e p sc a nb ea u t o m a t e db yd c p w i t hd c p , w eh a v ev e r i f i e ds e v e r a li n t e r e s t i n gc a s es t u d i e s i n c l u d i n gt h ef a m o u sg a s b u r n e re x a m p l e t h eg a sb u r n e r e x a m p l e c a ni l l u s t r a t et h ep o w e ro fd c pb e s t i ti sn o tv e r y c o m p l i c a t e d ，y e ti t sp r o o f i sn o to b v i o u s ，r u l e sa b o u tc h o po p e r a t o r ：d o m sa b o u ti n t e g r a la n d a l s oi n d u c t i o nr u l e sh a v et ob eu s e dt ov e r i f yi t f i n a l l y , w es u m m a r i z ew h a tw eh a v ea c h i e v e da n d d i s c u s sp o s s i b l ef u t u r ew o r k i v 第一章绪论 随着计算机应用的深入，用于控制的计算机系统也越来越复杂。有一类系统，包括 飞行监测、核电站控制系统等，我们通常称之为安全攸关系统( s a f e t yc r i t i c a ls y s t e m s ) ， 因为这些系统一旦发生故障必将导致灾难。然而，这些系统对实时性的要求很高，系统 的设计也十分复杂。正确地设计这些系统无疑是一巨大挑战。 形式化方法一将数学方法应用于软硬件的设计过程，被公认为是一种行之有效的减 少设计错误的方法。其中很重要的一个流派就是逻辑方法。在这种方法中，系统的需求 和设计都被描述为相应的逻辑公式。为了验证设计符合需求规范，于是我们只需证明形 如“d e s 辛r e q 的蕴含式是逻辑系统的定理。然而，如果没有一个有效的工具支持，仅 借助于纸、笔进行推导，则这样一项工作是既枯燥又易犯错的。实用工具的缺乏，限制了 形式化方法的更广泛的应用。这一点已为越来越多的学者所承认。 为了实现高效实用的形式化验证工具，适于计算机应用的证明理论和技术是必不可 少的。在过去的半个世纪中，尽管自动定理证明领域已取得十分丰富的成果，但这些成 果大多都是针对经典逻辑。而用于形式规范和验证的通常是一些特殊设计的应用逻辑， 已有技术往往不能很好地支持这些逻辑的定理证髓。在本论文中，我们研究了一族区间 逻辑的定理证明技术以及在通用的高阶逻辑框架中实现相应的机械化证明工具的方法。 1 1 本文的研究对象 时序逻辑( t e m p o r a ll o g i c ) 已经成为数学家、哲学家以及计算机科学工作者们共同关 注的一个热门研究学科。在程序验证中，时序逻辑也是一个常用的工具。单从字面上看， 时序逻辑可以简单地理解为关于时间的逻辑。根据人们对时间本质的不同认识，时序逻 辑可以分为： 线性时间或分支时间( 1 i n e a rt i m e o rb r a n c h i n gt i m e ) 时间是线性或是分支的? 线性时间观认为任一时刻存在唯一的将来，j 而在分支时间 观中时间结构是树形的，即任_ 时刻均可延伸出若干不同的将来线性时序逻辑的 代表是命题线性时序逻辑( p r o p o s i t i o n a ll i n e a rt e m p o r a ll 0 舀c ，p t l ) 1 ，分支时序逻 辑的代表是计算树逻辑( c o m p u t a t i o n a lt r e el o g i c ，c t l ) ”。关于线性分支时序逻 辑孰优孰劣的问题，e m e r s o n 和l a m p o r t 等人之间曾有过长时间的辩论，最终的结 论是两者各有所长。例如分支时序逻辑适合描述非确定行为，而线性时序逻辑则更擅 于描述进程的并发性质。 离散时间或连续时间( d i s c r e t et i m eo rc o n t i n u o u st i m e ) 时间是离散或是连续的? 对于这一问题，通常人们容易达成共识，连续的时间观显然 更自然。当然，离散的时间模型作为一种简化，有其自身的应用但对更复杂的应用 如实时系统( r e a l - t i m es y s t e m s ) ，混合系统( h y b r i ds y s t e m s ) ，越来越多的人倾向于聚器 连续( 实时) 时问模型 2第一章绪论 基于点或基于区间( p o i n tb a s e do ri n t e r v a lb a s e d ) 时间是由点或区闻组成的? 反映到逻辑中，基于点或区间的逻辑根本不同点在于公 式的语义是解释在点或区间上传统的时序逻辑大多是基于点的但这并不能说明点 作为时间的基本构件更合理可能的一个原因是：基于点的逻辑如p t l ，c t l 与古老 的自动机理论有着密切联系。由于教育的原因人们更易于接受基于点的逻辑。早期对 时序逻辑的研究也主要集中这一类逻辑上。本世纪来，越来越多的人相信“区间是更 基本、更具体的时间单位，而点则是可由区间构造出的抽象实体”【2 ，第1 1 7 页l 。甚至还 有人认为“点从来不真正存在，。相应地，对区间逻辑的研究也正活跃起来。我们相 信两种逻辑各有优缺点，没有一种逻辑能够适应所有的应用 、 本文的研究对象是基于区间的线性实时时序逻辑。具体说，本文将只讨论一族实时区 间逻辑，包括：m o s z k o w s k i 的区同时序逻辑f 3 】( i n t e r v a lt e m p o r a ll o g i c ，i t l ) 的一个实时版 本f 4 j ，周巢尘等的邻域逻轷5 j ( 肫神概施d 蛳gn l ) ，均值演算i s ( m e a nv a l u ec a l c u l u s , m v c ) ，及时段演算用( d u r a t i o ng a l e u l s , d c ) 。特别地，本文着重于从计算机科学的角度 研究这一族区间逻辑的定理证明技术及机械化辅助证明工具的实现技术。 1 2 区间逻辑 尽管人们对区间逻辑( i n t e r v a ll o g i c s ，砒e r v a ! b a s e dt e m p o r a ll o g i c s ) 的研究远远不如对 基于点的逻辑的研究那样深入，我们还是可以在文献中找到为数不少的相关研究工作 随着计算机应用领域的拓广，不断有新的区间逻辑被提出下面我们有选择地列举关于 区间逻辑的若干研究工作： v a nb e n t h e m ， 8 lg a l t o n ，【9 jh u m b e r s t o n e ，f 1 0 lr s p e r 1 1 】等分别从 语言学、哲学角度研究了关于区间的模态逻辑；文削t 2 - t s l 等从逻辑、数学的角度探讨了 区间逻辑j 计算机科学领域的相关工作有 6 , 7 , 1 6 - 1 8 】等，此外区问逻辑与进程逻辑之间的密 切联系也已被发现【肛2 l 】。 大多数区间逻辑都包含了一称为切割( c h o p ) 的二元模态词一和一度量区间长度的 特殊符号z 。如公式a ，、b 在区间i 上为真的含义是区间i 可以切割成前后两个相邻的子 区间五k ，并且a ，曰分别在区间五k 上为真。因此，对于某些性质，例如，嚏在任长 于f 的观察区间上总为真”，“在任何a 为真的区间上，b 在前半部分成立，而g 恰在 后半部分为真”等，使用区间逻辑来描述、推导显然更方便、更自然。特别是在描述关于 时序上下文性质时，区间逻辑明显要强于基于点的逻辑如下的例子尽管并非源自具体 的实际应用，但多少体现了这一点。 例子1 1 令p ，q ，r 表示一系统的可观察信号，该系统的时序行为受如下条件约束： 1 p 初始为假； 2 对任一p 持续为真的极大有穷区闻，若g 在该区闻的右端持续为宾，则在该区间内 任一处，q 为宾当且仅当r 为假。 1 3 证明系统概述 述行为规范如果用命题时序逻辑来描述将不得不使用深度嵌套的u n t i l 算子。在下 面的公式中，u ，“分别表示弱、强u n t i l 算子jp r e c e d e 算子p 定义为：p p q 皇，( p u g ) 。 为了便于阅读，我们将该公式以二维平面方式写出： 1 p 口 p u f ( q u i p ) 、| 1 p “i 二ji 辛 i ( g 铮、r ) u p ( 1 。1 ) 尽管公式l _ l 确实正确地描述了系统的行为，但这一点并不是显而易见的，层层嵌套 的u n t i l 算子使得上述规范公式很难理解。而主要原因是p t l 这一类基于点的时序逻辑 既没有“区间”这一语义摄念，又不包含自然地描述这一概念的语法结构，“极大p 持续 为真的区闻这一概念很难简洁地表达出来。 区间逻辑允许自然的图形表示，这使得用区间逻辑描述的规范直观易读的多。例如， 时段演算直接提供了描述信号p 在区间上( 几乎) 处处为真的语法结梅一函 。利用这一 结构以及切割算子，我们可以很快写出描述上述系统行为的如下规范公式： m 刚0 、一( 。鬻1 卜、 ( 1 2 ) 区闻逻辑已在许多领域找到成功应用，而且其应用领域还在不断扩大。区间逻辑的 部分典型应用包括： 计划( p l a n ) 2 2 自然语言理解 2 3 1 程序( 实时系统) 规范与验证【2 4 衢j 硬件电路设计2 1 多媒体【2 s 1 1 。3 证明系统穰述 逻辑的主要用途是推导。自然地，各种不同的证明过程成了逻辑研究的重要内容。 文献中出现过不少证明系统。其中，最重要的有如下几种：公理系统( a x i o m a t i cs y s t e m s ， 0 1 ：h i l b e r ts y s t e m s ) ，自然演绎法( n a t u r a l d e d u c t i o n ) ，消解( r e s o l u t i o n ) ，表方法( t a b l e a u m e t h o d ) 和相继式演算( s e q u e n tc 出曲) 。 4第一章绪论 公理系统是最古老、最普遍的一种证明系统。对某些非经典逻辑，很可能仅存在公 理系统。公理系统通常包括一组公理和较少的几条推导规则。在这一系统中，证明是满 足特定条件的公式序列，序列中的每一公式或者是已知公理之一，或者可以由出现于它 之前的公式应用推导规则变换得到。 对自然演绎法的研究可以归溯到g e n t z e n 和f i t c h 等的开创性工作【2 9 , 3 0 。自然演 绎法的主要目的是将人们习惯的非形式化推导形式化。它主要基于从属证明( s u b o r d i n a t e p r o o 也) 的思想：首先从某些前提出发推导出特定结论，然后去掉前提得到无假设的结论。 例如，假定由假设a 出发可以推导出b ，则我们可以去掉前提得到ajb 。 公理系统和自然演绎法属于前向( f o r w a r d ) ”或“自底向上( b o t t o m u p ) ”证明系统。 这一类系统的最大缺点在于证明过程的每一步所能推导出的中间结论成指数级增长，它 们本身实际上不能为证明或否证公式提供任何启发。在这一类系统中推导过于依赖人们 的经验，有时尽管最终的证明并不长，但找到这一证明仍有可能十分困难。因而前向系 统并不十分适合应用于计算机辅助的( 半) 自动化证明工具中。 消解系统【3 1 和表方法1 3 2 】都是基于短句( c l a u s e ) 的证明系统。消解与合取正规范式 ( 或短句范式) 相关，表方法则与析取正规范式( 或对偶短句范式) 相关。在消解和表方法 中，定理证明均是反驳的过程( r e f u t a t i o n a lp r o c e d u r e ) 。换言之，为证明a ，我们从一a 出 发构造一矛盾。首先通过一系列消解或表扩张规则( e x p a n s i o nr u l e s ) 将其变换为短句集。 对于表方法，每个表都是一棵树，扩张规则逐步将树展开。若树的任一分支都存在某短 句x 及其否定，x ，则我们得到一矛盾。消解系统采用了一特殊的消解规则，证明即是 不停应用这一规则直至得到矛盾一空短句。 g e n t z e n 的相继式演算可以看作是自然演绎与表方法的中介。文献中相继式演算有时 也被指为自然演绎法，丽事实上两者均可以在g e n t z e n 的经典论文l 别中找到。相继式演 算与表方法的密切联系体现在大多数相继式演算的完备性问题被归结为对应的表系统的 完备性问题。在文 3 3 , 3 4 j 中，m i n t s 指出了相继式演算与模态消解( m o d a lr e 珥o l u t i o n ) 之间 的紧密联系。类似地，f i t t i n g 3 5 】给出了表方法，d a v i s p u t n a m 过程1 3 6 】及模态消解之间 的联系。 消解，表方法及相继式演算都是晤向( b a c k w a r d ) ”或“目标制导( g o a l d i r e c t e d ) ”的 证明系统。在这一类系统中，证明搜索可以以系统化的方式进行，因此它们较适于( 半) 自动化的机器定理证明工具中。消解技术通常更适合于自动化程度非常高的定理证明工 具( 如o t t e r 3 7 ) ) ，而相继式演算或表方法则适合于自动化不是非常高并且可能经常需要 用户交互的证明工具( 如p v s s s , 删) 。消解技术的一大“缺点”是待征公式必须首先转换 成短旬范式1 ，这过程破坏了公式结构并经常造成一庞大无比的短句集。对于具有很高 自动化证明程度的逻辑，由于消解规则基本上由计算机选择应用，上述缺点”并不构成 任何闯题。而当逻辑不可判定，用户的交互不可避免时，庞大的短句集往往意味着大障 1 尽管存在非短句的消解( n o n - d a u s a ir e s o l u t i o n ) 技术，大多敦实现都采用了首先完全转换劐短句范式再应用悄解 规朋的方法 i 4g e n t z e n 的相继式演算 碍。因为我们所感兴趣的四种区间逻辑都是不可判定的。在证明过程中，用户经常需要 与证明工具交互，所以本文将着重考虑g e n t z e n 风格的相继式演算。对于命题逻辑，相继 式演算( 或表方法) 同样也可以得到自动判定过程，尽管这一过程未必总有消解技术那么 高效但是已经知道一些工程上的技术i 舡诏】可以进一步提高它的效率。 1 4 g e n t z e n 的相继式演算 本节将对g e n t z e n 的相继式演算作一简单介绍。我们用大写的希腊字母如r 和来 表示有穷( 可能为空) 公式集。相继式( s e q u e n t ) 是一有序对偶( r ，) ，这里r 称作相继式 的前件( a n t e c e d e n t ) ，丽a 称作后件( s u c c e e d e n t ) 。通常我们引入一特殊符号“o ”而把相 继式表示成f - 。为简洁起见，我们用记号r ， 及一分别表示r u a ) 和d _ 。 以规则号- 为例，相继式演算中的推导规则具有如下形式： i _ ，ar ，b 斗 了j 乃f 彳万一 横线以上的零个或多个相继式称作是前提( p r e m i s e ) ，以下的称作结论( c o n c l u s i o n ) 。 其中a 辛b 称为主公式( p r i n c i p a lf o r m u l a ) ，a ，b 为从公式( s i d ef o r m 山) ，而r ，则称 为参数公式( p a r a m e t r i cf o r m u l a ) 。前提为空的规则即相继式演算的公理。相继式演算通 常包含很少的公理和一组非常结构化的规则。在公理系统中，证明是一公式序列。对于相 继式演算，证明是一相继式树，其所有叶节点都是公理，而中间节点与其子节点正好是 某规则的结论和前提。推导即是始于根的逐步构造证明树的过程。公式a 是相继式系统 的定理当且仅当相继式一a 存在证明。下面我们介绍一阶逻辑的一个相继式演算： 逻辑规则( 1 0 9 i c a ln l l e 矿) 逻辑规则包括同性公理和c u t 规则。c u t 规更j 是在证明过程中引入分情形的一种 机制：例如在r 一上应用规则产生两个子目标r ，且一和i 、_ ，且，后者可以 看作是在个分支上假设a ，而在另一分支上假设，a 。强大的c u t 规则通常能极 大地缩短证明长度，但这规则破坏了子公式性质。对于命题及谓词逻辑，c u t 规则 已知是冗余的。 ( i d e n t i t y )a _ + a ( c u t ) _ 二下j 五。 结构规则( s t r u c t u r a ln l l e ) 在早期的论文中，相继式中的前件和后件均表示为公式的有穷序列。结构规则使得 我们可以重新组织相继式。如通过e x c h a n g e 规则交换相继式中某两个相邻公式的位 置；通过收缩( c o n t r a c t i o n ) 规则引入某公式的多次出现等。当前、后件表示为有穷 公式集时，只有如下单调性( 或削弱w e a k 衄i n g ) 规则是必须的了。 ( m o n o t o n i c i t y ) 年= ；蓄 若有一p 及。 逻辑规则诃掘可能会产生歧义事实上，在一些文献中j 后享的操作提鲥被指为逻辑规剐，而c u t 规则被划蓟 结构规则中我钔这里所甩的分类怯由珏e h 蝻也w a n m 醒给出 操作规则( o p e r a t i o n a ln d 铅) ( 辛一+ ，笔掣 r ，a ，b - + ( 一) f , 二二a 二a b - - 一 a ( v 一+ ) 譬杀群 ，1 1 - - + a ，a 、 一叶) f = 百= 毒五 、r ，忱a ( 。) ，a ( 口) _ a 一+ ) 二i 可蠢丢i 茅 ( - 手寺) ( - a ) ( 叶v ) - 一) ( - v ) 第一章绪论 工，a - ，b p _ a j b r 斗，ar + a ，b f - a a b r _ a ，a ，b r _ j 4 v b r ，a _ r 斗1 a ! ! 兰堕! ! 垒 r _ v z ，a ( ，a r ，a 扫) - + i - 知a ( z ) ，a ( 疗) ， q _ ) r 聂j 两j 五i - + j j f 了五面瓦五一 关于量词的规则v - + ，_ v ，j 斗，- j 带有额外的约束条件：其中8 是对写在a 中自由的 项，而p 是从未出现过的s k o l e m i z a t i o n 常量。 相继式演算目前已被许多经典逻辑的证明工具所采用。但在非经典逻辑中，相继式 演算的应用却相当少。根据w a a s i n g 在e s s l l i 9 4 讲座中的说法，尽管已有一些工作将 g e n t z e n 的方法扩充到模态逻辑，姆d o e n 的高级相继式( k i g l l e r - l e v e ls e q u e n t s ) 4 3 l m a s i g i 的高维楣继式( h i g h e r - d i m e n s i o n a l s e q u e n t s ) 4 4 】；b e l a a p 等的显示逻辑( d i s p l a y l o g i c ) 4 5 】等， 但“它们并未真正繁荣起来”。特别地，这些扩充主要是针对模态算子口，。就作者所 知，这些方法还不能处理区间逻辑的切割算子及邻域模态词。 1 5 相关研究工作 在过去的三、四十年中，经典一阶逻辑的推导技术一直是自动定理证明研究团体的 最主要目标。至今，一阶逻辑的定理证明技术已相当丰富。但对于一阶逻辑以外的其它 逻辑如时序逻辑，情形并非如此。具体到我们所感兴趣四种实时区间逻辑，我们还不知 道是否有任何已完成或正在进行的工作。对于时序逻辑的定理证明技术，大体有如下几 种途径： l l 公理系统 当逻辑的公理