Reject underivable queries in incremental ABA skeptical preferred

[ctoth]

Fixes #72: the incremental ASP route for skeptical preferred ABA acceptance accepted literals that nothing can derive.

Root cause

In an assumption-free framework with no rule for q, supported(q) is never grounded. AbaIncrementalSolver.is_skeptically_accepted_preferred still passed it to clingo as a false assumption when searching for a counterexample. Clingo reports UNSAT for an assumption on an absent atom (potassco/clingo#671). The counterexample search (Lehtonen et al. 2021, Sec 4.2.3: UNSAT means skeptically accepted) read that UNSAT as acceptance. The correct answer is False: the only preferred extension is {}, and its closure does not contain q (Bondarenko et al. 1997, Th(T), p.69).

Fix

• _is_grounded(ctl, symbol) checks ctl.symbolic_atoms for the query atom.
• An ungrounded query is decided without calling clingo: no assumption set derives it, so the answer is False, with a preferred extension as the counterexample.
• The credulous complete and stable helpers get the same guard, so they no longer depend on how clingo handles absent atoms.

Routes checked

A probe over 336 checks compared every route with the native reference on four assumption-free and small frameworks, across complete, preferred and stable semantics, credulous and skeptical tasks, and every language literal. The routes covered were:

• solve_aba_with_backend with asp and support_reference, each with simplify on and off;
• solve_aba_acceptance with native, sat, asp and auto.

Before the fix, 4 checks failed: all were skeptical preferred on the assumption-free framework, via the ASP routes and auto (which dispatches to ASP here). Native, SAT and support-reference were already correct. After the fix, all 336 checks pass.

Tests (tests/structured/aba/test_aba_skeptical_underivable.py)

• The issue's reproduction, with simplify on and off: the answer is False, the counterexample is {}, and there are at most 2 solver calls. Both cases failed before the fix.
• Every acceptance route rejects the underivable literal, for 3 semantics × 2 tasks × 4 backends. The ASP and auto skeptical-preferred cases failed before the fix.
• Control: with the fact rule -> q, every route accepts q.
• A Hypothesis guard checks that ASP matches native on generated assumption-free frameworks. It already passed before the fix; the explicit cases above are what pin the regression.

Closes #72

🤖 Generated with Claude Code

https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg