Time-Stamped Claim Logic
Pith reviewed 2026-05-24 21:08 UTC · model grok-4.3
The pith
Time-Stamped Claim Logic provides a sound and complete sequent calculus that reduces evidence sets while removing inconsistencies according to trust relations.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
We introduce the Time-Stamped Claim Logic including a sound and complete sequent calculus that allows one to reduce the size of the collected set of evidence and removes inconsistencies, i.e., the logic ensures that the result is consistent with respect to the trust relations considered.
What carries the argument
The sound and complete sequent calculus for Time-Stamped Claim Logic, which incorporates trust relations to manage and reduce contradictory time-stamped claims.
If this is right
- Collected evidence from distributed sources can be systematically reduced in size.
- Inconsistencies are removed in a way that respects the given trust relations.
- The logic supports handling of large volumes of potentially contradictory claims.
- The calculus is demonstrated on a cyber-attribution case study.
Where Pith is reading between the lines
- The sequent calculus could be implemented in automated tools for real-time evidence processing.
- Extensions might allow trust relations themselves to change over time.
- Similar methods could apply to evidence aggregation in legal or sensor-network domains.
Load-bearing premise
Predefined trust relations between sources exist and can be applied to resolve contradictions without introducing new inconsistencies or requiring additional external validation.
What would settle it
A concrete set of time-stamped claims together with given trust relations for which the sequent calculus fails to produce a reduced and consistent result would falsify the claim.
Figures
read the original abstract
The main objective of this paper is to define a logic for reasoning about distributed time-stamped claims. Such a logic is interesting for theoretical reasons, i.e., as a logic per se, but also because it has a number of practical applications, in particular when one needs to reason about a huge amount of pieces of evidence collected from different sources, where some of the pieces of evidence may be contradictory and some sources are considered to be more trustworthy than others. We introduce the Time-Stamped Claim Logic including a sound and complete sequent calculus that allows one to reduce the size of the collected set of evidence and removes inconsistencies, i.e., the logic ensures that the result is consistent with respect to the trust relations considered. In order to show how Time-Stamped Claim Logic can be used in practice, we consider a concrete cyber-attribution case study.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper defines Time-Stamped Claim Logic for reasoning about distributed time-stamped claims collected from sources with varying trust levels. It presents a sequent calculus asserted to be sound and complete that reduces the size of the evidence set and eliminates inconsistencies in a manner consistent with the given trust relations. The approach is illustrated via a concrete cyber-attribution case study.
Significance. If the soundness and completeness results hold, the logic supplies a formal mechanism for pruning contradictory evidence in large distributed collections while respecting external trust parameters. This has clear relevance to evidence management tasks in security and attribution domains. The sequent-calculus presentation and the case study together constitute a self-contained demonstration of the framework's intended use.
minor comments (2)
- The abstract states that the sequent calculus is sound and complete, but the manuscript would benefit from an explicit pointer (e.g., to the relevant theorem number) in the introduction so that readers can locate the proof immediately.
- Notation for time-stamped claims and the trust-ordering relation should be introduced with a small illustrative example before the full sequent rules are presented, to aid readability.
Simulated Author's Rebuttal
We thank the referee for the positive summary of our paper and the recommendation for minor revision. The assessment correctly identifies the core contributions of Time-Stamped Claim Logic, the sequent calculus, and the cyber-attribution case study.
Circularity Check
No significant circularity detected
full rationale
The paper introduces a new Time-Stamped Claim Logic as a formal definition together with a sequent calculus whose soundness and completeness are established by standard proof techniques. Trust relations are external parameters supplied by the user; the calculus operates on them to prune evidence and eliminate inconsistencies without any fitted parameters, self-referential equations, or load-bearing self-citations that reduce the central result to its own inputs. The derivation chain consists of syntactic definitions, inference rules, and meta-theoretic proofs that are independent of the target conclusions; no step equates a derived quantity to a prior fit or renames an input as a prediction. This is the normal case of a self-contained logic presentation.
Axiom & Free-Parameter Ledger
axioms (2)
- domain assumption Sequent calculus rules support soundness and completeness for the defined language
- domain assumption Trust relations between sources are given as input and sufficient to resolve all inconsistencies
invented entities (1)
-
Time-stamped claim
no independent evidence
Reference graph
Works this paper leans on
-
[1]
M. H. Almeshekah and E. H. Spafford. Planning and integrating deception into computer security defenses. In NSPW, pages 127–138. ACM, 2014
work page 2014
-
[2]
M. H. Almeshekah and E. H. Spafford. Cyber security deception. In S. Jajodia, V. S. Sub- rahmanian, V. Swarup, and C. Wang, editors, Cyber Deception: Building the Scientific Foundation, pages 23–50. Springer, 2016
work page 2016
-
[3]
S. Artemov. Explicit provability and constructive semantics. The Bulletin of Symbolic Logic, 7(1):1–36, 2001
work page 2001
-
[4]
S. Artemov. The logic of justification. The Review of Symbolic Logic, 1(4):477–513, 2008
work page 2008
-
[5]
B. Aziz. Modelling and refinement of forensic data acquisition specifications. Digital Investigation, 11(2):90–101, 2014
work page 2014
- [6]
-
[7]
N. Beebe. Digital forensic research: The good, the bad and the unaddressed. In Ad- vances in Digital Forensics V - Fifth IFIP WG 11.9 International Conference on Digital Forensics, pages 17–36, 2009
work page 2009
-
[8]
S. Bucheli, R. Kuznets, and T. Studer. Justifications for common knowledge. Journal of Applied Non-Classical Logics, 21(1):35–60, 2011
work page 2011
-
[9]
M. Caminada and D. M. Gabbay. A logical account of formal argumentation. Studia Logica, 93(2-3):109–145, 2009
work page 2009
-
[10]
W. A. Carnielli and A. Rodrigues. An epistemic approach to paraconsistency: a logic of evidence and truth. Synthese, in print
-
[11]
Analysis of the cyber attack on the Ukrainian power grid
Defense Use Case. Analysis of the cyber attack on the Ukrainian power grid. Electricity Information Sharing and Analysis Center (E-ISAC) , 2016
work page 2016
-
[12]
P. M. Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77(2):321–357, 1995. 26
work page 1995
-
[13]
M. Fitting. A quantified logic of evidence. Annals of Pure and Applied Logic , 152(1- 3):67–83, 2008
work page 2008
-
[14]
M. Fontani, T. Bianchi, A. De Rosa, A. Piva, and M. Barni. A framework for decision fu- sion in image forensics based on Dempster-Shafer theory of evidence. IEEE Transactions on Information Forensics and Security , 8(4):593–607, 2013
work page 2013
-
[15]
D. M. Gabbay. Fibring argumentation frames. Studia Logica, 93(2-3):231–295, 2009
work page 2009
-
[16]
R. K. Goutam. The problem of attribution in cyber security. International Journal of Computer Applications, Foundation of Computer Science , 131(7):34–36, 2015
work page 2015
-
[17]
J. Y. Halpern and R. Pucella. A logic for reasoning about evidence. Journal of Artificial Intelligence Research, 26:1–34, 2006
work page 2006
-
[18]
On digital image trustworthiness
Donghui Hu, Xiaotian Zhang, Yuqi Fan, Zhong-Qiu Zhao, Lina Wang, Xintao Wu, and Xindong Wu. On digital image trustworthiness. Applied Soft Computing , 48:240 – 253, 2016
work page 2016
-
[19]
E. Karafili, M. Cristani, and L. Vigan` o. A formal approach to analyzing cyber-forensics evidence. In Proceedings of ESORICS 2018, Part I , pages 281–301, 2018
work page 2018
-
[20]
E. Karafili, L. Wang, A. C. Kakas, and E. Lupu. Helping forensic analysts to attribute cyber-attacks: An argumentation-based reasoner. In PRIMA, volume 11224, pages 510–
-
[21]
I. Kokkinis, Z. Ognjanovi´ c, and T. Studer. Probabilistic justification logic. In Logical Foundations of Computer Science , volume 9537 of Lecture Notes in Computer Science , pages 174–186. Springer, 2016
work page 2016
-
[22]
J. Lurie. Probabilistic justification logic. Philosophies, 3(1):2, 2018
work page 2018
- [23]
- [24]
-
[25]
A. Sernadas, J. Rasga, and C. Sernadas. On probability and logic. Portugaliae Mathe- matica, 74(4):267–313, 2017
work page 2017
-
[26]
C. Sernadas, J. Rasga, and A. Sernadas. Preservation of Craig interpolation by the product of matrix logics. Journal of Applied Logic , 11(3):328–349, 2013
work page 2013
-
[27]
J. van Benthem, D. Fern´ andez-Duque, and E. Pacuit. Evidence logic: a new look at neighborhood structures. In Advances in Modal Logic, volume 9, pages 97–118. College Publications, London, 2012
work page 2012
-
[28]
J. van Benthem and E. Pacuit. Logical dynamics of evidence. In Logic, Rationality, and Interaction, volume 6953 of Lecture Notes in Computer Science , pages 1–27. Springer, 2011. 27
work page 2011
-
[29]
H. van Dirmarsch, W. van der Hoek, and B. Kooi. Dynamic Epistemic Logic. Springer, 2008
work page 2008
-
[30]
D. A. Wheeler and G. N. Larsen. Techniques for cyber attack attribution. Technical report, Institute for Defense Analyses Alexandria VA, 2003. A Some Proofs of Sections 5 and 6 Proposition A.1 (a.k.a. Proposition 5.2) The rules of the sequent calculus are sound. Proof: It is quite straightforward to see that the rules Ax, Cut, ER, ES and ET are sound. (EC...
work page 2003
-
[31]
ψ is t1∼= t2. (a) Assume that t1∼= t2∈ ΨL. Then ( t1, t2)∈∼=IH and so IH ρ⊩ t1∼= t2. (b) Assume that t1∼= t2∈ ΨR. Then ( t1, t2)∈∼=IH and so IH ρ̸⊩ t1∼= t2
-
[32]
ψ is a1⊴p a2. (a) Assume that a1⊴p a2∈ ΨL. Then ( a1, a2)∈⊴IH p and so IH ρ⊩ a1⊴p a2. (b) Assume that a1⊴p a2∈ ΨR. Then ( a1, a2) /∈⊴IH p and so IH ρ̸⊩ a1⊴p a2
-
[33]
ψ is∀x. x⊴p a. (a) Assume that ∀x. x⊴p a∈ ΨL. Then for each a1∈ X′ A we have a1⊴p a∈ ΨL. Hence, IH ρ⊩ a1⊴p a for each a1∈ DA and so Iρ⊩∀x. x⊴p a. (b) Assume that ∀x. x⊴p a∈ ΨR. Then there is a′∈ X′ A such that a′⊴p a∈ ΨR. Therefore, Iρ̸⊩ a′⊴p and so Iρ̸⊩∀x. x⊴p a
-
[34]
ψ is a : t· p. (a) Assume that a : t· p∈ ΨL. Then V (p, a, t) = 1 and IH ρ⊩ a : t· p. (b) Assume that a : t· p∈ ΨR. Then V (p, a, t)∈{ 0, 1 2} and so IH ρ̸⊩ a : t· p
-
[35]
(a) Assume that a :−(t· p)∈ ΨL
ψ is a :−(t· p). (a) Assume that a :−(t· p)∈ ΨL. Then V (p, a, t) = 0. Hence IH ρ⊩ a :−(t· p). (b) Assume that a :−(t· p)∈ ΨR. Then V (p, a, t)∈{ 1, 1 2} and so IH ρ̸⊩ a :−(t· p)
-
[36]
ψ is a : φ. (a) Assume that a : φ∈ ΨL. Then, for each a′ ∈ X′ A either a⊴var(φ) a′ ∈ ΨR or a′ :−φ∈ ΨR. Hence, by the induction hypothesis, for each a′∈ X′ A either IH ρ̸⊩ a⊴var(φ)a′ or IH ρ̸⊩ a′ :−φ. Hence for each a′∈ X′ A if IH ρ⊩ a⊴var(φ)a′ then IH ρ̸⊩ a′ :−φ. Let ρ′ be an assignment such that ρ′≡A′ b ρ and IH ρ′⊩ a⊴var(φ) b. Thus IH ρ⊩ a⊴var(φ) ρ′(b)....
-
[37]
ψ is φ∈ KP . 30 (a) Assume that φ∈ ΨL. Then there is a′∈ X′ A such that a′ : φ, a′ : φ∈ ΨL and for every a∈ X′ A either a :−φ∈ ΨR or a : −φ∈ ΨR. Thus, by the induction hypothesis, there is a′ ∈ X′ A such that IH ρ⊩ a′ : φ and IH ρ⊩ a′ : φ and for each a∈ X′ A either IH ρ̸⊩ a :−φ or IH ρ̸⊩ a : −φ. We now show that IH ρ⊩ φ. Let ρ′ ≡A′ b ρ be such that IH ρ′...
-
[38]
ψ is a :: (φ1, . . . , φn/φ). (a) Assume that a :: (φ1, . . . , φn/φ)∈ ΨL. Then either φi∈ ΨR for some i = 1, . . . , n or a : φ∈ ΨL. Then, by the induction hypothesis, either IH ρ̸⊩ φi for some i = 1, . . . , n or IH ρ⊩ a : φ. Therefore, IH ρ⊩ a :: (φ1, . . . , φn/φ). (b) Assume that a :: (φ1, . . . , φn/φ)∈ ΨR. Then if φ1, . . . , φn∈ ΦL then a : φ∈ ΨR....
-
[39]
Assume by contradiction that β∈ ΨL and β∈ ΨR
Either β /∈ ΨL or β /∈ ΨR where β is of the form a : φ, t1∼= t2 and a1⊴p a2. Assume by contradiction that β∈ ΨL and β∈ ΨR. Hence, there are 1 ≤ i, j≤ n such that β∈ Γ′ i and β∈ ∆′ j. Observe that any rule preserves β. Therefore, β∈ Γ′ n∩ ∆′ n and so Γ′ n→ ∆′ n is an axiom contradicting the hypothesis that the branch is open
-
[40]
Assume, by contradiction, that β is not in Ψ L∪ ΨR
Either β∈ ΨL or β∈ ΨR where β is of the form a : φ, t1∼= t2 and a1⊴p a2. Assume, by contradiction, that β is not in Ψ L∪ ΨR. Consider the branch Γ ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n Γ′ n→ ∆′ n, β using the cut rule in the last step. Observe that this branch is still analytical. Indeed β does not occur in ( iR)n and no fresh variables are involved. Hence we get a con...
-
[41]
Immediate by rule (ER) since the branch is open
t∼= t /∈ ΨR. Immediate by rule (ER) since the branch is open. Similarly for ⊴p
-
[42]
If t1∼= t2∈ ΨL then t2∼= t1 /∈ ΨR. Suppose that t1∼= t2∈ ΨL. Then if t2∼= t1∈ ΨR we could conclude that the branch was not open using rule (ES)
-
[43]
Suppose that t1∼= t2, t2∼= t3∈ ΨL
If t1 ∼= t2, t2 ∼= t3 ∈ ΨL then t1 ∼= t3 /∈ ΨR and similarly for ⊴p. Suppose that t1∼= t2, t2∼= t3∈ ΨL. Then if t1∼= t3∈ ΨR we could conclude that the branch was not open using rule (ET)
-
[44]
Suppose that t1∼= t2, [a : φ]t1 t2∈ ΨL
If t1∼= t2, [a : φ]t1 t2∈ ΨL then a : φ /∈ ΨR. Suppose that t1∼= t2, [a : φ]t1 t2∈ ΨL. Then if a : φ∈ ΨR we could conclude that the branch was not open using rule (EC)
-
[45]
The proof is similar to the one of (6)
If a1⊴p a2, a2⊴p a1, [a : φ]a1 a2∈ ΨL then a : φ /∈ ΨR. The proof is similar to the one of (6)
-
[46]
x⊴p a ∈ ΨR then there is a′ ∈ X′ A such that a′⊴p a ∈ ΨR
If ∀x. x⊴p a ∈ ΨR then there is a′ ∈ X′ A such that a′⊴p a ∈ ΨR. Assume that ∀x. x⊴p a∈ ΨR. Suppose, by contradiction, that for every a′∈ X′ A, a′⊴p a /∈ ΨR. Then, rule (AMR) was not applied to ∀x. x⊴p a and so∀x. x⊴p a∈ ∆′ n. Consider the branch Γ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n Γ′ n→ (∆′ n\{∀ x. x⊴p a}), b⊴p a using in the last step the rule (AMR) where b is not...
-
[47]
x⊴p a∈ ΨL then a1⊴p a∈ ΨL for each a1∈ X′ A
If ∀x. x⊴p a∈ ΨL then a1⊴p a∈ ΨL for each a1∈ X′ A. Assume that ∀x. x⊴p a∈ ΨL. Suppose, by contradiction, that there is a1∈ X′ A such that a1⊴p a /∈ ΨL. Observe that ∀x. x⊴p a is in Γ′ n. Consider the branch Γ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n a1⊴p a, Γ′ n→ ∆′ n using in the last step the rule (AML). Observe that this branch is still analytical. So the original bran...
-
[48]
If a : φ∈ ΨL then a :−φ∈ ΨR. Suppose that a : φ∈ ΨL. Assume, by contradiction that a :−φ /∈ ΨR. Consider the branch Γ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n Γ′ n→ ∆′ n, a :−φ using in the last step the rule (NS). Observe that this branch is still analytical. Indeed a :−φ does not occur in (iR)n and no fresh variables are involved. Hence we get a contradiction since the g...
-
[49]
The proof is similar to one of (10)
If t1∼= t2, a :−(t1· p)∈ ΨR then a : t2· p∈ ΨR. The proof is similar to one of (10)
-
[50]
If a : φ∈ ΨR then, there is a′∈ X′ A such that a⊴var(φ) a′, a′ :−φ∈ ΨL. Assume that a : φ∈ ΨR. Suppose, by contradiction, that for every a′∈ X′ A either a⊴var(φ) a′ /∈ ΨL or a′ :−φ /∈ ΨL. In both cases, rule (SCR) was not applied to a : φ. Then a : φ is in ∆′ n. Consider the branch Γ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n a⊴var(φ) b, b :−φ, Γ′ n→ (∆′ n\{ a : φ}) using in...
-
[51]
If a : φ∈ ΨL then, for each a′ ∈ X′ A either a⊴var(φ) a′ ∈ ΨR or a′ :−φ∈ ΨR. Assume that a : φ∈ ΨL. Suppose, by contradiction, that there is a′∈ X′ A such that a⊴var(φ) a′ /∈ ΨR and a′ :−φ /∈ ΨR. Observe that a : φ is in Γ′ n. Consider the branch Γ′ 1 → ∆′ 1··· Γ′ n → ∆′ n Γ′ n → ∆′ n, a⊴var(φ) a′ using in the last step the rule (SCL). Observe that this b...
-
[52]
If φ∈ ΨR then either there exists a′∈ X′ A such that a′ :−φ, a′ : −φ∈ ΨL or for each a∈ X′ A either a : φ∈ ΨR or a : φ∈ ΨR. Suppose that φ∈ ΨR. Assume, by contradiction, that the thesis does not hold. Then, φ∈ ∆′ n since rule (SKR) was not applied to φ in the branch. Consider the branch Γ ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n b :−φ, b : −φ, Γ′ n → ∆′ n using in the las...
-
[53]
If φ∈ ΨL then there is a′∈ X′ A such that a′ : φ, a′ : φ∈ ΨL and for each a∈ X′ A either a :−φ∈ ΨR or a : −φ∈ ΨR. Assume that φ∈ ΨL. Suppose, by contradiction and with no loss of generality, that for every a′∈ X′ A, either a′ : φ /∈ ΨL or a′ : φ /∈ ΨL. Then rule (KL) was not applied in the branch to φ. Hence, φ is in Γ′ n. Consider the branch Γ′ 1→ ∆′ 1··...
-
[54]
If a :: ( φ1, . . . , φn/φ)∈ ΨR then if φ1, . . . , φn∈ ΨL then a : φ∈ ΨR. Assume that a :: ( φ1, . . . , φn/φ)∈ ΨR and φ1, . . . , φn ∈ ΨL. Assume, by contradiction, that a : φ /∈ ΨR. Then rule (CR1) was not applied in the branch to a :: (φ1, . . . , φn/φ). Hence, a :: (φ1, . . . , φn/φ) is in ∆′ n. Consider the branch Γ′ 1→ ∆′ 1··· Γ′ n→ ∆′ n φ1, . . . ...
-
[55]
, φn/φ)∈ ΨL then either φi∈ ΨR for some i = 1 ,
If a :: ( φ1, . . . , φn/φ)∈ ΨL then either φi∈ ΨR for some i = 1 , . . . , n or a : φ∈ ΨL. Suppose that a :: ( φ1, . . . , φn/φ) ∈ ΨL. Assume, by contradiction, that φi /∈ ΨR for every i = 1 , . . . , n and a : φ /∈ ΨL. Then rule (CR2) was not applied in the branch to a :: (φ1, . . . , φn/φ). Hence, a :: (φ1, . . . , φn/φ) is in Γ′ n. Consider the branch...
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.