The logic of Peirce algebras

Peirce algebras combine sets, relations and various operations linking the two in a unifying setting. This paper offers a modal perspective on Peirce algebras. Using modal logic a characterization of the full Peirce algebras is given, as well as a finite axiomatization of their equational theory that uses so-called unorthodox derivation rules. In addition, the expressive power of Peirce algebras is analyzed through their connection with first-order logic, and the fragment of first-order logic corresponding to Peirce algebras is described in terms of bisimulations.     

Bisimulations for Temporal Logic

We define bisimulations for temporal logic with Since and Until. This new notion is compared to existing notions of bisimulations, and then used to develop the basic model theory of temporal logic with Since and Until. Our results concern both invariance and definability. We conclude with a brief discussion of the wider applicability of our ideas.     

Elementary Definability and Completeness in General and Positive Modal Logic

The paper generalises Goldblatt's completeness proof for Lemmon–Scott formulas to various modal propositional logics without classical negation and without ex falso, up to positive modal logic, where conjunction and disjunction, andwhere necessity and possibility are respectively independent.Further the paper proves definability theorems for Lemmon–Scottformulas, which hold even in modal propositional languages without negation and without falsum. Both, the completeness theorem and the definability theoremmake use only of special constructions of relations,like relation products. No second order logic, no general frames are involved.     

Two Natural Deduction Systems for Hybrid Logic: A Comparison

In this paper two different natural deduction systems forhybrid logic are compared and contrasted.One of the systems was originally given by the author of the presentpaper whereasthe other system under consideration is a modifiedversion of a natural deductionsystem given by Jerry Seligman.We give translations in both directions between the systems,and moreover, we devise a set of reduction rules forthe latter system bytranslation of already known reduction rules for the former system.     

Naming Worlds in Modal and Temporal Logic

In this paper we suggest adding to predicate modal and temporal logic a locality predicate W which gives names to worlds (or time points). We also study an equal time predicate D(x, y)which states that two time points are at the same distance from the root. We provide the systems studied with complete axiomatizations and illustrate the expressive power gained for modal logic by simulating other logics. The completeness proofs rely on the fairly intuitive notion of a configuration in order to use a proof technique similar to a Henkin completion mixed with a tableau construction. The main elements of the completeness proofs are given for each case, while purely technical results are grouped in the appendix. This revised version was published online in August 2006 with corrections to the Cover Date.     

Natural Deduction for First-Order Hybrid Logic

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.     

Means-End Relations and a Measure of Efficacy

Propositional dynamic logic (PDL) provides a natural setting for semantics of means-end relations involving non-determinism, but such models do not include probabilistic features common to much practical reasoning involving means and ends. We alter the semantics for PDL by adding probabilities to the transition systems and interpreting dynamic formulas 〈α〉 ϕ as fuzzy predicates about the reliability of α as a means to ϕ. This gives our semantics a measure of efficacy for means-end relations.     

一种新的汉语自动分词算法的研究和应用

针对中文信息处理中词与词之间的歧义切分难点,通过分析词语之间的逻辑关系,然后用泛布尔代数将其表达出来,再将此算法用于汉语自动分词系统。实验表明此方法提高了分词的速度和准确性,达到了较好的分词效果。     

带Rough相等关系词的Rough逻辑系统及其推理

以公式的定义域集的下和上近似分别相等方法,定义了两个Rough逻辑公式Rough相等,并以此定义了Rough相等关系词“＝R”,它不仅比等值词“←→”运算有更多的直观性,而且既考虑了可定义的公式,也包含了那 边界线上不可定义或可能可定义的公式,所以,经典逻辑中的隐含量φ→ψ被移至Rough逻辑中应当解释为R.(d(φ））包含R.(d(ψ))∧R^*(d(φ))包含R^*（d(ψ））。经典逻辑中的等值式φ←→ψ被移至Rough逻辑中应当解释为R.(d(φ））＝R.(d(ψ))∧R^*(d(φ))＝R^*（d(ψ））,其中d(F)是公式F的定义区域,它可能是可定久集,也可能是不可定义集或Rough集,这是Rough逻辑与经典逻辑与其它非标准逻辑的重要区别之一,将这种Rough相等词“＝R”引入Rough逻辑中,因而得一些相关的性质和相关的推理规则。文本中建立了带Rough相等关系词“＝R”的Rough逻辑推理系统,并在这个系统下用演绎推理方法证明了几个具体的实例。     

Logic of transition systems

Labeled transition systems are key structures for modeling computation. In this paper, we show how they lend themselves to ordinary logical analysis (without any special new formalisms), by introducing their standard first-order theory. This perspective enables us to raise several basic model-theoretic questions of definability, axiomatization and preservation for various notions of process equivalence found in the computational literature, and answer them using well-known logical techniques (including the Compactness theorem, Saturation and Ehrenfeucht games). Moreover, we consider what happens to this general theory when one restricts attention to special classes of transition systems (in particular, finite ones), as well as extended logical languages (in particular, infinitary first-order logic). We hope that this puts standard logical formalisms on the map as a serious option for a theory of computational processes. As a side benefit, our approach increases comparability with several other existing formalisms over labeled transition systems (such as Process Algebra or Modal Logic). We provide some pointers to this effect, too.     

空间数据库的方向关系模型

方向作为一个定性的空间关系,是空间拓扑关系的一个重要补充。现在的方向关系模型运用十分粗糙的最小包含矩形或概括为单个的点来表示近似方向关系。文章设计的方向关系矩阵模型克服了传统模型的限制,为复杂空间对象提供了更好的方向近似,包括凹面区域和有洞的对象。     

Pi演算与动态描述逻辑DDL的关系研究

分析了Pi演算与动态描述逻辑DDL之间的关系:DDL分别从静态结构与动态结构两方面对Pi演算的若干过程定义进行描述,体现了过程的逻辑结构及过程间逻辑关系的变化;以一种基于Pi演算的过程模型为基础,分析了ALC描述逻辑、TBox和ABox的语义,并通过一个例子说明Pi演算对DDL动态知识的变化过程的描述.以上工作表明:DDL的可判定推理可解决基于Pi演算的动态系统的某些一致性检测问题,而Pi演算对动态系统的描述能力可解决DDL动态知识的变化过程的描述问题.     

Algebras of Relations and Relevance Logic

We prove that algebras of binary relations whose similaritytype includes intersection, composition, converse negation andthe identity constant form a non-finitely axiomatizable quasivarietyand that the equational theory is not finitely based. We applythis result to the problem of the completeness of relevant logicwith respect to binary relations.     

Dynamic Negation, the One and Only

We consider the variety of Dynamic Relation Algebras V(DRA). We show that the monoid of an algebra in this variety determines dynamic negation uniquely.     

关于部分四值逻辑中保2元正则可离关系的分类

根据部分多值逻辑的完备性理论,定出部分四值逻辑中保2元正则可离关系,并按照准完备集之间的相似关系概念,对所定出的关系进行分类。     

Decidable and undecidable logics with a binary modality

We give an overview of decidability results for modal logics having a binary modality. We put an emphasis on the demonstration of proof-techniques, and hope that this will also help in finding the borderlines between decidable and undecidable fragments of usual first-order logic.Research supported by the Hungarian National Foundation for Scientific Research grants no. T16448, F17452, T7255. Research of the first author is also supported by a grant of Logic Graduate School of Eötvös Loránd University Budapest     

Logic of Proofs and Labels with a Complete Set of Operations

We develop a framework in which operations on proofs can bespecified and studied. Proofs are treated as structures builtfrom atomic proofs and references by means of computable operations. Our approach extends the ideas of Logic of Proofs (Artemov,1995, Bull. Symb. Logic, 7, 1–36) in which the proof predicate‘t is a proof of F ’ is incorporated into the propositionallanguage. We introduce an additional storage predicate ‘xis a label for F ’ (Yavorskaya, 2005, J. Logic Comput.,15, 517–537). In this article which is essentially a continuation of Yavorskaya'swork, we study a natural example of a logic with operationson proofs and labels. This logic is decidable and complete with respect to its intended semantics. is capable to internalizeits own proofs, and operations of suffice to realize all operations specified in the languagewith proofs and labels.