nogood-backtracking

57 beliefs (50 IN, 7 OUT)

• IN absence-and-outlist-form-complete-negative-semantics
  The system has complete semantics for all forms of negation: structural absence produces emergent premise behavior and asymmetric fail modes, while explicit outlist entries provide conjunctive defeat with defined absent-node handling and persistence — together covering every mechanism by which beliefs can be negated or defeated.
• IN absence-has-consistent-dual-semantics
  Absence has deliberate, defined semantics throughout the system at two levels: structural absence (no justifications) creates premise behavior via vacuous truth over empty lists, while referential absence (missing nodes) follows conservative/permissive asymmetry — both forms of absence produce predictable behavior rather than errors or undefined state.
• IN add-nogood-always-records
  `add_nogood` appends a `Nogood` record unconditionally before checking whether the contradiction is active, so nogoods are preserved even when not all member nodes are currently IN
• IN add-nogood-fallback-uses-dependent-count
  When `find_culprits` returns no candidates (all nogood nodes are premises with no justification chains), the fallback retracts the nogood member with the fewest direct dependents
• IN add-nogood-retraction-prefers-least-entrenched
  The primary retraction path traces back through justification chains to premises and chooses the one with the lowest entrenchment score (speculative assumptions before evidence-backed observations)
• IN all-defeat-mechanisms-are-reversible
  Every outlist-based defeat operation (challenge, kill-switch, supersession) is inherently reversible because outlist semantics flip truth values without deleting nodes
• IN backtracking-retracts-least-entrenched
  `add_nogood` resolves contradictions via dependency-directed backtracking: `find_culprits` traces to premises, scores by `_entrenchment`, and retracts the least-entrenched premise to minimize disruption.
• IN contradiction-dry-run-overrides-auto-apply
  When both `--dry-run` and `--auto-apply` are passed to the `contradictions` CLI subcommand, no nogoods are recorded in the database (applied count is 0).
• IN contradiction-in-only-filter
  `detect_contradictions` excludes OUT nodes from LLM prompts even when explicitly listed in `belief_ids`.
• IN contradiction-management-is-complete-and-traceable
  The system provides complete contradiction management: the revision pipeline reliably resolves contradictions through outlist defeat and dependency-directed backtracking with guaranteed termination, while nogood resolution maintains a consistent referenceable history of all detected contradictions — enabling both automated resolution and post-hoc forensic analysis of belief conflicts.
• IN contradiction-min-two-claims
  `parse_contradiction_response` drops any nogood with fewer than 2 valid claim IDs; this is enforced both before and after `valid_ids` filtering.
• IN contradiction-plan-round-trips-apply-entries
  Writing a contradiction plan with `write_contradiction_plan` and parsing it back with `parse_contradiction_plan` preserves all `[APPLY]`-tagged NOGOOD entries with their IDs and claims, while discarding `[SKIP]`-tagged entries — enabling a human review workflow.
• IN contradiction-resolution-achieves-minimal-impact-complete-cascades
  Contradiction resolution simultaneously achieves minimal disruption (least-entrenched culprit selection with surgical recovery hints targeting only cascade victims) and complete effect propagation (retraction cascades transitively through all dependent nodes with guaranteed termination) — the system minimizes blast radius while ensuring no node escapes the cascade.
• IN contradiction-resolution-is-lifecycle-safe
  When contradictions are detected, the entire resolution pipeline respects node lifecycle: backtracking identifies the least-entrenched culprit premise deterministically, retraction cascades through BFS propagation that skips retracted nodes and stops on unchanged truth values, ensuring resolution terminates without disturbing lifecycle-inert nodes.
• IN contradiction-resolution-is-minimal-disruption
  The nogood resolution system minimizes network disruption through layered heuristics: the primary path traces justification chains back to premises and selects the least-entrenched for retraction, the fallback uses dependent count when no traceable chain exists, and all contradictions are unconditionally recorded regardless of resolution outcome.
• IN contradiction-resolution-is-traceable-and-recoverable
  Contradiction resolution provides complete operational support along two independent dimensions: it minimizes disruption with guided recovery (least-entrenched culprit selection plus surgical restoration hints for cascade victims), AND creates consistently identifiable artifacts (nogoods with durable collision-free IDs, challenge nodes with deterministic auto-IDs), enabling both forensic root-cause analysis and practical guided recovery.
• IN contradiction-resolution-minimizes-disruption-and-guides-recovery
  Contradiction resolution achieves both minimal impact and guided recovery: dependency-directed backtracking selects the least-entrenched culprit premise to minimize the retraction cascade, while restoration hints identify specific cascade victims that have surviving alternative premises — providing a complete resolve-and-recover pipeline
• IN contradiction-triggers-deterministic-resolution
  When contradictions are detected, resolution and propagation form a deterministic pipeline: backtracking identifies the least-entrenched culprit premise, retraction triggers BFS propagation that terminates via stop-on-unchanged, producing a new consistent state with minimal network disruption and guaranteed convergence.
• IN contradictions-belief-text-truncated-at-200-chars
  `format_beliefs_for_contradiction_check` truncates each belief's text at 200 characters in the LLM prompt to avoid blowing context windows on large belief descriptions
• IN contradictions-cross-batch-pairs-undetected
  Batch boundaries are non-overlapping — each belief appears in exactly one batch per run — so contradictions between beliefs in different batches cannot be detected in a single run.
• IN contradictions-min-two-claims-per-nogood
  The contradiction parser enforces that every returned nogood has at least 2 valid claim IDs; single-claim or empty results are silently dropped.
• IN contradictions-no-storage-dependency
  `contradictions.py` operates on in-memory node dicts and has no import of `storage.py` or any database layer, making it testable in full isolation.
• IN contradictions-only-checks-in-beliefs
  `detect_contradictions` filters all input to `truth_value == "IN"` before processing; OUT beliefs are never sent to the LLM for contradiction checking.
• IN contradictions-semantic-skips-singleton-clusters
  `detect_contradictions_semantic` skips any cluster containing fewer than 2 beliefs, since no pairwise contradiction is possible within a singleton
• IN contradictions-shuffle-prevents-deterministic-batching
  Belief IDs are randomly shuffled before batching so that repeated runs cover different pairwise combinations across batch boundaries, increasing cross-batch contradiction coverage.
• IN contradictions-shuffles-before-batching
  The `contradictions` command randomly shuffles all IN beliefs before partitioning into batches of 50, ensuring that repeated runs probabilistically cover cross-belief comparisons that fixed sequential batching would never surface.
• OUT dispute-resolution-is-complete-and-reliable
  Both dispute resolution mechanisms — intentional (dialectical challenge/defend with irreversible premise transformation) and automated (contradiction detection with dependency-directed backtracking) — are individually fully reliable, crash-safe, and traceable, leaving no dispute pathway that could silently fail or lose history.
• OUT dispute-resolution-is-topology-accurate
  Both dispute resolution mechanisms — intentional dialectical challenge/defend and automated contradiction resolution — propagate their effects through an accurate convergent topology with complete dependency tracking, ensuring every transitively affected node reaches its correct truth state after any dispute.
• OUT dispute-resolution-spans-all-origins
  Both dispute resolution mechanisms (intentional dialectical and automated contradiction) are complete and reliable, and all belief origins participate in the same deterministic revision pipeline — every belief from any source can be disputed and resolved through identical mechanisms.
• IN edge-case-uniformity-reinforces-complete-negative-semantics
  Uniform handling of all semantic edge cases — vacuous premises, asymmetric absence, empty antecedents — reinforces the completeness and recoverability of negative semantics: every edge case within the negation lifecycle (missing outlist nodes treated as OUT, challenge of already-justified nodes, recovery from outlist defeat) is handled by the same minimal evaluation rules that ensure reversibility.
• IN multiple-outlist-is-conjunction
  When a justification has multiple outlist entries, ALL must be OUT for the justification to be valid; any single outlist node going IN defeats the entire justification
• OUT negation-is-transparent-to-evaluation
  The system's complete negative semantics — structural absence creating premise behavior, explicit outlist defeat with automatic reversal, and guided recovery — operate within transformation-invariant truth evaluation: negation mechanisms alter belief topology but never create special-case evaluation paths, because the same uniform rules evaluate all resulting structures identically regardless of how they were produced.
• IN negative-semantics-are-complete-reversible-and-recoverable
  The system's negative semantics form a complete belief modification lifecycle: complete semantics cover all negation forms (structural absence and explicit outlist defeat), all defeat mechanisms reverse automatically through BFS propagation cascades, and surgical restoration hints target only cascade victims with surviving premises — every belief retraction can be undone with guided recovery.
• OUT negative-semantics-are-uniform-through-minimality
  The system's complete negative semantics — structural absence creating premise behavior, explicit outlist defeat with automatic reversal, permanent identity effects from challenge — handle all edge cases uniformly because they derive from the same minimal primitives as all other truth evaluation, with no special-case handling for negation.
• IN negative-semantics-ground-deterministic-dialectics
  Complete reversible negative semantics — structural absence producing emergent premise behavior plus explicit outlist defeat with automatic reversal and guided recovery — are the foundation that enables deterministic reliable dialectics: challenge/defend operations inherit their determinism from evaluation purity applied to outlist primitives, and their reliability from the inherent reversibility of outlist-based defeat.
• IN negative-semantics-have-reversible-defeat-but-permanent-identity-effects
  The system's complete negative semantics — structural absence creating premise behavior and explicit outlist defeat — exhibit a fundamental asymmetry: all outlist-based defeat operations (challenge, kill-switch, supersession) are fully reversible in truth value, but dialectical challenge permanently destroys premise identity by injecting a justification into a formerly unjustified node, an irreversible structural transformation.
• IN network-retracted-nodes-persist
  Retracted nodes remain in `self.nodes` with `_retracted` metadata set; they are never deleted from the graph, enabling later restoration via `assert_node()` without rederivation.
• IN nogood-id-backwards-compat
  Databases created before the monotonic counter fix (lacking `network_meta` table) load without error; the counter is derived from max existing nogood ID + 1, or defaults to 1 if none exist
• IN nogood-id-collision-prevention
  After importing nogoods, `_next_nogood_id` is set to one past the highest imported ID, preventing `network.record_nogood` from generating a conflicting ID later.
• IN nogood-id-counter-is-monotonic
  `Network._next_nogood_id` only ever increases — deletion, clearing, save/load, and import never decrease it, preventing ID reuse after the issue #26 fix
• IN nogood-id-format-is-zero-padded
  Nogood IDs follow the format `nogood-NNN` with 3-digit zero-padded integers (e.g., `nogood-001`), and `_next_nogood_id` holds the next integer to assign, not the last used
• IN nogood-id-import-sync
  Both `import_json` and `import_into_network` must advance `_next_nogood_id` past the highest imported nogood ID to prevent collisions with pre-existing IDs
• IN nogood-id-monotonic
  `Network._next_nogood_id` only ever increases; deletions and clears do not decrement it, preventing ID reuse (fix for issue #26)
• IN nogood-id-persisted-in-meta
  The nogood counter is stored in the `network_meta` SQLite table and survives save/load cycles as a high-water mark, not a count of current nogoods
• IN nogood-ids-are-durable-and-collision-free
  Nogood IDs form a durable collision-free sequence: the counter only increases (surviving deletions and clears), persists across save/load cycles via the network_meta table, and advances past imported IDs to prevent collisions — no operation can produce a reused or ambiguous contradiction identifier
• OUT nogood-ids-assume-append-only
  Nogood IDs are derived from `len(self.nogoods) + 1`, so deleting a nogood from the list would cause ID collisions on subsequent calls
• IN nogood-resolution-maintains-consistent-ids
  Nogood recording and resolution produces a consistent, referenceable history of contradictions
• IN nogoods-require-valid-nodes
  Nogoods whose `Affects` list references node IDs not present in the network are silently skipped rather than raising an error during import
• IN non-monotonic-system-is-single-reversible-primitive
  The entire non-monotonic reasoning system — challenges, kill-switches, supersession, and dialectics — is built on a single primitive (outlist) that is inherently reversible, with no dedicated machinery for any defeat pattern.
• IN outlist-absent-means-out
  An outlist node that doesn't exist in the network is treated as OUT (justification satisfied); absent antecedent nodes fail validation — this asymmetry makes missing counter-evidence permissive while missing supporting evidence is strict
• IN outlist-enables-non-monotonic-reasoning
  The `outlist` field on `Justification` allows beliefs to be retracted when a defeating node becomes IN — this is the core non-monotonic mechanism powering `supersede`, `challenge`, and default-logic patterns.
• IN outlist-is-universal-defeat-mechanism
  The outlist primitive is the sole defeat mechanism underlying all non-monotonic features: challenges, agent kill-switches, supersession, and direct defeasible reasoning
• OUT outlist-nodes-not-in-dependents-index
  Outlist nodes are not tracked in the `dependents` index, so when an outlist node is retracted (goes OUT), dependent GATE beliefs are not enqueued for re-evaluation by `_propagate` — requiring manual `reasons assert` as a workaround.
• IN outlist-relationships-survive-persistence
  Outlists are stored as `outlist_json` in the SQLite `justifications` table; on load, the dependent index is rebuilt for both antecedents and outlist nodes, preserving propagation behavior across save/load cycles
• IN outlist-semantics-are-fully-specified
  The outlist primitive has complete, well-defined semantics: multiple entries form a conjunction (all must be OUT), absent nodes are treated as OUT (permissive default), and outlist relationships survive persistence through JSON serialization with rebuilt dependent indexes.
• IN supersession-is-reversible
  `supersede()` adds the new node's ID to the old node's outlist rather than deleting the old node; retracting the new belief automatically restores the old one through normal propagation
• IN supersession-is-reversible-and-view-consistent
  Supersession is both mechanically reversible (implemented via outlist, so retracting the superseder restores the original node's truth value) and view-consistent (superseded nodes are excluded from gated belief lists even if they retain active blockers), making it a first-class lifecycle operation rather than just a truth-value toggle.