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)

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)

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)

A recurring issue in any formal model representing agents' (changing) informational attitudes is how to account for the fact that the agents are limited in their access to the available inference steps, possible observations and available messages. This may be because the agents are not logically omniscient and so do not have unlimited reasoning ability. But it can also be because the agents are following a predefined protocol that explicitly limits statements available for observation and/or communication. Within the broad literature (...) on epistemic logic, there are a variety of accounts that make precise a notion of an agent's "limited access" (for example, Awareness Logics, Justification Logics, and Inference Logics). This paper interprets the agents' access set of formulas as a constraint on the agents' information gathering process limiting which formulas can be observed. (shrink)

To date no investigation has sought to interpret key themes in Aristotle’s writings on metaphysics, e.g., substance, potentiality, actuality, proximate cause, etc., within the context of a temporal logic or logic of events. Essentially, what follows is a programmatic effort to interpret aspects of Aristotle’s insights in Book Lambda of the Metaphysics in terms of recent advances in the development of a temporal logic, while being attentive to the sense of the original text as far (...) as possible. The significance of such an enterprise lies in unearthing and clarifying conceptual interconnections in Aristotle’s metaphysical writings which would be difficult to fathom through other means. This project, however exploratory in its present form, seems feasible partly because of the fact that at numerous points in Aristotle’s thesis process metaphors from the study of biology are strikingly evident. Also, there is additional justification for the suggested analysis in that his work involves repeated references to the “lived” activity of one’s inquiring into the nature of things. Thus a view of Aristotle’s pronouncements which presupposes a logic of events, where events are analysed pragmatically, i.e., in terms of a language-user and the extension of whatever is claimed to have occurred, is not alien to the mode of expression with which he presents his views. (shrink)

Temporal Logic: From Ancient Ideas to Artificial Intelligence deals with the history of temporal logic as well as the crucial systematic questions within the field. The book studies the rich contributions from ancient and medieval philosophy up to the downfall of temporal logic in the Renaissance. The modern rediscovery of the subject, which is especially due to the work of A. N. Prior, is described, leading into a thorough discussion of the use of (...) class='Hi'>temporal logic in computer science and the understanding of natural language. Temporal Logic: From Ancient Ideas to Artificial Intelligence thus interweaves linguistic, philosophical and computational aspects into an informative and inspiring whole. (shrink)

This much-needed book provides a thorough account of temporal logic, one of the most important areas of logic in computer science today. The book begins with a solid introduction to semantical and axiomatic approaches to temporal logic. It goes on to cover predicate temporal logic, meta-languages, general theories of axiomatization, many dimensional systems, propositional quantifiers, expressive power, Henkin dimension, temporalization of other logics, and decidability results. With its inclusion of cutting-edge results and unifying (...) methodologies, this book is an indispensable reference for both the pure logician and the theoretical computer scientist. (shrink)

Much previous work in artificial intelligence has neglected representing time in all its complexity. In particular, it has neglected continuous change and the indeterminacy of the future. To rectify this, I have developed a first‐order temporal logic, in which it is possible to name and prove things about facts, events, plans, and world histories. In particular, the logic provides analyses of causality, continuous change in quantities, the persistence of facts (the frame problem), and the relationship between tasks (...) and actions. It may be possible to implement a temporal‐inference machine based on this logic, which keeps track of several “maps” of a time line, one per possible history. (shrink)

ABSTRACT A complete axiomatic system CTLrp is introduced for a temporal logic for finitely branching ω+ -trees in a language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTLrp. In particular, that yields a complete axiomatization for the translations of all valid CTL*-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a (...) way more expressive medium for reasoning about branching time. (shrink)

We investigate logical consequence in temporal logics in terms of logical consecutions. i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be 'correct' in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame 〈L, ≤, ≥〉 of all integer numbers, is the (...) prime object of our investigation. We describe consecutions admissible LDTL in a semantic way—via consecutions valid in special temporal Kripke/Hintikka models. Then we state that any temporal inference rule has a reduced normal form which is given in terms of uniform formulas of temporal degree 1. Using these facts and enhanced semantic techniques we construct an algorithm, which recognizes consecutions admissible in LDTL. Also, we note that using the same technique it follows that the linear temporal logic L (N) of all natural numbers is also decidable w.r.t. inference rules. So, we prove that both logics LDTL and L (N) are decidable w.r.t. admissible consecutions. In particular, as a consequence, they both are decidable (Known fact), and the given deciding algorithms are explicit. (shrink)

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a (...) way more expressive medium for reasoning about branching time. (shrink)

This work concerns the use of operators for past and future contingency in Priorean temporal logic. We will develop a system named C_t, whose language includes a propositional constant and prove that (I) C_t is complete with respect to a certain class of general frames and (II) the usual operators for past and future necessity are definable in such system. Furthermore, we will introduce the extension C_t(lin) that can be interpreted on linear and transitive general frames. The theoretical (...) result of the current work is that contingency can be treated as a primitive notion in reasoning about temporal modalities. (shrink)

I present a variant of with time, called, interpreted in standard Kripke semantics. On the syntactic level, is nothing but the extension of atemporal individual by: the future tense and past tense operators, and the operator of group agency for the grand coalition. A sound and complete axiomatisation for is given. Moreover, it is shown that supports reasoning about interesting normative concepts such as the concepts of achievement obligation and commitment.

Justification logics are a family of modal logics whose non-normal modalities are parametrised by a type-theoretic calculus of terms. The first justification logic was developed by Sergei Artemov to provide an explicit modal logic for arithmetical provability in which these terms were taken to pick out proofs. But, justification logics have been given various other interpretations as well. In this paper, we will rely on an interpretation in which the modality \ is read ‘S accepts (...) \ as justification for \’. Since it is often important to specify just how much confidence agents have in propositions on the basis of justifications, the logic will need to be extended if it is to provide a sufficiently general account. The primary purpose of this paper is to extend justification logic with the expressive resources to needed to do so. Thus, we will construct the justification logic with confidence ). While \ will be extremely general, capable of accommodating a wide range of interpretations, we provide motivation in terms of the notion of confidence deriving recent work by Paul and Quiggin :363–382, 2018). Under this understanding, confidence must only correspond to a partial ordering. We axiomatise \ and provide a sound and complete semantics. (shrink)

Developed by Arthur Prior, Temporal Logic allows to represent temporal information on a logical system using modal operators such as P, F, H or G, whose intuitive meaning is “it was sometime in the Past...”, “it will be sometime in the Future...”, “it Has always been in the past...” and “it will always Going to be in the future...” respectively. Valuation of formulae built from these operators are carried out on Kripke semantics, so Modal Logic and (...) Temporal Logic are consequently related. In fact, Temporal Logic is an extension of Modal one. Even when both logics mechanisms are able to formalize modal-temporal information with some accuracy, they suffer from a lack of expressiveness which Hybrid Logic can solve. Indeed, one of the problems of Modal Logic consists in its incapacity of naming specific points inside a model. As Temporal Logic is based on it, it cannot make such a thing neither. But First-Order Logic does can by means of constants and equality relation. Hybrid Logic, which results from combining Modal Logic and First-Order Logic, may solve this shortcoming. The main aim of this paper is to explain how Hybrid Logic emanates from Modal and Temporal ones in order to show what it adds to both logics with regard to information representation, why it is more expressive than them and what relation it maintains with the First-Order Correspondence Language. (shrink)

Developed by Arthur Prior, Temporal Logic allows to represent temporal information on a logical system using modal operators such as P, F, H or G, whose intuitive meaning is “it was sometime in the Past...”, “it will be sometime in the Future...”, “it Has always been in the past...” and “it will always Going to be in the future...” respectively. Valuation of formulae built from these operators are carried out on Kripke semantics, so Modal Logic and (...) Temporal Logic are consequently related. In fact, Temporal Logic is an extension of Modal one. Even when both logics mechanisms are able to formalize modal-temporal information with some accuracy, they suffer from a lack of expressiveness which Hybrid Logic can solve. Indeed, one of the problems of Modal Logic consists in its incapacity of naming specific points inside a model. As Temporal Logic is based on it, it cannot make such a thing neither. But First-Order Logic does can by means of constants and equality relation. Hybrid Logic, which results from combining Modal Logic and First-Order Logic, may solve this shortcoming. The main aim of this paper is to explain how Hybrid Logic emanates from Modal and Temporal ones in order to show what it adds to both logics with regard to information representation, why it is more expressive than them and what relation it maintains with the First-Order Correspondence Language. (shrink)

Several justification logics have been created, starting with the logic LP, [1]. These can be thought of as explicit versions of modal logics, or of logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. We begin by sketching the basics of justification logics and their relations with modal logics. Then we move to new material. Modal logics come in various strengths. For their (...) corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open. (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. (shrink)

This paper investigates modular combinations of temporal logic systems. Four combination methods are described and studied with respect to the transfer of logical properties from the component one-dimensional temporal logics to the resulting combined two-dimensional temporal logic. Three basic logical properties are analyzed, namely soundness, completeness, and decidability. Each combination method comprises three submethods that combine the languages, the inference systems, and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional (...) temporal languages with varying expressivity and varying degrees of transfer of logical properties. The temporalization method and the independent combination method are shown to transfer all three basic logical properties. The method of full join of logic systems generates a considerably more expressive language but fails to transfer completeness and decidability in several cases. So a weaker method of restricted join is proposed and shown to transfer all three basic logical properties. (shrink)

We study the topic of realization from classical justification logics in the context of the recently introduced Gödel justification logics. We show that the standard Gödel modal logics of Caicedo and Rodriguez are not realized by the Gödel justification logics and moreover, we study possible extensions of the Gödel justification logics, which are strong enough to realize the standard Gödel modal logics. On the other hand, we study the fragments of the standard Gödel modal logics, which (...) are realized by the usual Gödel justification logics. We prove the corresponding realization theorem by using Fitting’s merging of realizations as well as appropriate hypersequent calculi on the modal side, adapting the work by Metcalfe and Olivetti. For these hypersequent calculi, we also show a cut-elimination theorem. We provide natural semantical characterizations for all of these newly introduced logics. (shrink)

This paper presents an approach to artificial intelligence planning based on linear temporal logic (LTL). A simple and easy-to-use planning language is described, Planning Domain Description Language with control Knowledge (PDDL-K), which allows one to specify a planning problem together with heuristic information that can be of help for both pruning the search space and finding better quality plans. The semantics of the language is given in terms of a translation into a set of LTL formulae. Planning is (...) then reduced to “executing” the LTL encoding, i.e. to model search in LTL. The feasibility of the approach has been successfully tested by means of the system Pdk, an implementation of the proposed method. (shrink)

A new combined temporal logic called synchronized linear-time temporal logic (SLTL) is introduced as a Gentzen-type sequent calculus. SLTL can represent the n -Cartesian product of the set of natural numbers. The cut-elimination and completeness theorems for SLTL are proved. Moreover, a display sequent calculus δ SLTL is defined.

Temporal Logic: From Ancient Ideas to Artificial Intelligence deals with the history of temporal logic as well as the crucial systematic questions within the field. The book studies the rich contributions from ancient and medieval philosophy up to the downfall of temporal logic in the Renaissance. The modern rediscovery of the subject, which is especially due to the work of A. N. Prior, is described, leading into a thorough discussion of the use of (...) class='Hi'>temporal logic in computer science and the understanding of natural language. Temporal Logic: From Ancient Ideas to Artificial Intelligence thus interweaves linguistic, philosophical and computational aspects into an informative and inspiring whole. (shrink)

While specifications and verifications of concurrent systems employ Linear Temporal Logic , it is increasingly likely that logical consequence in image will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard image with temporal operations image and image . The prime result is an algorithm recognizing consecutions admissible in image, so we prove that image is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the (...) validity of consecutions in image and solving the satisfiability problem. We start by a simple reduction of logical consecutions of image to equivalent ones in the reduced normal form . Then we apply a semantic technique based on image-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in image. These conditions lead to an algorithm which recognizes consecutions admissible in image by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for image. (shrink)

Internalization is a key property of justification logics. It states that justification logics internalize their own notion of proof which is essential for the proof of the realization theorem. The aim of this note is to show how to make use of internalization to track where an agent’s knowledge comes from and how to apply this to the problem of data privacy.

Justification logics provide a framework for reasoning about justifications and evidence. In this article, we study a fuzzy variant of justification logics in which an agent’s justification for a belief has certainty degree between 0 and 1. We replace the classical base of justification logics with Hájek’s rational Pavelka logic. We introduce fuzzy possible world semantics with crisp accessibility relation and also single world models for our logics. We establish soundness and graded-style completeness for both (...) kinds of semantics. We also introduce extensions with product conjunction. Finally, we offer a solution to a variant of the sorites paradox in our fuzzy justification logics. (shrink)

One of time's most puzzling aspects concerns its ontological status: on the one hand, it is a subjective and relative notion, based on our conscious experience of successive events; yet, on the other hand, our civilization and technology are based on the understanding that something like objective, absolute Time exists. Some philosophers have taken this paradox so far as to conclude that time is unreal; others, accepting the existence of absolute time, have engaged in heated debates regarding its structure, be (...) it linear or circular, bounded or unbounded, dense or discrete. (shrink)

Justification Logic provides an axiomatic description of justifications and delegates the question of their nature to semantics. In this note, we address the conceptual issue of the logical type of justifications: we argue that justifications in the logical setting are naturally interpreted as sets of formulas which leads to a class of epistemic models that we call modular models . We show that Fitting models for Justification Logic naturally encode modular models and can be regarded as (...) convenient pre-models of the former. (shrink)

We introduce and study hierarchies of extensions of the propositional modal and temporal languages with pairs of new syntactic devices: point of reference-reference pointer which enable semantic references to be made within a formula. We propose three different but equivalent semantics for the extended languages, discuss and compare their expressiveness. The languages with reference pointers are shown to have great expressive power (especially when their frugal syntax is taken into account), perspicuous semantics, and simple deductive systems. For instance, Kamp's (...) and Stavi's temporal operators, as well as nominals (names, clock variables), are definable in them. Universal validity in these languages is proved undecidable. The basic modal and temporal logics with reference pointers are uniformly axiomatized and a strong completeness theorem is proved for them and extended to some classes of their extensions. (shrink)

Accounting for the epistemic contribution of deduction has been a pervasive problem for logicians interested in deduction, such as, among others, Jakko Hintikka. The problem arises because the conclusion validly deduced from a set of premises is said to be “contained” in that set; because of this containment relation, the conclusion would be known from the moment the premises are known. Assuming this, it is problematic to explain how we can gain knowledge by deducing a logical consequence implied by a (...) set of known premises. To address this problem, we offer an alternative account of the epistemic contribution of deduction as the process required to deduce a conclusion or a theorem, understanding such a process not only in terms of the number of steps in the derivation but also, more importantly, in terms of the reason for or justification for every step. That is, we do not know a proposition unless we have a justification or proof of that proposition. With this goal in mind, we develop a justification logic system which exhibits the epistemic contribution of a deductive derivation as the resulting justified formula. (shrink)

In the 1980s, Pollock’s work on default reasons started the quest in the AI community for a formal system of defeasible argumentation. The main goal of this paper is to provide a logic of structured defeasible arguments using the language of justification logic. In this logic, we introduce defeasible justification assertions of the type t : F that read as “t is a defeasible reason that justifies F”. Such formulas are then interpreted as arguments and (...) their acceptance semantics is given in analogy to Dung’s abstract argumentation framework semantics. We show that a large subclass of Dung’s frameworks that we call “warranted” frameworks is a special case of our logic in the sense that Dung’s frameworks can be obtained from justification logic-based theories by focusing on a single aspect of attacks among justification logic arguments and Dung’s warranted frameworks always have multiple justification logic instantiations called “realizations”. We first define a new justification logic that relies on operational semantics for default logic. One of the key features that is absent in standard justification logics is the possibility to weigh different epistemic reasons or pieces of evidence that might conflict with one another. To amend this, we develop a semantics for “defeaters”: conflicting reasons forming a basis to doubt the original conclusion or to believe an opposite statement. This enables us to formalize non-monotonic justifications that prompt extension revision already for normal default theories. Then we present our logic as a system for abstract argumentation with structured arguments. The format of conflicting reasons overlaps with the idea of attacks between arguments to the extent that it is possible to define all the standard notions of argumentation framework extensions. Using the definitions of extensions, we establish formal correspondence between Dung’s original argumentation semantics and our operational semantics for default theories. One of the results shows that the notorious attack cycles from abstract argumentation cannot always be realized as justification logic default theories. (shrink)

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (...) (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for S4LPN based on Artemov–Fitting models. (shrink)

Hybrid logics internalize their own semantics. Members of the newer family of justification logics internalize their own proof methodology. It is an appealing goal to combine these two ideas into a single system, and in this paper we make a start. We present a hybrid/justification version of the modal logic T. We give a semantics, a proof theory, and prove a completeness theorem. In addition, we prove a Realization Theorem, something that plays a central role for (...) class='Hi'>justification logics generally. Since justification logics are newer and less well-known than hybrid logics, we sketch their background, and give pointers to their range of applicability. We conclude with suggestions for future research. Indeed, the main goal of this paper is to encourage others to continue the investigation begun here. (shrink)

This volume constitutes the proceedings of the First International Conference on Temporal Logic (ICTL '94), held at Bonn, Germany in July 1994. Since its conception as a discipline thirty years ago, temporal logic is studied by many researchers of numerous backgrounds; presently it is in a stage of accelerated dynamic growth. This book, as the proceedings of the first international conference particularly dedicated to temporal logic, gives a thorough state-of-the-art report on all aspects of (...) temporal logic research relevant for computer science and AI. It contains 27 technical contributions carefully selected for presentation at ICTL '94 as well as three surveys and position papers. (shrink)

The logic of justification provides an in-depth analysis of the epistemic states of an agent. This paper aims at solving some of the problems to which the common interpretation of the operators of justification logic is subject by providing a framework in which a crucial distinction between potential and explicit justifiers is exploited. The paper is subdivided into three sections. The first section offers an introduction to a basic system LJ of justification logic and (...) to the problems concerning its interpretation. In the second section, three new systems of justification logic are introduced and characterised with respect to an appropriate semantics. The final section shows why the highlighted problems do not afflict the new systems and how it is possible to interpret LJ in the new framework. (shrink)

This paper will develop ideas from [44]. We will generalize their work in two directions. First, we provide axioms for justification logics over the base logic B and show that the logic permits a proof of the internalization theorem. Second, we provide alternative frames that more closely resemble the standard versions of the ternary relational frames, as well as a more general approach to the completeness proof. We prove that soundness and completeness hold for justification logics (...) over a wide variety of base logics. Finally, we will strengthen Belnap’s variable sharing for the justification logic context, demonstrating that the justifications are properly relevant justifications. (shrink)

A prominent issue in mainstream epistemology is the controversy about doxastic obligations and doxastic voluntarism. In the present paper it is argued that this discussion can benefit from forging links with formal epistemology, namely the combined modal logic of belief, agency, and obligation. A stit-theory-based semantics for deontic doxastic logic is suggested, and it is claimed that this is helpful and illuminating in dealing with the mentioned intricate and important problems from mainstream epistemology. Moreover, it is argued that (...) this linking is of mutual benefit. The discussion of doxastic voluntarism directs the attention of doxastic logicians to the notion of belief formation and thus to dynamic aspects of beliefs that have hitherto been neglected. The development of a formal language and semantics for ascriptions of belief formation may contribute to clarifying the contents and the implications of voluntaristic claims. A simple observation concerning other-agent nestings of stit-operators, for instance, may help illuminating the notions of making belief and responsibility for beliefs of others. In this way, stit-theory may serve as a bridge between mainstream and formal epistemology. (shrink)