unicode_fol_kit.semantics.nonmonotonic

Non-monotonic reasoning — minimal-model entailment (predicate circumscription).

Classical entailment is monotonic: adding premises never retracts a conclusion. Common-sense reasoning is not — “Tweety is a bird” lets you conclude “Tweety flies” until you learn “Tweety is a penguin”. Circumscription (McCarthy) captures this by believing only what holds in the minimal models of a theory: those that make the circumscribed predicates as small (false of as many things) as possible.

Γ ⊨_circ φ (circumscribing the predicates in circumscribed) holds iff φ is true in every model of Γ that is ≤-minimal — where M ≤ M' means M and M' share a domain, constants, functions and the non-circumscribed (fixed) predicates, and every circumscribed predicate’s extension in M is a subset of its extension in M'. With circumscribed=None all predicates are minimised (closed-world-style minimal-model semantics), so e.g. ∅ ⊨_circ ¬P(a).

The search reuses the finite model finder, so it is bounded (domains up to max_size): True is minimal-model entailment over models within the bound, not a proof over all (possibly infinite) models. The relation is genuinely non-monotonic — adding premises can flip a True to False.

Public API: minimal_models(), minimal_entails().

Functions

minimal_entails(premises, conclusion[, ...])

Return whether premises circumscriptively entail conclusion (bounded).

minimal_models(premises[, circumscribed, ...])

Return the ≤-minimal finite models of premises up to max_size (bounded).
unicode_fol_kit.semantics.nonmonotonic.minimal_models(premises, circumscribed=None, max_size=4, max_candidates=1048576, extra_signature=())[source]

Return the ≤-minimal finite models of premises up to max_size (bounded).

circumscribed names the predicates to minimise (default: every predicate). Models are compared only within a shared domain and fixed part, so the result is the union of the minimal models found at each domain size. extra_signature adds formulas whose symbols the models must interpret without being constrained by them (so a goal’s constants/predicates are total in every enumerated model).

Parameters:

  • circumscribed (set | None)

  • max_size (int)

  • max_candidates (int)

Return type:

List[Structure]

unicode_fol_kit.semantics.nonmonotonic.minimal_entails(premises, conclusion, circumscribed=None, max_size=4, max_candidates=1048576)[source]

Return whether premises circumscriptively entail conclusion (bounded).

True iff the (universally closed) conclusion holds in every minimal model of premises found up to max_size (see minimal_models()). Non-monotonic: strengthening premises can turn a True into a False.

Parameters:

  • conclusion (Node)

  • circumscribed (set | None)

  • max_size (int)

  • max_candidates (int)

Return type:

bool