arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.32805

Choosing What to Observe: Higher-Order Obstructions in Horn Abduction

Yukun Yang
View original source ↗Read source document ↗Export metadata ↓

Abstract

An explanation may exist in every complete context yet be impossible to select from the information observed. We study this distinction in finite propositional Horn abduction with integrity constraints. Observations are sufficient when each report admits one hypothesis set that is consistent and entails the manifestation in every compatible context. We characterize sufficiency by minimal context families with no common explanation. Their variable spans form a canonical hypergraph whose transversals are exactly the sufficient observation sets. The characterization recovers classical discernibility for unique explanations and supports composition across independent components. Minimal obstructions have unbounded cardinality even for acyclic rules, while rectangular explanation families admit a tight bound given by their largest choice domain. With circuit-defined contexts, sufficiency is $Π_3^P$-complete and selecting at most $k$ observable variables is $Σ_4^P$-complete, already for unrestricted contexts and acyclic rules. The selection reduction makes observation choices enforce globally fixed existential commitments. Explicit contexts reduce both tasks to NP-complete problems; tabulated explanation families make sufficiency polynomial. These results connect explanatory choice, information requirements, and representation cost.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yukun Yang. 2026-10-23. Choosing What to Observe: Higher-Order Obstructions in Horn Abduction. https://arxiv.org/abs/2610.32805

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Non-Expansive Fuzzy Modal Logic Has Uniform Interpolation

Fuzzy logics with truth values in the unit interval vary in their choice of propositional connectives and their semantics, ranging from just minimum and maximum as in Zadeh logics to truncated addition and subtraction as in Łukasiewicz logics or their extensions with truth constants, known as Pavelka logics. In the more specific world of fuzzy modal logics, non-expansive fuzzy modal logic has recently been proposed as a sweet spot between Łukasiewicz (more precisely, Pavelka) and Zadeh fuzzy modal logic; it restricts Łukasiewicz propositional connectives to have one argument constant, equivalently extends the Zadeh propositional base with constant shift operators. It retains reasonable expressiveness both in practical terms and abstractly; in particular, it characterizes the standard notion of behavioural distance on fuzzy Kripke frames. At the same time, it allows for satisfiability checking in the same complexity as for its two-valued correspondent (the modal logic K, or the description logic ALC), in contrast to the notorious computational hardness of Łukasiewicz modal logic. In the present work, we show that non-expansive fuzzy modal logic admits uniform interpolation, a key property in modularization, information hiding, summarization, and other applications that fails for both Łukasiewicz (or Pavelka) and Zadeh modal logic.

cs.LO↗
arXiv2026

Extracting total Amb programs from proofs

We present a logical system CFP (Concurrent Fixed Point Logic) supporting the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators: Restriction (binary), a strengthening of implication, and a unary operator for total concurrency. The source of the extraction is formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of CFP is the fact that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb. This is a revised and extended version of the conference paper presented at ESOP 2022 with the same title that contains full proofs of all major results.

cs.LO↗
arXiv2026

A declarative approach to specifying Paxos using three-valued modal fixpoint logic

We present Three-valued Fixpoint Quorum Logic, or 3muQL for short; a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. 3muQL adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing and state-transitions are not explicitly modelled, and notions of 'quorum' are abstracted from concrete thresholds to abstract modal operators. This distinguishes our framework from approaches like TLA+. The logical abstraction emphasises the essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of 3muQL, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision 3muQL as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. The ideas we present are easily implemented, and to demonstrate this we have implemented a freely-available proof-of- concept 3muQL model-checker, as an effective prototyping tool.

cs.LO↗