SAT Modulo Well-Founded Semantics

A New Well-Supported Semantics for Description Logic Programs

Description logic programs are a powerful formalism for combining rules with ontologies. The well-supported semantics for description logic programs ensures that no answer sets rely on cyclic dependencies. Most popular semantics for logic programming have this property of well-supportedness. We recognize two limitations of the current well-supported semantics for DL programs: its increased computational complexity for the consistency problem and its lack of a reduct transformation characterization. In this work, we present a new semantics which evaluates ontological atoms more strictly than the current semantics. This keeps the complexity of its consistency problem NP-complete, rather than increasing it to the second level of the polynomial hierarchy. Additionally, we identify a syntactic class of description logic programs for which our new semantics is equivalent to the current semantics. We characterize our semantics using a fixpoint operator and a reduct-based transformation. Our new semantics is a strict subset of the current well-supported semantics, so it maintains the prior notion of well-supportedness while inducing its own stricter notion. We prefer our new notion of well-supportedness due to its similarities with logic programming.

Cover Semantics for Intuitionistic Modalities

Intuitionistic modal logic (IML) has inspired several developments in programming languages including modal type systems for staging, computational effects and language-based security. IMLs are typically studied using Kripke-style relational semantics, which simplifies proofs of meta-theoretic properties, such as completeness and consistency, by making it easy to construct models. Kripke-style relational semantics, however, relies upon classical reasoning principles, which makes it unappealing from a computational perspective and unsuitable for formalization in a constructive type theory. Goldblatt provides an alternative semantics for IMLs by extending Beth-Kripke-Joyal-style"cover"semantics for intuitionistic propositional logic with relations to support modalities. Goldblatt's"relational cover"semantics overcomes classical reasoning but introduces a new limitation: it relies upon a"modal localization"condition that restricts the class of models and complicates model construction. Goldblatt bypasses this restriction by using intricate order-theoretic completion arguments to prove completeness. In this article, we present a conservative extension of relational cover semantics that alleviates this restriction and is amenable to simpler and standard model construction techniques. We formalize our semantics in Agda and prove completeness constructively in the style of Normalization by Evaluation for a variety of IMLs featuring independent box and diamond modalities.

QBF Reasoning for Concept Satisfiability via an Optimised Reduction From K

Bound-Founded Semantics for Answer Set Programming with Difference Constraints: Preliminary Report

While the integration of linear constraints has significantly expanded the reach of Answer Set Programming (ASP), existing hybrid solvers often rely on disparate semantic underpinnings that lack a unified logical foundation. We address this gap by introducing a many-sorted variant of the Bound-founded Logic of Here-and-There (HTb), providing a versatile framework capable of characterizing equilibrium models across a wide spectrum of alternative semantics for extensions of ASP with linear constraints. We apply this framework to the setting of difference constraints, focusing on the semantic characterization of clingo[DL]. Central to our approach is the formalization of foundedness for numeric variables. By investigating how different hybrid systems - such as clingo[DL], clingcon, and flingo - justify constraint atoms, we uncover the semantic roots of their varying behaviors. This investigation results in a single, consistent framework that not only formalizes the foundations of current systems like clingo[DL] but also facilitates the rigorous study of program simplifications and the future integration of diverse semantic principles.

Refining Gelfond’s Rationality Principle: Towards More Comprehensive Foundational Principles for Answer Set Semantics

Non-monotonic logic programming is the basis for a declarative problem solving paradigm known as answer set programming (ASP), where solutions to problems are encoded by intended models (answer sets) of a logic program. Departing from the seminal definition by Gelfond and Lifschitz [45] for simple normal logic programs, various answer set semantics have been proposed for extensions such as disjunctive logic programs and epistemic logic programs. In the latter case, the semantics consists of sets of answer sets called world views. In general, it seems infeasible to formally prove whether a proposal defines answer sets/world views that correspond exactly to the solutions of any problem intuitively represented by a logic program. It is thus necessary to develop some general principles and use them as a baseline to intuitively compare and assess different answer set and world view semantics, respectively. Towards such a baseline, we consider two important questions: (1) Should the minimal model property, constraint monotonicity and foundedness as defined in the literature be mandatory conditions for an answer set semantics in general? (2) If not, what other properties could be considered as alternative principles for answer set semantics? We address the two questions with several contributions. First, we use examples to demonstrate that requiring minimal models, constraint monotonicity and foundedness as mandatory conditions may exclude expected answer sets for some simple disjunctive programs and world views for some epistemic specifications. Second, we evolve the Gelfond answer set (GAS) principles [42] for answer set construction by refining the Gelfond's rationality principle to well-supportedness, minimality w.r.t. negation by default, and minimality w.r.t. epistemic negation. The principle of well-supportedness guarantees that every answer set is constructible from if-then rules obeying a level mapping and is thus free of circular justification, while the two minimality principles ensure that the formalism minimizes knowledge both at the level of answer sets and of world views. We thus propose to consider the three refined GAS principles as alternative principles for answer set semantics in general and for answer set and world view construction in particular. Third, to embody the refined GAS principles, we extend the notion of well-supportedness substantially to answer sets and world views, respectively. Fourth, we propose to define answer set semantics in terms of the refined GAS principles, called rational answer set and rational world view semantics, respectively. Fifth, we use the refined GAS principles as an alternative baseline to intuitively assess the existing answer set semantics whether they satisfy (are compliant with) or even fully embody the refined GAS principles. Finally, we analyze the computational complexity of well-supportedness and the rational answer set and world view semantics, revealing them as expressive hosts for problem solving.

Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?

Reasoning about necessity and possibility depends on assumptions about accessibility between worlds and about which objects exist at each one. The same inference may therefore hold under one modal system and fail under another. Evaluating language models on such problems requires testing whether their judgments follow the stated semantics rather than a familiar logic. We construct paired modal problems with identical premises and conjecture but different frame or domain conditions; automated reasoning verifies opposite labels. A balanced core prevents the semantic condition alone from revealing the answer. On this core, four of five recent models perform below the condition-only baseline under direct prompting. Yet enabling reasoning mode raises DeepSeek V4 Flash from 4.4% to 88.1% on unchanged prompts. Following stipulated modal semantics thus depends strongly on inference mode as well as model identity. When frame conditions are omitted, models often agree but fit different familiar logics best. We release the formulas, oracle artifacts, countermodels, and responses.