Dynamic agent harnesses let language models change the software that shapes their own execution. This flexibility brings a new reasoning burden: a local plugin change can propagate through dependencies and cleanup. We introduce CordisBench, a 1,200-question benchmark of this lifecycle reasoning. It combines a controlled formal setting with programs executed against Cordis, a runtime that manages component dependencies and cleanup, and asks models to identify affected components, predict state after a specified teardown order, determine which conditions hold under all or some orders, and choose reconfigurations that succeed when executed. Across these tasks, we evaluate three efficiency-oriented models at low reasoning effort with 2, 4, 8, 16, 24, or 32 relevant interactions, using deterministic task-specific scoring. Models usually handle small systems well but grow less reliable as more interactions become relevant, especially when predicting final state and when reasoning across teardown orders. Additional inference effort recovers marked gains for some models. The cost is nontrivial: on our 16-interaction subset, GPT-5.6 Luna uses nearly 3,000 reasoning tokens per question at medium effort. For these controlled instances, that cost is avoidable: an independent finite reference semantics agrees with Cordis execution on every observation and action outcome used for scoring across all 528 executable questions.
Evidential argumentation extends Dung's abstract argumentation by requiring arguments and interactions to be backed by chains of evidence rooted in prima-facie elements. However, existing formalisms lack a unified treatment of evidential support, higher-order relations (attacks and supports targeting arbitrary elements), and collective interactions (sources as sets). In this paper, we introduce the Evidential-Based Higher-Order Set Argumentation Framework (EHSAF), which conservatively generalises several existing frameworks within a single expressive setting. We develop two complete semantics for EHSAFs: an \emph{adjacent complete labelling semantics} that admits multiple truth values (true, false, undecided) for arguments in support cycles, reflecting an open epistemic attitude toward future evidence; and an \emph{extension-based complete semantics} that follows a strict evidentialist stance, accepting only arguments with well-founded support chains. We show that these two semantics diverge in the presence of support cycles, and prove their equivalence under support-acyclicity. To enable computational reasoning, we provide a normal propositional encoding of EHSAFs and prove that, in three-valued Łukasiewicz logic, its models correspond precisely to the adjacent complete labellings. We further extend this encoding to continuous fuzzy logics (G{ö}del, Product, and Łukasiewicz), defining a continuous fuzzy normal encoded semantics. We establish that this fuzzy semantics satisfies key properties---continuity, monotonicity, boundary conditions, and solution existence---and that its ternarisation recovers the adjacent complete labellings under natural t-norm conditions. Our framework thus unifies expressive argumentation with principled three-valued and fuzzy semantics, bridging the gap between qualitative and quantitative reasoning about evidence.
This work introduces a formal semantic-block model for specifications and an execution-judged benchmark for evaluating specification quality independently of model capability. A specification is represented as a structure comprising semantic blocks, dependency relations, block-owned rules, decision points, and explicitly open questions, subject to four machine-checkable well-formedness conditions: acyclicity, single ownership, constraint domination, and totality or ambiguity-stop. Determinacy is defined model-theoretically as agreement among all conforming implementations and is estimated empirically through convergence across independent implementers. The model is instantiated on an Oracle-to-PostgreSQL migration specification containing 18 blocks and 19 dependency edges. Computational validation shows that the five-layer decomposition reduces mean per-task context by approximately 71% through dependency closures, covers 85.5% of the study-defined Oracle construct taxonomy with all identified gaps triaged, is not Pareto-dominated by the tested alternative partitions, and is recovered at the 99.9th percentile from citation-derived edges not used to define the original structure. The benchmark keeps the implementer panel fixed, includes a mandatory no-specification control arm, and uses PostgreSQL 16 and a live Oracle instance as deterministic execution judges. Six designed studies, including three pre-registered manipulations and three diagnostic analyses, further examine specification effects. Repeated runs on a 25-unit subsample reveal an empirical variability floor with a median arm-delta spread of 14.4 percentage points. The results support determinacy as a formal concept but not as a standalone empirical quality metric for the evaluated contemporary LLM implementers.
Intensional operators are often treated as quantifiers over possible worlds, parallel to the treatment of determiners as quantifiers over individuals. Yet individuals introduced in intensional contexts cannot serve as antecedents to later pronouns as easily as those introduced in merely quantificational contexts. For instance, "Everyone is eating a cheeseburger" may be followed by "They are large", where "they" refers to the cheeseburgers being eaten. However, as Stone (1999) points out, the similar "Andrea might be eating a cheeseburger" does not support later anaphoric references such as "It is large" or "They are large". Stone (1999), Stone and Hardt (1999), and Brasoveanu (2010) address this by requiring a pronoun's value (its referents) to exist in the world of evaluation, ruling out anaphora from non-veridical intensional contexts. We show, however, both cases where such anaphora is disallowed even when the pronoun's referents clearly exist and cases where it is allowed even though they might not exist. We argue that intensional anaphora is best captured using a description-based rather than value-based account. A pronoun presupposes that its corresponding antecedent description is instantiated in each world of the context set. Thus, there must be a cheeseburger being eaten by Andrea in every candidate world for "It is large" to be felicitous after "Andrea might be eating a cheeseburger". We implement our proposal via a new logic, building on Keshet (2018) and Abney and Keshet (2022), called Plural Intensional Presuppositional predicate calculus (PIP). Each PIP formula translates directly into standard first-order predicate calculus with set abstraction, providing a classical foundation for this work.
Jaime Osvaldo Salas, Paolo Pareti, Adeel Aslam +2cs.AI
The ODRL policy language is emerging as the de-facto standard for policy modelling data access and usage preferences, AI governance policies and data workflows in European dataspaces. The current standard has no mathematical formal semantics to describe how a system should implement policy evaluation. This has resulted in a variety of systems and tools that implement their own interpretation of the language, which limits interoperability and cannot guarantee consistent results. Based on an existing semantic model of ODRL, we formalise the problems of ODRL evaluation for the access control and monitoring scenarios, in both static and streaming settings, and we provide a novel, efficient algorithm and implementation. We present the first ODRL Evaluator with transparent formal semantics and supporting all rule types. We experimentally measure its performance, analysing different scalability dimensions related to policy complexity and size of the data on which a policy is evaluated. We compare our system with the state-of-the-art by providing a comparative review of existing ODRL evaluators, which highlights the differences in supported ODRL features and evaluation modes.
An AI system's output is not the fact or world state it appears to describe, but rather an engineered representation. We propose a semantic framework to describe AI systems, to be able to examine the correctness of such representations. To do so, we distinguish what is justified by accepted domain knowledge, what reference sources say, and what the system can currently use. This allows us to give precise definitions to common failures: extrapolation, refuted or unsupported assertion, sources versus knowledge mismatch, stale or refuted source, added hypotheses, unsupported use... We hope our framework gives a useful vocabulary for specifying and checking AI systems whose outputs, citations, tool calls, and world-changing actions must be justified by reliable claims and explicit authority rather than apparent fluency.
Munindar P. Singh, Samuel H. Christie, Amit K. Chopracs.PL cs.AI cs.MA
Current languages for specifying multiagent protocols either over-constrain protocol enactments or complicate capturing their meanings. We propose Langshaw, a declarative protocol language based on (1) sayso, a new construct that captures who has priority over setting each attribute, and (2) nono and nogo, two constructs to capture conflicts between actions. Langshaw combines flexibility with an information model to express meaning. We give a formal semantics for Langshaw, procedures for determining the safety and liveness of a protocol, and a method to generate a message-oriented protocol (embedding needed coordination) suitable for flexible asynchronous enactment.
Daham M. Mustafa, Christoph Lange, Giancarlo Guizzardi +3cs.LO cs.AI
ODRL policy evaluators produce verdicts, but say nothing about the normative positions a policy brings into existence, the authority structures those positions presuppose, or who holds the power to declare a norm violated. We formulate the Cross-Level Design Principle: any normative language with violable, consequential norms requires both conduct-level positions (Permission, Duty, Right, No right) and competence-level positions (Power, Subjection, Immunity, Disability). Applying this to ODRL, we establish that prohibition is sanctioned (violation possible and consequential), that permission is underspecified across its behaviour parameter (open vs. closed world), and that the formal semantics covers achievement obligations only. We ground ODRL in UFO-L, mapping each activated rule to a simple legal relator and extending coverage from two to eight legal positions; violation-declaration authority, implicit in every existing evaluator, becomes an explicit Power-Subjection pair. All axioms are mechanically verified in Isabelle/HOL and across a 39-problem benchmark under Vampire, E, and Z3.
In this paper, we explore the concept of modularity in first-order answer set programming (ASP). We introduce a new formalism called parametric modular logic programs, which allows defining subprograms with parameters and intensionality statements. We demonstrate how this formalism can capture the semantics of clingo-programs with collective control, a feature that enables structuring and instantiating subprograms. We provide theoretical foundations for modular ASP, illustrate its usefulness, and connect to traditional non-modular ASP.
Matti Berthold, Lydia Blümel, Giovanni Buraglio +1cs.AI cs.LO
This work proposes novel splitting techniques for argumentation formalisms that incorporate supports between defeasible elements. We base our studies on bipolar set-based argumentation frameworks (BSAFs) which generalize argumentation frameworks with collective attacks (SETAFs), as well as bipolar argumentation frameworks (BAFs), by incorporating both collective attacks and supports. Notably, BSAFs establish a crucial link to structured argumentation as they naturally capture general (potentially non-flat) assumption-based argumentation. The increase in expressiveness calls for diverse forms of splitting. We consider splits over collective attacks (thereby generalizing the recently proposed splitting techniques for SETAFs), splits over collective supports, as well as splits over both collective attacks and supports. We establish suitable splitting schemata and prove their correctness for the most common argumentation semantics.