A Temporal Logic for Sortals

With the past and future tense propositional operators in its syntax, a formal logical system for sortal quantifiers, sortal identity and (second order) quantification over sortal concepts is formulated. A completeness proof for the system is constructed and its absolute consistency proved. The completeness proof is given relative to a notion of logical validity provided by an intensional semantic system, which assumes an approach to sortals from a modern form of conceptualism.     

A Temporal Semantics for Basic Logic

In the context of truth-functional propositional many-valued logics, Hájek’s Basic Fuzzy Logic BL [14] plays a major rôle. The completeness theorem proved in [7] shows that BL is the logic of all continuous t-norms and their residua. This result, however, does not directly yield any meaningful interpretation of the truth values in BL per se. In an attempt to address this issue, in this paper we introduce a complete temporal semantics for BL. Specifically, we show that BL formulas can be interpreted as modal formulas over a flow of time, where the logic of each instant is ?ukasiewicz, with a finite or infinite number of truth values. As a main result, we obtain validity with respect to all flows of times that are non-branching to the future, and completeness with respect to all finite linear flows of time, or to an appropriate single infinite linear flow of time. It may be argued that this reduces the problem of establishing a meaningful interpretation of the truth values in BL logic to the analogous problem for ?ukasiewicz logic.     

Temporal Reference in Linear Tense Logic

The paper introduces a first-order theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems.     

Equality and Monodic First-Order Temporal Logic

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.     

Action and Knowledge in Alternating-Time Temporal Logic

Alternating-time temporal logic (ATL) is a branching time temporal logic in which statements about what coalitions of agents can achieve by strategic cooperation can be expressed. Alternating-time temporal epistemic logic (ATEL) extends ATL by adding knowledge modalities, with the usual possible worlds interpretation. This paper investigates how properties of agents’ actions can be expressed in ATL in general, and how properties of the interaction between action and knowledge can be expressed in ATEL in particular. One commonly discussed property is that an agent should know about all available actions, i.e., that the same actions should be available in indiscernible states. Van der Hoek and Wooldridge suggest a syntactic expression of this semantic property. This paper shows that this correspondence in fact does not hold. Furthermore, it is shown that the semantic property is not expressible in ATEL at all. In order to be able to express common and interesting properties of action in general and of the interaction between action and knowledge in particular, a generalization of the coalition modalities of ATL is proposed. The resulting logics, ATL-A and ATEL-A, have increased expressiveness without loosing ATL’s and ATEL’s tractability of model checking.     

Decidable Cases of First-order Temporal Logic with Functions

We consider the decision problem for cases of first-order temporal logic with function symbols and without equality. The monadic monodic fragment with flexible functions can be decided with EXPSPACE-complete complexity. A single rigid function is sufficient to make the logic not recursively enumerable. However, the monadic monodic fragment with rigid functions, where no two distinct terms have variables bound by the same quantifier, is decidable and EXPSPACE-complete. Presented by Robert Goldblatt     

时态数据库属性推理的类型逻辑

1994年Gabbay等论证了时态逻辑的公理化系统和证明论方法不适于时态数据库推理建模,因此目前主要使用非公理化的时态逻辑做推理。然而非公理化的时态逻辑缺乏公理化性质约束,形式晦涩,无直观性与运算性,因而一般不用于知识推理。另一方面,1983年Allen提出了13种时态关系运算,并使用区间逻辑对时态关系进行表达,但这些运算只能表示时间本身的运算关系,未能体现时间与属性之间的映射关系,不能表达时态数据库属性间的推理与运算。此外,时态数据库中仍存在着许多开问题,例如在做属性推理与运算时出现的Now语义的不确定性问题。基于此,我们提出一种基于时态数据库属性推理的类型逻辑系统,其主要思路为将属性映射为类型,将类型映射为时间向量子集,以时间向量集为逻辑语义模型,在推理中从句法逻辑系统剥离对时间的表示,减少逻辑算子,与时间相关的运算单纯由语义模型支持,从而降低复杂性,提高运算能力。并且由于该类型逻辑系统是基于构造性语义的,能直观解释Now的不确定性问题。文中给出了相对该系统的时态数据库属性推理的应用示例,从技术可操作性上介绍了根据该类型逻辑设计的时态推理中间件原型及工作流程,最后从元理论范畴证明了系统可靠性与完全性的逻辑性质及切割消除与判定性的证明论性质。     

A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic

This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.     

Cooperation,Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems.     

数字表型视域下的健康数据确权：基于时间逻辑的展开

健康数据的价值生成具有历时性的特征。数据确权的空间逻辑意识到了健康数据的公共价值,但是忽略了这种公共价值的生成与彰显可能需要经历长时间的积累。提倡健康数据确权的时间逻辑,就是要克服空间逻辑在确权问题上的即时性思考。数据价值在时间链条上的延伸得益于对健康数据的关系性解读,数据的当前使用与未来使用表征为数据与多个主体之间的“依附”与“分离”,由此赋予了数据以新的时间性。这意味着健康数据确权需要将数据价值的未来面向考虑进来。在此基础上,时间逻辑的践行需要代际义务、团结伦理的引导,同时强化规则的预防功能。

     

Logic,Logic, and Logic

In his recent paper in History and Philosophy of Logic, John Kearns argues for a solution of the Liar paradox using an illocutionary logic (Kearns 2007 Kearns, J. 2007. ‘An illocutionary logical explanation of the Liar Paradox’. History and Philosophy of Logic, 28: 31–66. [Taylor &; Francis Online], [Web of Science ®] , [Google Scholar]). Paraconsistent approaches, especially dialetheism, which accepts the Liar as being both true and false, are rejected by Kearns as making no ‘clear sense’ (p. 51). In this critical note, I want to highlight some shortcomings of Kearns' approach that concern a general difficulty for supposed solutions to (semantic) antinomies like the Liar. It is not controversial that there are languages which avoid the Liar. For example, the language which consists of the single sentence ‘Benedict XVI was born in Germany’ lacks the resources to talk about semantics at all and thus avoids the Liar. Similarly, more interesting languages such as the propositional calculus avoid the Liar by lacking the power to express semantic concepts or to quantify over propositions. Kearns also agrees with the dialetheist claim that natural languages are semantically closed (i.e. are able to talk about their sentences and the semantic concepts and distinctions they employ). Without semantic closure, the Liar would be no real problem for us (speakers of natural languages). But given the claim, the expressive power of natural languages may lead to the semantic antinomies. The dialetheist argues for his position by proposing a general hypothesis (cf. Bremer 2005 Bremer, M. 2005. An Introduction to Paraconsistent Logics, Bern: Lang.  [Google Scholar], pp. 27–28): ‘(Dilemma) A linguistic framework that solves some antinomies and is able to express its linguistic resources is confronted with strengthened versions of the antinomies’. Thus, the dialetheist claims that either some semantic concepts used in a supposed solution to a semantic antinomy are inexpressible in the framework used (and so, in view of the claim, violate the aim of being a model of natural language), or else old antinomies are exchanged for new ones. One horn of the dilemma is having inexpressible semantic properties. The other is having strengthened versions of the antinomies, once all semantic properties used are expressible. This dilemma applies, I claim, to Kearns' approach as well.     

Modal Logic As Dialogical Logic

The title reflects my conviction that, viewed semantically,modal logic is fundamentally dialogical; this conviction is based on the key role played by the notion of bisimulation in modal model theory. But this dialogical conception of modal logic does not seem to apply to modal proof theory, which is notoriously messy. Nonetheless, by making use of ideas which trace back to Arthur Prior (notably the use of nominals, special proposition symbols which name worlds) I will show how to lift the dialogical conception to modal proof theory. I argue that this shift to hybrid logic has consequences for both modal and dialogical logic, and I discuss these in detail.     

Behavior Matching in Multimodal Communication Is Synchronized

A variety of theoretical frameworks predict the resemblance of behaviors between two people engaged in communication, in the form of coordination, mimicry, or alignment. However, little is known about the time course of the behavior matching, even though there is evidence that dyads synchronize oscillatory motions (e.g., postural sway). This study examined the temporal structure of nonoscillatory actions—language, facial, and gestural behaviors—produced during a route communication task. The focus was the temporal relationship between matching behaviors in the interlocutors (e.g., facial behavior in one interlocutor vs. the same facial behavior in the other interlocutor). Cross‐recurrence analysis revealed that within each category tested (language, facial, gestural), interlocutors synchronized matching behaviors, at temporal lags short enough to provide imitation of one interlocutor by the other, from one conversational turn to the next. Both social and cognitive variables predicted the degree of temporal organization. These findings suggest that the temporal structure of matching behaviors provides low‐level and low‐cost resources for human interaction.