首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到19条相似文献,搜索用时 140 毫秒
1.
不同逻辑间翻译的逻辑性质   总被引:2,自引:0,他引:2  
如果考虑逻辑间模型的翻译并且一个逻辑的模型类被翻译为另一个逻辑的模型类的真子类,那么可靠的(the soundness)和完备的(the completeness)翻译可以将不可满足的公式翻译为可满足的公式.针对上述问题,该文提出了语义忠实(the faithfulness)和语义满(the fullness)两条逻辑性质来确保可满足的公式翻译为可满足的公式,不可满足公式翻译为不可满足公式.该文例证了二阶逻辑在标准语义下到一阶逻辑的翻译是语义忠实的但不是语义满的,在Henkin语义下是语义忠实的和语义满的.  相似文献   

2.
申宇铭  王驹  唐素勤  蒋运承 《软件学报》2012,23(9):2323-2335
对应物理论(counterpart theory)是一阶逻辑的一种理论.Lewis利用谓词模态逻辑到对应物理论的翻译来研究谓词模态逻辑的性质,但是Lewis的翻译存在把不可满足的公式翻译为可满足公式的情况针对这个问题,提出了一种扩展语义的谓词模态逻辑,建立了扩展语义后谓词模态逻辑模型与对应物理论模型的一一对应关系,并在此基础上建立了谓词模态逻辑到对应物理论的语义忠实语义满翻译(faithful and full translation),其可确保将谓词模态逻辑的可满足公式和不可满足公式分别翻译为对应物理论的可满足公式和不可满足公式.由对应物理论是可靠的、完备的一阶逻辑的理论且语义忠实语义满翻译保持可靠性和完备性,进一步证明了扩展语义的谓词模态逻辑也是可靠和完备的.  相似文献   

3.
从ER模式到OWL DL本体的语义保持的翻译   总被引:14,自引:0,他引:14  
许卓明  董逸生  陆阳 《计算机学报》2006,29(10):1786-1796
提出了一种从ER模式到OWL DL本体的语义保持的翻译方法.该方法在形式化表示ER模式的基础上,建立ER模式和OWL DL本体之间精确的概念对应,通过一个翻译算法按照一组预定义的映射规则实现模式翻译.理论分析表明,该方法是语义保持的和有效的;算法实现和案例研究进一步证实,完全自动的机器翻译是可实现的.该文方法是原创性的,为Web本体的开发以及数据库和语义Web之间语义互操作的实现开辟了一条有效途径.  相似文献   

4.
描述逻辑是语义网的理论基础,首先通过对语义Web服务中的输入/输出参数进行抽象描述,依据描述逻辑理论得到语义Web服务的形式化定义。从描述逻辑的角度把语义Web服务映射成某一领域中的概念,把语义Web服务的组合看成是一个新的语义Web服务的形成,新服务形成后是否有意义其实就是描述逻辑中新概念的满足性问题。通过引入Tableau算法,证明了新语义Web服务的可终止性,并给出了语义Web服务满足性的可判定过程。这一工作为具体语义下的Web服务的发现、组合等问题的解决提供了理论基础,具有十分重要的指导作用。  相似文献   

5.
面向语义Web语义表示的模糊描述逻辑   总被引:1,自引:0,他引:1  
蒋运承  史忠植  汤庸  王驹 《软件学报》2007,18(6):1257-1269
分析了语义Web语义表示理论的研究现状及存在的问题,提出了一种新的面向语义Web语义表示的模糊描述逻辑FSHOIQ(fuzzy SHOIQ).给出了FSHOIQ的语法和语义,提出了FSHOIQ的模糊Tableaux的概念,给出了一种基于模糊Tableaux的FSHOIQ的ABox约束下的可满足性推理算法,证明了可满足性推理算法的正确性.提出了FSHOIQ的TBox扩展和去除方法,并证明了FSHOIQ的TBox约束下的包含推理问题可以转化为ABox约束下的可满足性推理问题.FSHOIQ为语义Web表示和推理模糊知识提供了理论基础.  相似文献   

6.
语义网的一阶逻辑推理技术支持   总被引:2,自引:0,他引:2  
徐贵红  张健 《软件学报》2008,19(12):3091-3099
研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.  相似文献   

7.
Statecharts的组合语义与求精   总被引:4,自引:0,他引:4  
朱雪阳  唐稚松 《软件学报》2006,17(4):670-681
由于简洁、直观的表达能力,Statecharts被用于许多反应系统的行为建模.Statecharts可表示不同抽象层次的系统行为,因而可用来表示逐步求精建模中各步的结果.但对于求精过程中下层是否保持了上层的语义、所建模型是否满足某些性质的问题,却难以在其自身的框架下进行讨论.在这方面,形式化语言XYZ/E可与其互补.XYZ/E是一种可执行线性时序逻辑语言,既可表示系统的性质,又可表示系统的行为.递归地在基本迁移系统上解释Statecharts语义,用XYZ/E公式表示它的时序语义.这一语义是模块级可组合的.求精过程的语义保持,可直接从语义定义得到保证.Statecharts所描述的系统行为模型和性质在同一个逻辑中表示,因此,系统行为是否满足所需性质的问题可由逻辑蕴涵式表示.  相似文献   

8.
陈遥  朱跃龙  冯钧 《计算机工程》2008,34(11):200-202
介绍针对信息提取的机器翻译模型,分析该模型下基于语法分析的水情电报翻译系统及存在的问题。采用机器翻译中语义分析技术解决问题,利用语义信息提高翻译率。用逻辑语义建立水情电报的逻辑语义模型,结合语义信息实现对几种类型错报的翻译,由此提出基于语义的水情电报翻译模型。对系统的评价与分析结果表明,翻译率即自动化程度得到了提高,报文的不可翻译率从2%~5%降到0.96%左右。  相似文献   

9.
循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决.分析了描述逻辑循环术语集的研究现状和存在的问题,基于混合μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCIO中,提出了一种允许包含循环术语集的描述逻辑μALCIO.给出了μALCIO的语法和语义,证明了μALCIO的可满足性推理等价于混合μ-演算的可满足性推理,并利用树自动机理论给出了μALCIO的可满足性推理算法以及给出了推理算法正确性证明和复杂性定理.  相似文献   

10.
郭昊  曹钦翔 《软件学报》2022,33(6):2127-2149
霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.  相似文献   

11.
12.
Skolemization is not an equivalence preserving transformation. For the purposes of refutational theorem proving it is sufficient that skolemization preserves satisfiability and unsatisfiability. Therefore there is sometimes some freedom in interpreting Skolem functions in a particular way. We show that in certain cases it is possible to exploit this freedom for simplifying formulae considerably. Examples for cases where this occurs systematically are the relational translation from modal logics to predicate logic and the relativization of first-order logics with sorts.  相似文献   

13.
This paper concentrates on comparing the expressive powers of five non‐monotonic logics that have appeared in the literature. For this purpose, the concept of a polynomial, faithful and modular (PFM) translation function is adopted from earlier work by Gottlob, but a weaker notion of faithfulness is proposed. The existence of a PFM translation function from one non‐monotonic logic to another is interpreted to indicate that the latter logic is capable of expressing everything that the former logic does. Several translation functions are presented in the paper and shown to be PFM. Moreover, it is shown that PFM translation functions are impossible in certain cases, which indicates that the expressive powers of the logics involved differ strictly. The comparisons made in terms of PFM translation functions give rise to an exact classification of non‐monotonic logics, which is then named as the expressive power hierarchy (EPH) of non‐monotonic logics. Three syntactically restricted variants of default logic are also analyzed, and EPH is refined accordingly. Most importantly, the classes of EPH indicate some astonishing relationships in light of earlier results on the expressive power of non‐monotonic logics presented by Gottlob as well as Bonatti and Eiter: Moore’s autoepistemic logic and prerequisite‐free default logic are of equal expressive power and less expressive than Reiter’s default logic and Marek and Truszczyński’s strong autoepistemic logic. This revised version was published online in June 2006 with corrections to the Cover Date.  相似文献   

14.
First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use. Partially supported by EPSRC project: Analysis and Mechanisation of Decidable First-Order Temporal Logics (GR/R45376/01).  相似文献   

15.
对称逻辑公式在L*3逻辑度量空间中的分布   总被引:1,自引:0,他引:1  
在三值逻辑系统L*3中引入了对称三值R0函数的概念,在此基础上给出了对称逻辑公式和准对称逻辑公式的定义.研究了在逻辑等价意义下对称逻辑公式的性质,给出了L*3和经典逻辑系统L中对称逻辑公式之间的关系及其计数问题,证明了n元对称逻辑公式占全体n元逻辑公式的比例随n的增大而趋向于零,且全体对称逻辑公式的真度之集却在[0,1...  相似文献   

16.
17.
基于中心语块扩展的短语对齐   总被引:1,自引:0,他引:1  
短语等价对在词典编纂、机器翻译和跨语言信息检索中有着广泛的应用.提出了一种新的短语对齐方法,使用可信度较高的词典对齐结果来抽取源语言短语的译文中心语块,依据译文扩展可信度来确定源语言短语的译文统计边界.从译文中心语块出发,结合译文统计边界生成源语言短语的所有候选译文.对候选译文进行评价,从中选出最可靠的译文.同时利用贪心算法消除源语言短语译文边界之间的交叉冲突.实验结果表明,所提出的方法在开放测试中其正确率达到了82.76%,性能好于其他方法.  相似文献   

18.
Deciding Regular Grammar Logics with Converse Through First-Order Logic   总被引:1,自引:0,他引:1  
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators.  相似文献   

19.
This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant–contravariant simulation and the partial bisimulation preorders over labelled transition systems. It is shown that there are mutual translations between modal transition systems and labelled transition systems that preserve, and reflect, refinement and the covariant–contravariant simulation preorder. The translations are also shown to preserve the modal properties that can be expressed in the logics that characterize those preorders. A translation from labelled transition systems modulo the partial bisimulation preorder into the same model modulo the covariant–contravariant simulation preorder is also offered, together with some evidence that the former model is less expressive than the latter. In order to gain more insight into the relationships between modal transition systems modulo refinement and labelled transition systems modulo the covariant–contravariant simulation preorder, their connections are also phrased and studied in the context of institutions.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号