共查询到20条相似文献,搜索用时 250 毫秒
1.
2.
可计算性(Computability)即算法有解性,是数学和计算机科学领域中重要的概念之一。可计算性逻辑(Computability Logic,CoL)是关于可计算性的形式理论,是一种交互的资源逻辑。其中,CoL2系统采用博弈的语义,是对经典命题逻辑的扩展,在经典命题逻辑的基础上添加了选择运算和一般原子,比经典命题逻辑更富有表达力,具有更广阔的应用前景,并且有较高的证明效率。分析了CoL2系统的可判定性,即通过提出一个算法来判断任意一个CoL2公式是否是可证明的,并且证明了该算法是多项式空间内运行的。 相似文献
3.
反应系统的连续时序逻辑表示和验证 总被引:1,自引:0,他引:1
引进一个称为LTLC的连续时间时序逻辑,用来对反应系统进行规范与验证.LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质,这样就可将系统与性质问的满足关系转化为逻辑公式间的蕴涵关系.同时,采用非负实数集作为时间域还使我们可以利用标准的存在量词来表示变量隐藏,并可用逻辑蕴涵来表示反应系统间的求精关系.该文首先给出了LTLC的一个简单介绍,然后讨论了如何使用LTLC对反应系统进行表示与推理,最后证明了一个关于LTLC的可判定性结果.此结果可用于有穷状态反应系统的自动验证. 相似文献
4.
5.
张健 《计算机研究与发展》1998,35(5):389-392
文中研究了模态逻辑推理的翻译法,即把模态逻辑公式按照一定的规则翻译成经典逻辑公式,再用传统的定理器进行推理,文中指出,该方法在理论上保持了正规命题模态逻辑的可判定性,还给出了一些试验结果,说明该方法实际可行的。 相似文献
6.
描述了访问控制和逻辑的关系,并将访问控制授权判决问题归约成逻辑蕴涵问题;总结了基于逻辑的访问控制的基本逻辑问题,即逻辑基础、可判定性和安全性分析;分析了一些访问控制模型的基本逻辑问题,包括基于身份的访问控制模型、基于信任管理的访问控制模型和基于属性的访问控制模型;指出了结构化属性描述能力和安全性分析是基于逻辑的访问控制需要进一步研究的问题. 相似文献
7.
逻辑之间的语义忠实语义满翻译 总被引:1,自引:0,他引:1
翻译在计算机科学中的一个重要应用是实现一个逻辑与另一个逻辑在表达能力上的比较,以及利用目标逻辑的推理机实现源逻辑的推理.现有逻辑之间的翻译理论和性质没有深入研究逻辑的语义翻译,以及翻译是否保持不可满足性等问题.该文研究了一类同时保持公式的可满足性和不可满足性的翻译——语义忠实语义满翻译,给出了语义忠实语义满翻译的定义,比较了语义忠实语义满翻译与已有文献中翻译定义的区别和联系,讨论了逻辑的可靠性、完备性、可判定性、紧致性、公式的逻辑等价性,以及模型的初等等价性在语义忠实语义满翻译下被保持的问题.运用语义忠实语义满翻译的定义给出了逻辑之间的同义性定义,并证明了同义关系是逻辑之间的一个等价关系. 相似文献
8.
时态描述逻辑ALC-LTL的Tableau判定算法 总被引:2,自引:2,他引:0
时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-工`I'I、中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。 相似文献
9.
11.
Savas Konur 《Frontiers of Computer Science》2013,7(3):370-403
Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed. 相似文献
12.
Decidability by Resolution for Propositional Modal Logics 总被引:1,自引:0,他引:1
Renate A. Schmidt 《Journal of Automated Reasoning》1999,22(4):379-396
The paper shows that satisfiability in a range of popular propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution combined with condensing, and possibly some additional form of normalization, is a decision procedure for the satisfiability problem in certain so-called path logics. Path logics arise from normal propositional modal logics by the optimized functional translation method. The decision result provides an alternative method of proving decidability for modal logics, as well as closely related systems of artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, many standard first-order theorem provers that are based on resolution are suitable for facilitating modal reasoning. 相似文献
13.
Comparative logics were introduced by Casari in the 1980s totreat aspects of comparative reasoning occurring in naturallanguage. In this article Gentzen systems are defined for theselogics by means of a special mix rule that combines calculifor various substructural logics with a hypersequent calculusfor Meyer and Slaney's Abelian logic. Cut-elimination is establishedfor all these systems, and as a consequence, a positive answeris given to an open problem on the decidability of the basiccomparative logic. 相似文献
14.
Arnon Avron 《Annals of Mathematics and Artificial Intelligence》1991,4(3-4):225-248
The existence of simple semantics and appropriate cut-free Gentzen-type formulations are fundamental intrinsic criteria for the usefulness of logics. In this paper we show that by using hypersequents (which are multisets of ordinary sequents) we can provide such Gentzen-type systems to many logics. In particular, by using a hypersequential generalization of intuitionistic sequents we can construct cut-free systems for some intermediate logics (including Dummett's LC) which have simple algebraic semantics that suffice, e.g., for decidability. We discuss the possible interpretations of these logics in terms of parallel computation and the role that the usual connectives play in them (which is sometimes different than in the sequential case). 相似文献
15.
《Information and Computation》2006,204(10):1413-1452
Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics—which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics. 相似文献
16.
17.
18.
In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma theoretical perspective. We provide a very general definition of ML systems, which covers allthe ML systems used in the literature, and we develop a proof theoryfor an important subclass of them: the MR systems. We prove variousimportant results; among other things, we prove a normal form theorem,the sub-formula property, and the decidability of an importantinstance of the class of the MR systems. The paper concludes with a detailed comparison among the alternativeapproaches. 相似文献
19.
Davide Bresolin Angelo Montanari Guido Sciavicco 《Journal of Automated Reasoning》2007,38(1-3):173-199
Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements
that refer to time intervals. Unfortunately, most such logics turn out to be (highly) undecidable. In order to get decidability,
severe syntactic or semantic restrictions have been imposed to interval-based temporal logics to reduce them to point-based
ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones that
are genuinely interval-based is still largely unexplored. In this paper, we focus our attention on interval logics of temporal
neighborhood. We address the decision problem for the future fragment of Neighborhood Logic (Right Propositional Neighborhood
Logic, RPNL for short), and we positively solve it by showing that the satisfiability problem for RPNL over natural numbers
is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure, and we prove its optimality. 相似文献
20.
Davide Bresolin Dario Della Monica Angelo Montanari Guido Sciavicco 《Annals of Mathematics and Artificial Intelligence》2014,71(1-3):11-39
Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema’s CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDTBS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Schönfinkel class. In addition, we show that CDTBS is in fact NP-complete (Bernays-Schönfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Schönfinkel class. Finally, we show that any increase in the negation depth of CDTBS modalities immediately yields undecidability. 相似文献