Abstract Logica is an open-source logic programming language that compiles to SQL and runs on platforms including DuckDB, SQLite, PostgreSQL, and BigQuery. Unlike classic Datalog, Logica permits the free combination of recursion and aggregation, enabling concise formulations of algorithms from shortest paths to PageRank. This expressiveness introduces fundamental semantic challenges: aggregate predicates are updated by replacement rather than accumulation, evaluation is sensitive to rule scheduling, and programs may converge to meaningful results without ever reaching a fixpoint, placing them outside the scope of traditional fixpoint semantics. We address these challenges with Defendant-Opponent (DO) semantics , a stabilization-based framework for nonmonotonic logic programs. Program evaluation is modeled as a rewrite system over derivation states. A ground atom is true if, from every reachable state, there exists a continuation after which the atom persists in all further derivations. This notion admits two equivalent characterizations: (1) game-theoretically, truth is what a Defendant can defend against any Opponent in a three-turn derivation game; and (2) modally, a formula t t $t$ is a theorem precisely when the condition white medium square lozenge white medium square t ◻ ◊ ◻ t $\Box \mkern 1.33mu{\LARGE \Diamond }\Box \mkern 1.33mu\,t$ holds in the derivation graph viewed as a Kripke structure. We show that DO semantics coincides with classic least fixpoint semantics for positive Datalog programs and is compatible with both the Well-Founded Semantics (the two never disagree on definite answers) and the Stable Model Semantics (every stable model is a DO interpretation). For programs that converge without reaching a fixpoint, we introduce omega ω $\omega$ -limit interpretations, giving rigorous meaning to iterative computations such as PageRank. DO semantics thus offers a coherent framework that complements existing logic programming semantics while supporting recursive aggregation.
Abstract Metric temporal equilibrium logic ( MEL MEL $\textrm {MEL}$ ) extends temporal equilibrium logic ( TEL TEL $\textrm {TEL}$ ) by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. MEL MEL $\textrm {MEL}$ is particularly suited for domains where time-bound properties are crucial, such as embedded systems, cyber-physical systems, and real-time software. It facilitates the precise expression of timing behaviors, such as the requirement that an event must occur within 5 milliseconds of a trigger, which often elude traditional qualitative temporal logics. In this paper, we present a Tseitin-like translation that maps any metric temporal formula into a logic programming fragment restricted to past operators. This translation provides a formal bridge to leverage existing answer set programming (ASP) solvers for reasoning about metric temporal constraints. By restricting the target fragment to past operators, we enable more effective evaluation and integration with current ASP-based toolchains for multi-shot solving.
In the field of static analysis of logic programs, the optimality of abstract operators is a valuable theoretical property, as it provides insight into the structure of abstract domains and the maximum precision that can be achieved. However, implementing optimal operators is often complex and may significantly impact performance, giving rise to a trade-off between precision and efficiency. We experimentally investigate this trade-off in the context of sharing and linearity analysis of logic programs. Our experiments build on previous work that proposed several optimal operators for unification and matching. We have implemented these abstract operators and the corresponding abstract domains within the PLAI analyzer, part of the CiaoPP preprocessor, and we report the impact of increasing operator precision on the accuracy and performance of the overall analysis.
