Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

A fixpoint operator makes non-Markovian temporal logic exact and fast.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

LAT logic adds time and open-world uncertainty to annotated logic programs; its PyReason engine dynamically materializes only the atoms it needs, showing orders-of-magnitude speedups and memory savings.

T0 review reviewed 2026-08-05 challenge →

load-bearing objection Solid engineering with a real implementation and credible experiments, but the paper's central convergence theorem is not proven for the lattice it defines, and the main correctness proof is circular. the 3 major comments →

arxiv 2509.02958 v1 pith:YPUOQG2C submitted 2025-09-03 cs.LO cs.AIcs.LGcs.PL

Lattice Annotated Temporal (LAT) Logic for Non-Markovian Reasoning

Kaustuv Mukherji , Jaikrishna Manojkumar Patil , Dyuman Aditya , Paulo Shakarian , Devendra Parkar , Lahari Pokala , Clark Dorman , Gerardo I. Simari This is my paper
classification cs.LO cs.AIcs.LGcs.PL MSC 68N1703B7068T2768Q60
keywords temporal logic programminggeneralized annotated logic programslower lattice semanticsSkolemizationnon-Markovian reasoningfixpoint operatorknowledge graph completionreinforcement learning
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper introduces Lattice Annotated Temporal (LAT) logic, a temporal extension of generalized annotated logic programs in which facts carry interval truth values and rules carry time delays. The authors aim to show that one fixpoint operator, Γ, computes exact entailments for these programs, so a rule's conclusion at time t+Δt follows from premises satisfied at t, and that the lower-lattice annotation structure keeps this reasoning tractable. Because atoms whose truth is completely unknown sit at the bottom of the lattice, they do not need to be materialized, and new constants are created only when rules fire. If the theoretical and empirical claims hold, temporal logic programming becomes a practical, explainable engine for non-Markovian simulation, knowledge graph completion, and reinforcement learning rather than an intractable formalism.

Core claim

The central claim is that for a consistent LAT program Π, entailment of a timed annotated literal a:μ is exactly the condition μ ≤ lfp(Γ)(a), where Γ is the fixpoint operator that maps an interpretation (an assignment of interval annotations to ground literals at each time point) to the interpretation taking suprema of all annotations derivable from rules whose bodies are satisfied at the appropriate earlier time. This makes the least fixpoint of Γ the canonical model, so deductive inference is exact rather than approximate. The companion performance claim is that grounding can be Skolemized: since the bottom lattice element represents total uncertainty, atoms at the bottom can be omitted fr

What carries the argument

The load-bearing object is the fixpoint operator Γ over time-indexed interpretations. It revises the entire grid of ground literal/time-point annotations at once, which is what lets rules with heterogeneous delays Δt express non-Markovian dependencies. The supporting mechanism is the lower-lattice annotation structure: annotations are intervals within [0,1] ordered by reverse inclusion, making [0,1] (total uncertainty) the bottom; atoms resting at the bottom need not be allocated memory, and Skolemization creates constants only when rules fire.

Load-bearing premise

The paper's termination and tractability guarantees assume the truth-value lattice has finite height—only finitely many strictly increasing levels—but the lattice it defines, subsets of the real unit interval, has infinitely many such levels.

What would settle it

Build a consistent LAT program with a single ground fact and a delayed rule that, at each Γ application, raises an atom's annotation one step up an infinite chain of intervals (e.g., [0,1], [0.5,1], [0.75,1], ...). If Γ does not reach a fixpoint within height(M)×|A|×t_max iterations—or if that bound is not finite—the convergence theorem fails.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • For any consistent LAT program, entailment of a timed literal reduces to checking whether its annotation sits below the least fixpoint of Γ, so exact inference is a single monotone computation rather than a search over models.
  • Skolemized grounding keeps the materialized atom set proportional to rule firings: each fixpoint step adds at most the sum over rules of the products of their body support sizes, so sparse domains stay sparse.
  • Because atoms at the bottom lattice element are implicitly uncertain and never stored, LAT programs can be run over infinite or open constant domains without materializing every possible ground atom in advance.
  • The temporal delay parameter Δt lets a single rule set simulate non-Markovian dynamics, and in the grid-world experiments including observations from the previous timestep raises the best policy win rate from 59% to 85%.
  • In the reported benchmarks, the Skolemizing engine reduces runtime by up to three orders of magnitude and memory by up to five orders of magnitude while matching or improving task performance, indicating the approach scales past full-grounding systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Editorial extension: to make the termination bound finite as written, one can restrict the annotation lattice to a fixed finite set of intervals (e.g., a user-specified grid); the fixpoint machinery is unchanged and the bound becomes finite.
  • Editorial extension: Theorem 4.4 gives a cheap pre-inference cost estimate—count support sizes per predicate and compute rule-body products—which the paper does not automate; a tool could flag rules whose product explodes before running.
  • Editorial extension: the reinforcement-learning results suggest replacing the grid-world wrapper with learned interval or probabilistic annotations so the same fixpoint machinery acts as a differentiable simulator, connecting to tractable probabilistic circuits.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces Lattice Annotated Temporal (LAT) logic, a temporal extension of Generalized Annotated Logic Programs in which annotations come from a lower lattice. The central theoretical claims are: (i) a fixpoint operator Gamma provides exact deductive inference in the sense that entailment of a TAF coincides with the annotation lying below lfp(Gamma) (Theorem 4.1); (ii) consistent programs converge in a finite number of Gamma applications bounded by height(M)*|A|*t_max (Theorem 4.2); (iii) inconsistency can be detected within a polynomial number of applications (Theorem 4.3); and (iv) Skolemization bounds the growth of ground atoms (Theorem 4.4). The paper also describes the open-source PyReason implementation and reports experiments on geospatial simulation, knowledge graph completion, and reinforcement learning, claiming several orders of magnitude speedup and memory reduction.

Significance. If the theoretical foundations were fully established, LAT logic would be a useful contribution: it offers a concrete, explainable, non-Markovian temporal reasoning formalism with an open-source implementation, reproducible experiment commands, and a clear way to leverage lower-lattice annotations for open-world grounding. The paper's strengths are its extensive empirical evaluation, the public implementation, and the fact that the performance claims are stated in a falsifiable form. However, the convergence and exactness results are not rigorously established as written: Theorem 4.2 relies on a finite lattice height that the defined annotation lattice does not have, and the proof of Theorem 4.1(3) is circular. These are load-bearing issues because the advertised tractable exact inference rests on them.

major comments (3)
  1. [Section 3.1, Definition 3.2; Section 4.1, Theorem 4.2] Theorem 4.2 states that lfp(Gamma) = Gamma^x with x = height(M) * |A| * t_max. This uses height(M) as a finite quantity, but the lattice M defined in Section 3.1 consists of subsets/closed intervals of [0,1] with [0,1] as the bottom element under the lower-lattice order. Under that order, the chain [0,1] superset [0,1/2] superset [0,1/3] superset ... is an infinite ascending chain, so height(M) is unbounded. The proof only observes that annotations 'must stay the same or increase monotonically'; it does not bound the number of lattice levels a single annotation can traverse. Hence x is not a finite number as stated, and the claimed termination guarantee is unsupported. The same gap infects Theorem 4.3's assertion that inconsistency is detected in a 'finite, polynomial number of applications.' The theorem should be restated under a finite-height annotation lattice, or a program-specific b
  2. [Section 4.1, Theorem 4.1(3)] The proof of the entailment/fixpoint equivalence is circular. The forward direction says that if Pi entails a:mu then 'there is a series of logical constructs that allow us to derive a:mu'—but that derivability assertion is exactly the completeness half of what is being proved. The converse says that if mu <= lfp(Gamma)(a) then entailment must hold because 'Gamma directly leverages the elements of Pi,' which is likewise the soundness half stated without proof. What is needed is a model-theoretic argument showing that lfp(Gamma) is the least model of Pi, together with an induction on Gamma applications that connects derivability to semantic entailment. As written, Theorem 4.1(3) is an assertion rather than a proof.
  3. [Section 4.2, Theorem 4.4 and Section 6.2.1] Section 6.2.1 reports 'cases where the number of constants produced exceeds the theoretical bound (in lower inference steps)' and attributes this to the choice of parameters. If Theorem 4.4 is an upper bound, no parameter choice should allow the measured count to exceed it. This discrepancy must be resolved: either the theorem's assumptions do not cover the experimental configuration, or the empirical measurement counts a different quantity than the theorem. As written, the experimental section appears to contradict the very bound it is meant to validate.
minor comments (5)
  1. [Section 3.1, Definition 3.2] The text says M consists of subsets of [0,1], then describes elements as intervals, and says 'upper elements are all intervals [l,u] where l=u'—this appears to be a typo for l<=u. Please clarify whether M is the set of all subsets, the set of closed intervals, or a finite sub-lattice, and define the ordering symbol used in Definition 3.7.
  2. [Section 3.2, Definition 3.13] The definition of Gamma uses sup over annoSet. It should be stated explicitly that M is a complete lattice and that the supremum used is with respect to the lower-lattice order; otherwise the well-definedness of Gamma is not immediate.
  3. [Section 4.1, footnote 1] The footnote says a version of Section 4.1 appeared in the authors' earlier work [61]. Since the paper claims these results for the temporal extension, the proofs should be self-contained; the one-sentence justifications for Theorem 4.1(1) and (2) are not sufficient.
  4. [Section 4.1, Theorem 4.3] The statement says 'for value i' without quantification. It should read 'there exists i' or 'for some i,' depending on the intended reading.
  5. [Algorithm 2] The algorithm uses Nbr(v), Rnbr(w), and thresholds Theta_i that are not formally defined in the syntax section. Please define these before the algorithm or point to where they are introduced.

Circularity Check

2 steps flagged

Central exact-inference theorem is proven by assuming the model-theoretic/operational equivalence it claims; the same result is explicitly imported from the authors' own prior [61].

specific steps
  1. other [Theorem 4.1(3), proof (Section 4.1)]
    "Suppose BWOC that Π entails 𝑎 : 𝜇 and 𝜇 > lfp(Γ)(𝑎). However, this would imply there is a series of logical constructs that allow us to derive 𝑎 : 𝜇 at some time t, and this would trivially be reflected in the iterative applications of the Γ operator. Going the other way, BWOC if 𝜇 ≤ lfp(Γ)(𝑎) but Π does not entail 𝑎 : 𝜇 would imply that there is no application of the constructs in Π that lead to the deductive conclusion of 𝑎 : 𝜇 at any time t; however this is again contradicted by the fact that Γ directly leverages the elements of Π."

    The theorem asserts that model-theoretic entailment (Π |=ent a:μ) coincides with the least fixpoint of the rule-application operator Γ. The proof's first direction infers derivability by Γ from entailment, which is exactly the completeness half of the theorem; the second direction infers entailment from Γ-derivability, which is the soundness half. Since Γ is defined as the operator that directly applies the program's rules, the identification of lfp(Γ) with entailment is the conclusion, not a consequence of the definitions. No minimal-model, induction-on-derivations, or compactness argument is given. The proof therefore assumes the statement being proved.

  2. self citation load bearing [Section 3 (Technical Preliminaries) and footnote to Section 4.1]
    "The lower lattice semantics were introduced in our prior work [61], which did not include temporal extensions, implementation, or many of the theoretical results in this paper. ... A version of the results in Section 4.1 presented in an earlier conference paper from the authors in [61]; however, here we expand on them to include GAPs with temporal structures."

    The paper's central claim of exact deductive inference is not independently demonstrated here: Theorem 4.1 is explicitly a version of results from the authors' own [61], and the proof supplied is the same assertion-based argument that assumes what it must show. The lower-lattice semantics that drive the open-world/Skolemization claims are also attributed to [61]. Because [61] is not machine-checked, code-reproduced, or independently falsified within this paper, the load-bearing correctness result rests on an unverified self-citation rather than on a self-contained derivation.

full rationale

The paper has substantial independent content: the LAT temporal extension, the Skolemization-based grounding bound of Theorem 4.4 (a genuine worst-case inequality), the implementation, and the measured speedups/memory reductions in Sections 6.1-6.3 are not fitted to the theory and would survive even if the theoretical proofs were rewritten. However, the advertised central property -- exact tractable inference -- is supported by Theorem 4.1(3), whose proof is circular: it equates model-theoretic entailment with the fixpoint of the rule-application operator without proving either direction beyond restating the conclusion. The same result is explicitly sourced from the authors' prior [61], making the self-citation load-bearing. Separately, there is a non-circular correctness gap: Theorem 4.2 states convergence in x = height(M)*|A|*t_max applications, but M in Section 3.1 contains all intervals/subsets of [0,1] and has infinite height under the lower-lattice order (e.g., [0,1] ⊑ [0,1/2] ⊑ [0,1/3] ⊑ ... is an infinite ascending chain), so the stated bound is not finite as written; the paper would need an explicit finite-height restriction. This does not affect the circularity score. The parameter choices in Section 6.1.1 for plotting 'theoretical bounds' are fitted to first-step data, but the formal bound of Theorem 4.4 is proven with all fractions at 1, so this is a presentational choice rather than a fabricated prediction. Overall, partial circularity in the core correctness proof warrants a score of 6.

Axiom & Free-Parameter Ledger

2 free parameters · 5 axioms · 0 invented entities

The framework inherits the full GAP semantics and its lattice-theoretic machinery from prior work, and adds temporal annotations. The main unstated axioms are the finite-height assumption on the annotation lattice (needed for Theorem 4.2) and the fixed-language assumption that is violated by the dynamic Skolemization. The RL results also depend on manually chosen reward values.

free parameters (2)
  • RL reward values = +250 win, -250 loss, +400 shoot, -200 shot, -2 valid action, -10 invalid action, -200 unsafe action
    These hand-chosen rewards drive the learned policy and the reported win-rate improvement (26% in non-Markovian vs Markovian). They are not fitted to data but are ad hoc choices that affect the central RL claim.
  • Rule confidence threshold = 0.70
    Rules from AnyBURL are filtered at minimum 70% confidence; this affects the logic programs used in KG experiments.
axioms (5)
  • standard math Kleene fixpoint theorem and lattice monotonicity
    Used to argue Γ has a least fixpoint and converges; invoked implicitly in Theorem 4.1 and 4.2.
  • domain assumption GAP semantics of Kifer and Subrahmanian (annotated literals, satisfaction, entailment)
    LAT logic builds directly on GAP definitions; Section 3 adopts them for lower lattice and temporal annotations.
  • domain assumption Lower-lattice open-world semantics from [61]
    The authors' own prior work establishes that lower-lattice annotations give open-world behavior; Theorem 4.1 correctness is inherited from there.
  • domain assumption Constant set C is fixed in the formal semantics
    Definitions 3.1-3.5 quantify over a fixed C; the Skolemization implementation adds constants dynamically, which is not covered by this axiom.
  • ad hoc to paper The annotation lattice M has finite height
    Theorem 4.2 requires a finite height(M) to bound convergence; M as defined (all subsets of [0,1]) has unbounded height.

reviewed 2026-08-05 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Lattice Annotated Temporal (LAT) Logic for Non-Markovian Reasoning." pith.science (2026). https://pith.science/paper/YPUOQG2C

@misc{pith2026250902958,
  author       = {Pith},
  title        = {Pith review of: Lattice Annotated Temporal (LAT) Logic for Non-Markovian Reasoning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YPUOQG2C}},
  note         = {Machine review of arXiv:2509.02958}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

We introduce Lattice Annotated Temporal (LAT) Logic, an extension of Generalized Annotated Logic Programs (GAPs) that incorporates temporal reasoning and supports open-world semantics through the use of a lower lattice structure. This logic combines an efficient deduction process with temporal logic programming to support non-Markovian relationships and open-world reasoning capabilities. The open-world aspect, a by-product of the use of the lower-lattice annotation structure, allows for efficient grounding through a Skolemization process, even in domains with infinite or highly diverse constants. We provide a suite of theoretical results that bound the computational complexity of the grounding process, in addition to showing that many of the results on GAPs (using an upper lattice) still hold with the lower lattice and temporal extensions (though different proof techniques are required). Our open-source implementation, PyReason, features modular design, machine-level optimizations, and direct integration with reinforcement learning environments. Empirical evaluations across multi-agent simulations and knowledge graph tasks demonstrate up to three orders of magnitude speedup and up to five orders of magnitude memory reduction while maintaining or improving task performance. Additionally, we evaluate LAT Logic's value in reinforcement learning environments as a non-Markovian simulator, achieving up to three orders of magnitude faster simulation with improved agent performance, including a 26% increase in win rate due to capturing richer temporal dependencies. These results highlight LAT Logic's potential as a unified, extensible framework for open-world temporal reasoning in dynamic and uncertain environments. Our implementation is available at: pyreason.syracuse.edu.

Figures

Figures reproduced from arXiv: 2509.02958 by Clark Dorman, Devendra Parkar, Dyuman Aditya, Gerardo I. Simari, Jaikrishna Manojkumar Patil, Kaustuv Mukherji, Lahari Pokala, Paulo Shakarian.

Figure 1
Figure 1. Figure 1: Excerpt of logic program Π𝑔𝑒𝑜 for the geospatial example shown in [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Geospatial example: Creation of new atoms during inference for two time steps (left to right). Newly created atoms at each [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Example of a lower semi-lattice structure where the elements are intervals in [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A simple logic program Π𝑠𝑖𝑚𝑝𝑙𝑒 used to illustrate the application of fixpoint operator in Example 3.7. A GAP is said to entail a TAF if it logically implies or derives the TAF from its rules and annotations under its semantic framework. Definition 3.11 (Entailment). We say GAP Π entails TAF 𝑎 : (𝜇, 𝑡), denoted Π |=ent 𝑎 : (𝜇, 𝑡), iff for every interpretation 𝐼 s.t. 𝐼 |= Π we have that 𝐼 |=𝑡 𝑎 : 𝜇. A model … view at source ↗
Figure 5
Figure 5. Figure 5: Example of a logic program Π𝑘𝑔 for the knowledge graph shown in [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Knowledge graph before (left) and after (right) inference. The newly created binary atom is shown in red. [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: (Clockwise from top-left) Comparison of #ground atoms with multiple applications of fixpoint operator ( [PITH_FULL_IMAGE:figures/full_fig_p023_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: (Clockwise from top-left) Speed-up vs Map size for [PITH_FULL_IMAGE:figures/full_fig_p024_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: (Clockwise from top-left) Memory reduction (in MB) vs Map size for [PITH_FULL_IMAGE:figures/full_fig_p025_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: (Clockwise from top-left) Comparison of number of ground atoms with multiple applications of fixpoint operator for UMLS, [PITH_FULL_IMAGE:figures/full_fig_p026_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Speed-up and Memory reduction vs Program size for 2 (top) and 5 (bottom) fixpoints on UMLS dataset. [PITH_FULL_IMAGE:figures/full_fig_p027_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Grid map for the scenario. Red (bottom-right) and Blue (top-left) squares are fixed base locations for each team. All agents [PITH_FULL_IMAGE:figures/full_fig_p029_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Runtime (left) and memory footprint (right) comparison when 1 (top), 5 (middle), 20 (bottom) agents/team take random [PITH_FULL_IMAGE:figures/full_fig_p030_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Win percentage for policies learned with Markovian and non-Markovian dynamics. [PITH_FULL_IMAGE:figures/full_fig_p033_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Graph representation of example triple to work with PyReason. [PITH_FULL_IMAGE:figures/full_fig_p041_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Graph representation of example triple after Inference. [PITH_FULL_IMAGE:figures/full_fig_p042_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Example grid for agent movement in Geospatial application. In this case, note that cell #5 has an obstacle, hence the agent is [PITH_FULL_IMAGE:figures/full_fig_p042_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: (a) Initial PyReason graph representation of grid and agent location. (b) Updated PyReason graph after two timesteps of [PITH_FULL_IMAGE:figures/full_fig_p043_18.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming

    cs.CR 2026-08 conditional novelty 7.0

    A logic-based verifier using temporal annotated logic raises the share of LLM-proposed vulnerability exploration paths that satisfy domain knowledge from 78% to 98%.

Reference graph

Works this paper leans on

69 extracted references · 55 canonical work pages · cited by 1 Pith paper · 1 internal anchor

  1. [1]

    Dyuman Aditya, Kaustuv Mukherji, Srikar Balasubramanian, Abhiraj Chaudhary, and Paulo Shakarian. 2023. PyReason: Software for Open World Temporal Logic. In AAAI Spring Symposium: MAKE

    work page 2023

  2. [2]

    Dyuman Aditya, Colton Payne, Mario Leiva, and Paulo Shakarian. 2025. Machine Learning Model Integration with Open World Temporal Logic for Process Automation. arXiv preprint arXiv:2506.17776 (2025)

    arXiv 2025

  3. [3]

    Mridul Agarwal and Vaneet Aggarwal. 2023. Reinforcement learning for joint optimization of multiple rewards. Journal of Machine Learning Research 24, 49 (2023), 1–41

    work page 2023

  4. [4]

    Kiyoshi Akama and Ekawit Nantajeewarawat. 2011. Meaning-preserving skolemization. In International Conference on Knowledge Engineering and Ontology Development, Vol. 2. SCITEPRESS, 322–327

    work page 2011

  5. [5]

    Claudi Alsina, Enric Trillas, and Llorenç Valverde. 1983. On some logical connectives for fuzzy sets theory. J. Math. Anal. Appl. 93, 1 (1983), 15–26

    work page 1983

  6. [6]

    D Bavikadi, D Aditya, D Parkar, P Shakarian, G Mueller, C Parvis, and GI Simari. 2025. Geospatial Trajectory Generation via Efficient Abduction: Deployment for Independent Testing. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE 416, 416 (2025), 274–287

    work page 2025

  7. [7]

    Divyagna Bavikadi, Nathaniel Lee, Paulo Shakarian, and Chad Parvis. [n. d.]. Sea-cret Agents: Maritime Abduction for Region Generation to Expose Dark Vessel Trajectories. ([n. d.])

    work page

  8. [8]

    Antoine Bordes, Nicolas Usunier, Alberto Garcia-Duran, Jason Weston, and Oksana Yakhnenko. 2013. Translating Embeddings for Modeling Multi-relational Data. In Advances in Neural Information Processing Systems , C.J. Burges, L. Bottou, M. Welling, Z. Ghahramani, and K.Q. Weinberger (Eds.), Vol. 26. Curran Associates, Inc. https://proceedings.neurips.cc/pap...

    work page 2013

  9. [9]

    Laura Bozzelli and David Pearce. 2015. On the Complexity of Temporal Equilibrium Logic. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. 645–656. doi:10.1109/LICS.2015.65

    work page doi:10.1109/lics.2015.65 2015

  10. [10]

    Andreas Bueff and Vaishak Belle. 2023. Deep inductive logic programming meets reinforcement learning. arXiv preprint arXiv:2308.16210 (2023)

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  11. [11]

    Andreas Burgdorf, Alexander Paulus, André Pomp, and Tobias Meisen. 2022. DocSemMap: Leveraging Textual Data Documentations for Mapping Structured Data Sets into Knowledge Graphs. In 2022 IEEE 16th International Conference on Semantic Computing (ICSC) . 209–216. doi:10.1109/ ICSC52841.2022.00042

    work page arXiv 2022

  12. [12]

    Pedro Cabalar and Gilberto Pérez Vega. 2007. Temporal Equilibrium Logic: A First Approach. In Computer Aided Systems Theory – EUROCAST 2007 , Roberto Moreno Díaz, Franz Pichler, and Alexis Quesada Arencibia (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 241–248

    work page 2007

  13. [13]

    Stefano Ceri, Georg Gottlob, Letizia Tanca, et al. 1989. What you always wanted to know about Datalog(and never dared to ask). IEEE transactions on knowledge and data engineering 1, 1 (1989), 146–166

    work page 1989

  14. [14]

    Siddharth Chandak, Pratik Shah, Vivek S Borkar, and Parth Dodhia. 2024. Reinforcement learning in non-Markovian environments. Systems & Control Letters 185 (2024), 105751

    work page 2024

  15. [15]

    Y Choi, Antonio Vergari, and Guy Van den Broeck. 2020. Probabilistic circuits: A unifying framework for tractable probabilistic models. UCLA. URL: http://starai. cs. ucla. edu/papers/ProbCirc20. pdf (2020), 6

    work page 2020

  16. [16]

    Edmund M Clarke, E Allen Emerson, and A Prasad Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8, 2 (1986), 244–263

    work page 1986

  17. [17]

    Purushothaman Iyer, and Murali Narasimha

    Rance Cleaveland, S. Purushothaman Iyer, and Murali Narasimha. 2005. Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science 342, 2 (2005), 316–350. doi:10.1016/j.tcs.2005.03.048

    doi:10.1016/j.tcs.2005.03.048 2005

  18. [18]

    Peter D Clive, Jeffrey A Johnson, Michael J Moss, James M Zeh, Brian M Birkmire, and Douglas D Hodson. 2015. Advanced framework for simulation, integration and modeling (AFSIM)(Case Number: 88ABW-2015-2258). In Proceedings of the international conference on scientific computing (CSC) . The Steering Committee of The World Congress in Computer Science, Comp...

    work page 2015

  19. [19]

    Alain Colmerauer. 1982. Prolog and infinite trees. Logic Programming 16, 231-251 (1982), 2

    work page 1982

  20. [20]

    Maxwell John Cresswell and George Edward Hughes. 2012. A new introduction to modal logic . Routledge

    work page 2012

  21. [21]

    Andrew Cropper, Sebastijan Dumančić, and Stephen H Muggleton. 2020. Turning 30: New ideas in inductive logic programming. arXiv preprint arXiv:2002.11002 (2020)

    Pith/arXiv arXiv 2020

  22. [22]

    Wang-Zhou Dai, Qiuling Xu, Yang Yu, and Zhi-Hua Zhou. 2019. Bridging machine learning and logical reasoning by abductive learning. Advances in Neural Information Processing Systems 32 (2019)

    work page 2019

  23. [23]

    Alex Dekhtyar, Michael I Dekhtyar, and VS Subrahmanian. 1999. Temporal Probabilistic Logic Programs.. In ICLP, Vol. 99. 109–123. Manuscript submitted to ACM LAT Logic for Non-Markovian Reasoning 37

    work page 1999

  24. [24]

    Dekhtyar, and V

    Alex Dekhtyar, Michael I. Dekhtyar, and V. S. Subrahmanian. 1999. Temporal Probabilistic Logic Programs. InInternational Conference on Logic Programming. 109–123

    work page 1999

  25. [25]

    Martin Diller, Adam Wyner, and Hannes Strass. 2019. Making Sense of Conflicting (Defeasible) Rules in the Controlled Natural Language ACE: Design of a System with Support for Existential Quantification Using Skolemization. In Proceedings of the 13th International Conference on Computational Semantics - Short Papers, Simon Dobnik, Stergios Chatzikyriakidis...

    doi:10.18653/v1/w19-0505 2019

  26. [26]

    Dragan Doder and Zoran Ognjanović. 2024. Probabilistic temporal logic with countably additive semantics. Annals of Pure and Applied Logic 175, 9 (2024), 103389

    work page 2024

  27. [27]

    Esra Erdem, Michael Gelfond, and Nicola Leone. 2016. Applications of answer set programming. Ai Magazine 37, 3 (2016), 53–68

    work page 2016

  28. [28]

    Richard Evans and Edward Grefenstette. 2018. Learning Explanatory Rules from Noisy Data. J. Artif. Int. Res. 61, 1 (jan 2018), 1–64

    work page 2018

  29. [30]

    Maor Gaon and Ronen Brafman. 2020. Reinforcement learning with non-markovian rewards. In Proceedings of the AAAI conference on artificial intelligence, Vol. 34. 3980–3987

    work page 2020

  30. [31]

    Matt Ginsberg. 2012. Essentials of Artificial Intelligence. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA

    work page 2012

  31. [32]

    M Gelfond GL881 and V Lifschitz. 1988. The stable model semantics for logic programming. In Proc. 5’h International Conference and Symposium on Logic Programming. 1070–1080

    work page 1988

  32. [33]

    Gaurav Gupta, Chenzhong Yin, Jyotirmoy V Deshmukh, and Paul Bogdan. 2021. Non-markovian reinforcement learning using fractional dynamics. In 2021 60th IEEE Conference on Decision and Control (CDC) . IEEE, 1542–1547

    work page 2021

  33. [34]

    Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal aspects of computing 6, 5 (1994), 512–535

    work page 1994

  34. [35]

    Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. 2016. Deep residual learning for image recognition. In Proceedings of the IEEE conference on computer vision and pattern recognition . 770–778

    2016

  35. [36]

    Patrick Hohenecker and Thomas Lukasiewicz. 2020. Ontology reasoning with deep neural networks. In Journal of Artificial Intelligence Research , Vol. 68. 503–540

    work page 2020

  36. [37]

    Ulrich Höhle. 1978. Probabilistic uniformization of fuzzy topologies. Fuzzy Sets and Systems (1978)

    work page 1978

  37. [38]

    Subrahmanian

    Michael Kifer and V.S. Subrahmanian. 1992. Theory of Generalized Annotated Logic Programming and its Applications. J. Log. Program. 12, 3&4 (1992), 335–367

    work page 1992

  38. [39]

    Kowalski

    Robert A. Kowalski. 1988. The early years of logic programming. Commun. ACM 31, 1 (Jan. 1988), 38–43. doi:10.1145/35043.35046

    arXiv 1988

  39. [40]

    Lattner and V

    C. Lattner and V. Adve. 2004. LLVM: a compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, 2004. CGO 2004. 75–86. doi:10.1109/CGO.2004.1281665

    Pith/arXiv arXiv 2004

  40. [41]

    Mario Leiva, Noel Ngu, Joshua Shay Kricheli, Aditya Taparia, Ransalu Senanayake, Paulo Shakarian, Nathaniel Bastian, John Corcoran, and Gerardo Simari. 2025. Consistency-based Abductive Reasoning over Perceptual Errors of Multiple Pre-trained Models in Novel Environments. arXiv preprint arXiv:2505.19361 (2025)

    arXiv 2025

  41. [42]

    D Loveland. 1978. Automated Theorem Proving: A Logical Basis North Holland. New York (1978), N75

    work page 1978

  42. [43]

    Victor W Marek and Miroslaw Truszczyński. [n. d.]. Stable models and an alternative logic programming paradigm. In The logic programming paradigm: A 25-year perspective . Springer, 375–398

    work page

  43. [44]

    Joao Marques-Silva. 2024. Logic-based explainability: past, present and future. In International Symposium on Leveraging Applications of Formal Methods. Springer, 181–204

    work page 2024

  44. [45]

    Karsten Martiny and Ralf Möller. 2016. PDT logic: a probabilistic doxastic temporal logic for reasoning about beliefs in multi-agent systems. Journal of Artificial Intelligence Research 57 (2016), 39–112

    work page 2016

  45. [46]

    Bridget T McInnes, Ted Pedersen, and Serguei VS Pakhomov. 2009. UMLS-Interface and UMLS-Similarity: open source software for measuring paths and semantic similarity. In AMIA annual symposium proceedings , Vol. 2009. American Medical Informatics Association, 431

    work page 2009

  46. [47]

    Christian Meilicke, Melisachew Wudage Chekol, Patrick Betz, Manuel Fink, and Heiner Stuckeschmidt. 2024. Anytime bottom-up rule learning for large-scale knowledge graph completion. The VLDB Journal 33, 1 (2024), 131–161

    work page 2024

  47. [48]

    Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A Rusu, Joel Veness, Marc G Bellemare, Alex Graves, Martin Riedmiller, Andreas K Fidjeland, Georg Ostrovski, et al. 2015. Human-level control through deep reinforcement learning. nature 518, 7540 (2015), 529–533

    work page 2015

  48. [49]

    Charles G Morgan. 1974. Symbolic Logic and Mechanical Theorem Proving (Chin-Liang Chang and Richard Char-Tung Lee). SIAM Rev. 16, 3 (1974), 403–407

    work page 1974

  49. [50]

    Kaustuv Mukherji, Devendra Parkar, Lahari Pokala, Dyuman Aditya, Paulo Shakarian, and Clark Dorman. 2024. Scalable Semantic Non-Markovian Simulation Proxy for Reinforcement Learning. In 2024 IEEE 18th International Conference on Semantic Computing (ICSC) . IEEE, 183–190

    work page 2024

  50. [51]

    Ilkka Niemelä. 1999. Logic Programs with Stable Model Semantics as a Constraint Programming Paradigm. Ann. Math. Artif. Intell. 25 (11 1999), 241–273. doi:10.1023/A:1018930122475

    work page doi:10.1023/a:1018930122475 1999

  51. [52]

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. [n. d.]. Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. In The 2023 Conference on Empirical Methods in Natural Language Processing

    work page 2023

  52. [53]

    Jaikrishna Manojkumar Patil, Adam Chapman, Richard Knuszka, John Chapman, and Paulo Shakarian. 2025. Reasoning about Medical Triage Optimization with Logic Programming. arXiv preprint arXiv:2507.10781 (2025). Manuscript submitted to ACM 38 K. Mukherji et al

    arXiv 2025

  53. [54]

    David Pearce. 2006. Equilibrium logic. Annals of Mathematics and Artificial Intelligence 47, 1–2 (June 2006), 3–41. doi:10.1007/s10472-006-9028-z

    doi:10.1007/s10472-006-9028-z 2006

  54. [55]

    Amir Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) . 46–57. doi:10.1109/ SFCS.1977.32

    work page 1977

  55. [56]

    Ryan Riegel, Alexander Gray, Francois Luus, Naweed Khan, Ndivhuwo Makondo, Ismail Yunus Akhalwaya, Haifeng Qian, Ronald Fagin, Francisco Barahona, Udit Sharma, Shajith Ikbal, Hima Karanam, Sumit Neelam, Ankita Likhyani, and Santosh Srivastava. 2020. Logical Neural Networks

    work page 2020

  56. [57]

    Jürgen Schmidhuber. 1990. Reinforcement learning in Markovian and non-Markovian environments. Advances in neural information processing systems 3 (1990)

    work page 1990

  57. [58]

    Lenhart Schubert. 1999. Dynamic Skolemization. In Computing Meaning: Volume 1. Springer, 219–253

    work page 1999

  58. [59]

    Prithviraj Sen, Breno W. S. R. de Carvalho, Ryan Riegel, and Alexander Gray. 2022. Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks. AAAI conference on Artificial Intelligence 8 (2022)

    work page 2022

  59. [60]

    Simari, and Venkatramana V

    Paulo Shakarian, Austin Parker, Gerardo I. Simari, and Venkatramana V. S. Subrahmanian. 2011. Annotated probabilistic temporal logic. ACM Trans. Comput. Logic 12, 2, Article 14 (jan 2011), 44 pages. doi:10.1145/1877714.1877720

    arXiv 2011

  60. [61]

    Paulo Shakarian and Gerardo I Simari. 2022. Extensions to Generalized Annotated Logic and an Equivalent Neural Architecture. In 2022 Fourth International Conference on Transdisciplinary AI (TransAI) . IEEE, 63–70

    work page 2022

  61. [62]

    Simari, and Robert Schroeder

    Paulo Shakarian, Gerardo I. Simari, and Robert Schroeder. 2013. MANCaLog: a logic for multi-attribute network cascades. In International conference on Autonomous Agents and Multi-Agent Systems, AAMAS . 1175–1176

    work page 2013

  62. [63]

    Paulo Shakarian, Gerardo I Simari, and VS Subrahmanian. 2012. Annotated probabilistic temporal logic: Approximate fixpoint implementation. ACM Transactions on Computational Logic (TOCL) 13, 2 (2012), 1–33

    work page 2012

  63. [64]

    Hikaru Shindo, Masaaki Nishino, and Akihiro Yamamoto. 2021. Differentiable Inductive Logic Programming for Structured Examples. In AAAI Conference on Artificial Intelligence. 5034–5041

    work page 2021

  64. [65]

    Suchanek, Gjergji Kasneci, and Gerhard Weikum

    Fabian M. Suchanek, Gjergji Kasneci, and Gerhard Weikum. 2007. Yago: a core of semantic knowledge. In Proceedings of the 16th International Conference on World Wide Web (Banff, Alberta, Canada) (WWW ’07) . Association for Computing Machinery, New York, NY, USA, 697–706. doi:10.1145/1242572.1242667

    arXiv 2007

  65. [67]

    Alexandros Vassiliades, Spyridon Symeonidis, Sotiris Diplaris, Georgios Tzanetis, Stefanos Vrochidis, Nick Bassiliades, and Ioannis Kompatsiaris

    work page

  66. [68]

    A Vaswani. 2017. Attention is all you need. Advances in Neural Information Processing Systems (2017)

    2017

  67. [69]

    Oriol Vinyals, Timo Ewalds, Sergey Bartunov, Petko Georgiev, Alexander Sasha Vezhnevets, Michelle Yeo, Alireza Makhzani, Heinrich Küttler, John Agapiou, Julian Schrittwieser, et al. 2017. Starcraft ii: A new challenge for reinforcement learning. arXiv preprint arXiv:1708.04782 (2017)

    Pith/arXiv arXiv 2017

  68. [70]

    Peter Vojtáš. 2001. Fuzzy logic programming. Fuzzy sets and systems 124, 3 (2001), 361–370. A Complete Proof for Theorem 4.4 Proof. Let𝑃Π⊆ 𝑃 be the set of predicates containing only predicates present in the head of at least one rule in ΠRules. |𝑔𝑖| = | Ø 𝑝∈𝑃 𝑔𝑖(𝑝)| = ∑︁ 𝑝∈𝑃 |𝑔𝑖(𝑝)| = ∑︁ 𝑝∈𝑃Π |𝑔𝑖(𝑝)|+ ∑︁ 𝑝∉𝑃Π |𝑔𝑖(𝑝)| = ∑︁ 𝑝∈𝑃Π |𝑔𝑖(𝑝)|+ ∑︁ 𝑝∉𝑃Π |𝑔0(𝑝)| (12...

    work page 2001

  69. [2023]

    In 2023 IEEE 17th International Conference on Semantic Computing (ICSC)

    XR4DRAMA Knowledge Graph: A Knowledge Graph for Disaster Management. In 2023 IEEE 17th International Conference on Semantic Computing (ICSC). 262–265. doi:10.1109/ICSC56153.2023.00051

    work page arXiv 2023

This paper was first reviewed by deepseek-v4-flash on August 5, 2026.