Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linear Temporal Justification Logics with Past Operators

Meghdad Ghari

TL;DR

This paper presents various temporal justification logics involving both past and future time modalities, and investigates the two well-known epistemic-temporal notions of no forgetting and no learning in the framework of justification logics.

Abstract

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 both past and future operators), and establish its soundness and completeness. Then we investigate several principles describing the interaction of justification and time.

Linear Temporal Justification Logics with Past Operators

TL;DR

This paper presents various temporal justification logics involving both past and future time modalities, and investigates the two well-known epistemic-temporal notions of no forgetting and no learning in the framework of justification logics.

Abstract

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 both past and future operators), and establish its soundness and completeness. Then we investigate several principles describing the interaction of justification and time.

Paper Structure

This paper contains 14 sections, 56 theorems, 125 equations.

Table of Contents

  1. Introduction
  2. Language
  3. Axioms
  4. Maximal consistent sets
  5. Semantics of $\textsf{LPLTL}^{\sf P}$
  6. Soundness and Completeness of $\textsf{LPLTL}^{\sf P}$
  7. Another semantics for $\textsf{LPLTL}^{\sf P}$
  8. Connecting principles
  9. Semantics
  10. $\textsf{LPLTL}^{\sf P}$ with indexed application operators
  11. Completeness for $(\textsf{generalize})$
  12. Internalization
  13. No forgetting and no learning
  14. Reasoning takes time

Key Result

lemma 1

The following formulas are provable in $\textsf{LTL}^{\sf P}$: In item 1, $(\textsf{MP})$ is the only rule that is used in the derivation.

Theorems & Definitions (128)

  • definition 1
  • remark 1
  • lemma 1
  • proof
  • lemma 2
  • lemma 3
  • lemma 4
  • lemma 5
  • definition 2
  • lemma 6
  • ...and 118 more