Temporal Logic

I this paper I give minimal axioms for the ontology of time, especially A-theories and B-theories and I derive philosophically interesting lemmas. The exercise is set-theoretical, defining all notions and indicating assumptions and philosophical points of disagreement, while being easy to translate to other formal expressions . The issue of a logic for A-theories of time is treated towards the end, where I sketch ‘copresent’ operators for capturing the idea of temporal passage. The main conclusion will be that, while circularity (...) threatens both families of theories, the growing block theory (belonging to the A-theory) is the least objectionable philosophically. (shrink)

Philosophical views about the logical structure of time are typically divided between proponents of A and B theories, based on McTaggart's A and B series. Drawing on Paul Ricoeur's hermeneutic phenomenology, I develop and defend McTaggart's thesis that the C series and the A series working together give a consistent description of temporal experience, provided that the two series are treated as distinct dimensions internal to time. In the proposed two-dimensional model, the C series expresses a nesting order of the (...) constitutive states of a world, whereas ontological continuity and change are properties of the A series. This, I argue, allows limited backward causation. (shrink)

This paper presents the proof of the apparent nature of relative simultaneity originally derived from Einstein’s Special Theory of Relativity (STR). The proof does not challenge the validity of the STR but uncovers fundamental and widespread error in understanding of practical implications of Lorentz transformations. It is demonstrated that more than a century long debates generally miss the point. This results in counterintuitive claims of coexisting multiple time realities by mere equivalence of equal clock indications and simultaneity. Such claims have (...) little empirical significance but they are substantial in education and philosophy which has become utterly confused after universal acceptance of the STR and rejections of Henri Bergson’s challenge. There is nothing more to “relative simultaneity” other than the effect of identical clocks being shifted by an offset which depends on synchronisation method. (shrink)

The paper consists of two parts. The first critically analyses Meyer’s [2005] version of the triviality objection to presentism (according to which, presentism is either trivial or untenable), and tries to show that his argument is untenable because – contrary to what he claimed – he did not take into account the entire possible spectrum of interpretations of the presentist’s thesis. In the second, positive part of the paper, it is shown that a leading form of tensed theory of time (...) postulates the same ontology as presentism and that it avoids the triviality problem which means that it can be used to generate an alternative formulation of presentism which is no longer vulnerable to the triviality objection. (shrink)

Temporal logic is of importance in theoretical computer science for its application in formal verification, to state requirements of hardware or software systems. Linear temporal logic is an appropriate logical environment to formalize Yablo’s paradox which is seemingly non-self-referential and basically has a sequential structure. We give a brief review of Yablo’s paradox and its various versions. Formalization of these paradoxes yields some theorems in Linear Temporal Logic (LTL) for which we give syntactic proofs using an appropriate axiomatization of LTL.

Adrian Bardon has produced a new version of his historical introduction to the philosophy of time. Originally published in 2013, the second edition of 2024 is partly rewritten and supplemented with a more extensive discussion on our disposition to project the passage of time [...] Although the book’s title emphasizes history, most of the chapters are directed at issues in systematic philosophy of time: the realism/antirealism debate, temporal passage, temporal experience, spacetime, direction, time travel, time and free will, and the (...) temporal boundaries of the universe. (shrink)

In her recent book, Russell (2023) examines various so-called “barriers to entailment,” including Hume’s law, roughly the thesis that an ‘ought’ cannot be derived from an ‘is.’ Hume’s law bears an obvious resemblance to the proscription on fallacies of modality in relevance logic, which has traditionally formally been captured by the so-called Ackermann property. In the context of relevant modal logic, this property might be articulated thus: no conditional whose antecedent is box-free and whose consequent is box-prefixed is valid (for (...) the connection, interpret box deontically). While the deontic significance of Ackermann-like properties has been observed before, Russell’s new book suggests a more broad-scoped formal investigation of the relationship between barrier theses of various kinds and corresponding Ackermann-like properties. In this paper, I undertake such an investigation by elaborating a general relevant bimodal logical framework in which several of the barriers Russell examines can be given formal expression. I then consider various Ackermann-like properties corresponding to these barriers and prove that certain systems satisfy them. Finally, I respond to some objections Russell makes against the use of relevance logic to formulate Hume’s law and related barriers. (shrink)

The concept of branching time is widely utilized to counter fatalistic arguments to the conclusion that whatever will happen is already unavoidable. The most common semantics for branching time, such as Ockhamism, Peirceanism, and Supervaluationism, offer a formal explanation for why fatalistic arguments are flawed. This paper explores a different type of argument, one that borders on fatalism and is concerned with what might possibly happen in the future. In the paper, I show how this type of argument poses a (...) new fatalistic threat to branching time. (shrink)

In this paper, we study temporal logic for finite linear structures and surjective bounded morphisms between them. We give a characterisation of such structures by modal formulas and show that every pair of linear structures with a bounded morphism between them can be uniquely characterised by a temporal formula up to an isomorphism. As the main result, we prove Kripke completeness of the logic with respect to the class of finite linear structures with bounded morphisms between them.

We combine linear temporal logic (with both past and future modalities) with a deontic version of justification logic to provide a framework for reasoning about time and epistemic and normative reasons. In addition to temporal modalities, the resulting logic contains two kinds of justification assertions: epistemic justification assertions and deontic justification assertions. The former presents justification for the agent’s knowledge and the latter gives reasons for why a proposition is obligatory. We present two kinds of semantics for the logic: one (...) based on Fitting models and the other based on neighborhood models. The use of neighborhood semantics enables us to define the dual of deontic justification assertions properly, which corresponds to a notion of permission in deontic logic. We then establish the soundness and completeness of an axiom system of the logic with respect to these semantics. Further, we formalize the Protagoras versus Euathlus paradox in this logic and present a precise analysis of the paradox, and also briefly discuss Leibniz’s solution. (shrink)

The fundamental relations in private law are claims and duties. These legal relations can be changed by agents with the appropriate legal powers. We use propositional dynamic logic and ideas about propositional control from the agency literature to formalize these changes in legal relations. Our models are sets of states with functions specifying atomic facts, agents’ abilities to change atomic facts, legal relations between agents concerning changing atomic facts and agents’ powers. We present a formal language that allows us to (...) describe models and changes of models caused by two kinds of actions: actions that change atomic facts and actions that change legal relations. Next, we present a sound and complete calculus for this language. The paper demonstrates that the perspective on actions borrowed from computer science can be used to shed interesting light on the dynamics of legal relations. (shrink)

We show that monadic intuitionistic quantifiers admit the following temporal interpretation: “always in the future” (for$\forall $) and “sometime in the past” (for$\exists $). It is well known that Prior’s intuitionistic modal logic${\sf MIPC}$axiomatizes the monadic fragment of the intuitionistic predicate logic, and that${\sf MIPC}$is translated fully and faithfully into the monadic fragment${\sf MS4}$of the predicate${\sf S4}$via the Gödel translation. To realize the temporal interpretation mentioned above, we introduce a new tense extension${\sf TS4}$of${\sf S4}$and provide a full and faithful translation (...) of${\sf MIPC}$into${\sf TS4}$. We compare this new translation of${\sf MIPC}$with the Gödel translation by showing that both${\sf TS4}$and${\sf MS4}$can be translated fully and faithfully into a tense extension of${\sf MS4}$, which we denote by${\sf MS4.t}$. This is done by utilizing the relational semantics for these logics. As a result, we arrive at the diagram of full and faithful translations shown in Figure 1 which is commutative up to logical equivalence. We prove the finite model property (fmp) for${\sf MS4.t}$using algebraic semantics, and show that the fmp for the other logics involved can be derived as a consequence of the fullness and faithfulness of the translations considered. (shrink)

Todd and Rabern (2021) have argued that if we assume that future contingents are untrue and if we accept the Retro-closure principle (???? → PF(????)), then the existence of a temporal omniscient entity becomes metaphysically impossible. Since the truth of a metaphysical and theological theory should not be dependent on questions of temporal semantics, Todd and Rabern conclude that, if one wishes to maintain that future contingents are untrue, one must abandon the Retro-closure principle. The aim of this paper is (...) to propose a temporal semantics system in which future contingents are untrue, the Retro-closure principle is valid, and the possibility of the existence of an omniscient and temporal being is guaranteed. (shrink)

In this paper, we continue with the study of tense operators on Nelson algebras (Figallo et al. in Studia Logica 109(2):285–312, 2021, Studia Logica 110(1):241–263, 2022). We define the variety of algebras, which we call tense Nelson D-algebras, as a natural extension of tense De Morgan algebras (Figallo and Pelaitay in Logic J IGPL 22(2):255–267, 2014). In particular, we give a discrete duality for these algebras. To do this, we will extend the representation theorems for Nelson algebras given in Sendlewski (...) (Studia Logica 43(3):257–280, 1984) to the tense case. (shrink)

Temporal justification logic is a new family of temporal logics of knowledge in which the knowledge of agents is modelled using a justification logic. In this paper, we present various temporal justification logics involving both past and future time modalities. We combine Artemov’s logic of proofs with linear temporal logic with past, and we also investigate several principles describing the interaction of justification and time. We present two kinds of semantics for our temporal justification logics, one based on interpreted systems (...) and Fitting models and the other based on Mkrtychev models, and further, we establish soundness and completeness. We show that the internalization property holds in some of the temporal justification logics. We further investigate the two well-known epistemic-temporal notions of no forgetting and no learning in the framework of justification logics. Finally, we present temporal justification logics that avoid the logical omniscience problem. (shrink)

There are essentially two ways to develop the Peircean idea that future contingents are all false. One is to provide a quantificational semantics for "will," as is usually done. The other is to define a quantificational postsemantics based on a linear semantics for "will." As we will suggest, the second option, although less conventional, is more plausible than the first in some crucial respects. The postsemantic approach overcomes three major troubles that have been raised in connection with Peirceanism: the apparent (...) scopelessness of "will" with respect to negation, the failure of Future Excluded Middle, and the so-called zero credence problem. (shrink)

Is it possible to change the past—to make something that has happened not have happened? Past-alteration is widely believed to be ‘logically impossible’. But despite this, there have been few attempts to actually apply logical resources to the question of whether it is possible to change the past. This chapter articulates a novel tense logic and uses it to argue that past-alteration is possible—with just a single dimension of time—so long as it’s possible for time to have a certain kind (...) of structure: one which is ‘backwards-branching’ and in which the relation of precedence ‘comes apart’ from the relation of succession. The remainder of the chapter explores some of the metaphysical implications of this account of what it is to change the past. (shrink)

This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.

Social bots are computer programs that act like human users on social media platforms. Social bot detection is a rapidly growing field dominated by machine learning approaches. In this paper, we propose a complementary method to machine learning by exploring bot detection as a model checking problem. We introduce Temporal Network Logic (TNL) which we use to specify social networks where agents can post and follow each other. Using this logic, we formalize different types of social bot behavior with formulas (...) that are satisfied in a model of a network with bots. We also consider an extension of the logic where we explore the expressive power of including elements from hybrid logic in our framework. We give model checking algorithms for TNL and its hybrid extension, and show that the complexity of the former is in p and the latter in pspace. (shrink)

A novel fatalistic argument that combines elements of modal, temporal, and epistemic logic to prove that the fixed past is not compatible with the open future has recently been presented by Lampert (Analysis 82(3):426–434, 2022). By the construction of a countermodel, it is shown that his line of reasoning is defective. However, it is also explained how Lampert’s argument could be corrected if it were supported with an extra premise regarding the temporal status of a priori knowledge. This additional assumption—which (...) was tacit in the original presentation—is shown to be the weakest link, and it is argued that, despite Lampert’s assurance, it can be plausibly rejected in a roughly Ockhamist framework. Thus, it is concluded that the fixed past poses no threat to the open future; however, a few different lessons about knowledge, necessity, and time are drawn from careful reflection on this novel argument. (shrink)

Fitch's Paradox and the Paradox of the Knower both make use of the Factivity Principle. The latter also makes use of a second principle, namely the Knowledge-of-Factivity Principle. Both the principle of factivity and the knowledge thereof have been the subject of various discussions, often in conjunction with a third principle known as Closure. In this paper, we examine the well-known Surprise Examination paradox considering both the principles on which this paradox rests and some formal characterisations of the surprise notion, (...) crucial in this paradox. Standard formalizations of the Surprise Examination paradox in modal logic do not seem, at first glance, to depend on either factivity or knowledge-of-factivity, but we will argue that both factivity and knowledge-of-factivity play a key implicit role in the paradox. Namely, they are implicitly, perhaps unintentionally, used in order to simplify the definition of surprise. We analyze modal logical formalizations of three versions of the paradox concluding that the Surprise Examination paradox is the result of two flaws: the assumption of knowledge-of-factivity, and the over-simplification of the definition of "surprise" accordingly. By fixing these two flaws, the Surprise Examination paradox vanishes. (shrink)

In our previous work we have introduced loop-type sequent calculi for propositional linear discrete tense logic and proved that these calculi are sound and complete. Decision procedures using the calculi have been constructed for the considered logic. In the present paper we restrict ourselves to the logic with the unary temporal operators “next” and “henceforth always”. Proof-theory of the sequent calculus of this logic is considered, focusing on loop specification in backward proof-search. We describe cyclic sequents and prove that any (...) loop consists of only cyclic sequents. A class of sequents for which backward proof-search do not require loop-check is presented. It is shown how sequents can be coded by binary strings that are used in backward proof-search for the sake of more efficient loop-check. (shrink)

Branching time is a popular theory of time that is intended to account for the openness of the future. Generally, branching-time models the openness of the future by positing a multiplicity of concrete alternative futures mirroring all the possible ways the future could unfold. A distinction is drawn in the literature among branching-time theories: those that make use of moment-based structures and those that employ history-based ones. In this paper, I introduce and discuss a particular kind of openness relative to (...) the possibility that time ends (doomsday). I then show that whereas moment-based branching structures cannot represent this kind of openness, history-based structures can account for it. The conclusion is that history-based structures have an advantage over moment-based ones. (shrink)

The language of linear temporal logic can be interpreted on the class of dynamic topological systems, giving rise to the intuitionistic temporal logic ${\sf ITL}^{\sf c}_{\Diamond \forall }$, recently shown to be decidable by Fernández-Duque. In this article we axiomatize this logic, some fragments, and prove completeness for several familiar spaces.

The concept of hypodox is dual to the concept of paradox. Whereas a paradox is incompatibly overdetermined, a hypodox is underdetermined. Indeed, many particular paradoxes have dual hypodoxes. So, naively the dual of Russell’s Paradox is whether the set of all sets that are members of themselves is self-membered. The dual of the Liar Paradox is the Truth-teller, and a hypodoxical dual of the Heterological paradox is whether ‘autological’ is autological. I provide some analysis of the duality and I search (...) for modal hypodoxes as duals to known paradoxes. I also try to continue this search further by mapping the relations between some paradoxes and hypodoxes in duality squares. This investigation increases the known extension of the concept of hypodox, and the duality relation between paradoxes and hypodoxes assists in finding some of these. (shrink)

1. First, a short anecdote. In the mid-1980s, Professor Jerzy Pogonowski gave a series of lectures entitled The Lvov-Warsaw School at the Institute of Philosophy at the Adam Mickiewicz University i...

This paper starts the systematic study of inconsistency measures for propositional logics enriched with operators involving time. We use Prior’s operators for tense logic: H, G, P, and F; however, we apply different semantics to them. We define two logics. The first one, ATPL, allows formulas with the application of any of the four operators any number of times to propositional logic formulas. The semantics is given in terms of TPL structures. We then show how to measure the inconsistency of (...) a set of ATPL formulas using appropriately modified versions of standard inconsistency measures for propositional logic. Additionally, these new measures are checked for the satisfaction of various properties. We also investigate a new concept of inconsistency that cannot be defined for propositional logic. Then, ATPL is extended to CTPL by applying the propositional connectives to ATPL formulas and measuring inconsistency is extended to sets of CTPL formulas. (shrink)

Gabbay's separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In this paper, we establish an analogous statement a...

Although formal system verification has been around for many years, little attention was given to the case where the specification of the system has to be changed. This may occur due to a failure in capturing the clients’ requirements or due to some change in the domain (think for example of banking systems that have to adapt to different taxes being imposed). We are interested in having methods not only to verify properties, but also to suggest how the system model (...) should be changed so that a property would be satisfied. For this purpose, we will use techniques from the area of Belief Revision, that deals with the problem of changing a knowledge base in view of new information. In the last thirty years, several authors have contributed with change operations and ways of characterizing them. However, most of the work concentrates on knowledge bases represented using classical propositional logic. In the last decade, there have been efforts to apply belief revision theory to description and modal logics. In this work, we analyze what is needed for a theory of belief revision which can be applied to the temporal logic, such as the Computation Tree Logic (CTL). In particular, we illustrate different alternatives for formalizing the concept of revision of CTL. Our interest in this particular logic comes both from practical issues, since it is used for software specification, as from theoretical issues, as it is a non-compact logic and most existing results rely on compactness. We focus here on the revision of CTL models and present a characterization result for the revision of partial models. (shrink)

The article approaches the epistemological question on the concept of time from an anthropological psychology perspective. The differentiation between imminent perceptions and existence beyond imminent perception has been the earliest conceptualization of time found so far in the traces of human civilizations. The research differentiated psychological time from modern physics and astronomy as the basic hypothesis in the inquiries on the concept of time in physics and modern astronomy – is the physical unit of time an ontological existence of things (...) or an inter-subjective concept? The research adopts transcendental philosophy in the questioning of unconsciousness in the sociology of knowledge with a dissection between psychological time and physical units of time. With further questioning into the physics of time, and the nonphysical nature of time, I second with the primordial graviton background’s pragmatic approach, despite of the falsifiability of the Big Bang theory and inflation. (shrink)

The present article is devoted to a logical inquiry on the notions of permanence and termination, which play a central role in many areas of temporal reasoning. In the first part, we introduce a bimodal framework to represent these notions and provide a syntactic and semantic comparison with a monomodal framework representing the notion of future necessity. In the second part, we focus on the problem of defining synonymous logical systems over the two frameworks; as an example, we provide an (...) extended analysis of two systems, the monomodal K4 and the bimodal S4X. The third part of the article indicates possible developments of the proposed line of inquiry, such as finding a simple representation in the bimodal language of some interesting properties of time and identifying further pairs of synonymous systems. (shrink)

This book discusses fundamental topics on contemporary Ockhamism. The collected essays show how contemporary Ockhamism can impact areas of research such as semantics, metaphysics and also the philosophy of science. In addition, the volume hosts one historian of Medieval philosophy who investigates the way in which William of Ockham “in flesh and bone” construed time and, more generally, future contingency. The essays explore the different meanings of this theory. They cover three main topics, in particular. The first examines the thesis (...) that sentences and propositions about the future have a definite truth value, without any ensuing commitment to determinism or fatalism. The second topic looks at the problem whether the branching-time model needs to countenance a privileged branch (the so-called Thin Red Line). Finally, the third topic considers the idea that there are so-called soft facts. These would be the subject matter of sentences and propositions verbally about the present or the past, but metaphysically about a later time, and which might change in the future. Overall, the book provides an updated and rigorous idea of the debate about Ockhamism. It gives readers a deeper understanding into this philosophical approach influenced by William of Ockham, characterized by the rejection of the Aristotelian idea that, in order to preserve the contingency of the future, future contingents must be deemed neither true nor false. (shrink)

n this paper, a non-classical axiomatic system was introduced to classify all moods of Aristotelian syllogisms, in addition to the axiom "Every a is an a" and the bilateral rules of obversion of E and O propositions. This system consists of only 2 definitions, 2 axioms, 1 rule of a premise, and moods of Barbara and Datisi. By adding first-degree propositional negation to this system, we prove that the square of opposition holds without using many of the other rules of (...) classical logic (including double negation elimination). We then show that the Propositional Substructural Logic SLe is the best logic to study Aristotelian Syllogisms. Also, based on the IFLe square of opposition, the rules of conversation and the rules of negation are completely proved in Muzaffar's logic. For this purpose, we used the monadic first-order logic with the same standard deductive apparatus of quantifiers in classical logic, plus the axioms of "some a is an a" and "some not-a is a not-a". Finally, to show that there is no existential commitment to general terms in categorical logic, the Strong Four-Valued Relevant-classical Logic KR4 was used. With the same existential interpretation of the quantifiers and the standard translation of the quarter quantified. (shrink)

This paper explores mutable futurism, the view according to which the future can literally change—that is, it can happen that a future time t changes from containing an event E to lacking it. Mutable futurism has received little attention so far, and the details and implications of the view are underexplored in the literature. For instance, it currently lacks a precise metaphysical model and a formal semantics. Although we do not endorse mutable futurism, our goal here is to strengthen the (...) case for mutable futurism and help establish it as a worthy contender in the debate on the philosophy of time. To attain this goal, we try to make mutable futurism, along with its metaphysical and inferential commitments, as clear as possible, by providing it with a coherent metaphysical model and a plausible semantics, and we show that it can be backed by theoretical reasons. (shrink)

Potentialists think that the concept of set is importantly modal. Using tensed language as an heuristic, the following bar-bones story introduces the idea of a potential hierarchy of sets: 'Always: for any sets that existed, there is a set whose members are exactly those sets; there are no other sets.' Surprisingly, this story already guarantees well-foundedness and persistence. Moreover, if we assume that time is linear, the ensuing modal set theory is almost definitionally equivalent with non-modal set theories; specifically, with (...) Level Theory, as developed in Part 1. (shrink)

Non-bivalent semantics of the future tense assert that propositions regarding future contingents are neither true nor false. One of the most relevant non-bivalent semantics is supervaluationism :264–281, 1970; Thomason, in: Gabbay, Guenthner Handbook of philosophical logic, Springer, Berlin, 1984), which preserves important logical principles. Recently, non-bivalent semantics are under attack from some pragmatics arguments: these semantics would be incompatible with our practices of asserting future contingents and with the probability we ascribe to such assertions :251–271, 2014; Cariani and Santorio in (...) Mind 127:129–165, 2018). The aim of this paper is to defend supervaluationism against this kind of criticism. We argue that, if probability is interpreted as the subjective belief in a proposition and if a semantic contextualism is adopted, supervaluationism makes correct predictions concerning the norms that govern our practices of asserting future contingents. Obviously, other arguments can be proposed against supervaluationism, but they must be of a different kind, such as metaphysical arguments. (shrink)

We present the proof that the temporal logic of two-dimensional Minkowski spacetime is decidable, PSPACE-complete. The proof is based on a type of two-dimensional mosaic. Then, we present the modification of the proof so as to work for slower-than-light signals. Finally, a subframe of the slower-than-light Minkowski frame is used to prove the new result that the temporal logic of real intervals with during as the accessibility relation is also PSPACE-complete.

In traditional semantics for classical logic and its extensions, such as modal logic, propositions are interpreted as subsets of a set, as in discrete duality, or as clopen sets of a Stone space, as in topological duality. A point in such a set can be viewed as a "possible world," with the key property of a world being primeness—a world makes a disjunction true only if it makes one of the disjuncts true—which classically implies totality—for each proposition, a world either (...) makes the proposition true or makes its negation true. This chapter surveys a more general approach to logical semantics, known as possibility semantics, which replaces possible worlds with possibly partial "possibilities." In classical possibility semantics, propositions are interpreted as regular open sets of a poset, as in set-theoretic forcing, or as compact regular open sets of an upper Vietoris space, as in the recent theory of "choice-free Stone duality." The elements of these sets, viewed as possibilities, may be partial in the sense of making a disjunction true without settling which disjunct is true. We explain how possibilities may be used in semantics for classical logic and modal logics and generalized to semantics for intuitionistic logics. The goals are to overcome or deepen incompleteness results for traditional semantics, to avoid the nonconstructivity of traditional semantics, and to provide richer structures for the interpretation of new languages. (shrink)

This paper articulates in formal terms a crucial distinction concerning future contingents, the distinction between what is true about the future and what is reasonable to believe about the future. Its key idea is that the branching structures that have been used so far to model truth can be employed to define an epistemic property, credibility, which we take to be closely related to knowledge and assertibility, and which is ultimately reducible to probability. As a result, two kinds of claims (...) about future contingents—one concerning truth, the other concerning credibility—can be smoothly handled within a single semantic framework. (shrink)

In epistemic logic we are not only interested in the propositional knowledge expressed by “knowing that” operators, but also care about other types of knowledge used in natural language. In [1], Plaza proposed the “knowing value” operators and gave the complete axiomatization for the logic of knowledge with nonrigid designators. Moreover, in [2] Halpern and colleagues holds that, when analyzing a system in terms of knowledge, not only is the current state of knowledge of the agents in the system relevant, (...) but also how that state of knowledge changes over time. So we introduce temporal logic operators ‘next’ and ‘until’ to extend Plaza’s system. The completeness proof is highly non-trivial and we referred to the work of [2, 3]. (shrink)

Software-controlled bots, also called social bots, are computer programs that act like human users on social media platforms. Recent work on detection of social bots is dominated by machine learning approaches. In this paper we explore bot detection as a model checking problem. We introduce Temporal Network Logic which we use to specify social networks where agents can post and follow each other. In this logic we formalize different types of social bot behavior. These are formulas that are satisfied in (...) a model of a network with bots. We provide a simple algorithm to extract a logical model from a real-life social network. We show that we can reduce TNL to a fragment of linear temporal logic with past and use this to establish the computational efficiency of model checking for social bot detection. (shrink)

As a growing area of research, the philosophy of time is increasingly relevant to different areas of philosophy and even other disciplines. This book describes and evaluates the most important debates in philosophy of time, under several subject areas: metaphysics, epistemology, physics, philosophy of language, philosophy of mind, cognitive science, rationality, and art. -/- Questions this book investigates include: Can we know what time really is? Is time possible, especially given modern physics? Must there be time because we cannot think (...) without it? What do we experience of time? How might philosophy of time be relevant to understanding the mind-body relationship or evidence in cognitive science? Can the philosophy of time help us understand biases toward the future and the fear of death? How is time relevant to art – and is art relevant to philosophical debates about time? Finally, what exactly could time travel be? And could time travel satisfy emotions such as nostalgia and regret? -/- Through asking such questions, and showing how they might be best answered, the book demonstrates the importance philosophy of time has in contemporary thought. Each of the book’s 10 chapters begins with a helpful introduction and ends with study questions and an annotated list of further readings. This and a comprehensive bibliography at the end of the book prepare the reader to go further in their study of the philosophy of time. (shrink)