Module modal 

Structs

Belief

A signed belief: atom held positively (positive == true) or negatively.

Enums

ModalSystem

The normal modal axiom systems this engine recognises.

Functions

contract

AGM contraction K − φ: remove belief if present (vacuous if absent). Writes the result into out, returns its length.

everyone_knows

“Everybody knows” prop at world: K_i φ holds for every agent in agent_accesses.

expand

AGM expansion K + φ: add belief if absent. Writes the result into out, returns its length (no deductive closure beyond the explicit literals — a finite base model).

is_consistent

A belief base is consistent iff no atom is held both positively and negatively.

is_euclidean

Euclidean (axiom 5: ◇φ→□◇φ): wRv ∧ wRu ⇒ vRu.

is_reflexive

Reflexive (axiom T: □φ→φ): every world accesses itself.

is_serial

Serial (axiom D: □φ→◇φ): every world accesses at least one world.

is_symmetric

Symmetric (axiom B: φ→□◇φ): wRv ⇒ vRw.

is_transitive

Transitive (axiom 4: □φ→□□φ): wRv ∧ vRu ⇒ wRu.

knows

K_i φ — agent i (via its accesses_i relation) knows prop at world: every world i-accessible from world satisfies it.

necessary

□φ (necessary) — ALL worlds accessible from world satisfy prop. Vacuously true when no worlds are accessible (standard modal semantics).

possible

General modal logic over a Kripke frame — the shared modal substrate (□/◇) that the specific modalities (deontic, epistemic) specialise. Accessibility is (world →accesses→ world') (predicate == accesses); a world satisfies a proposition when (world, holds, prop) is present. Zero-heap (linear scans).

revise

AGM revision K * φ via the Levi identity: drop any belief about belief.atom (so the contrary ¬φ is contracted), then add φ. The result satisfies success (φ ∈ K*φ) and consistency (never both φ and ¬φ). Writes into out, returns its length.

validates

Does the frame validate the characteristic axiom(s) of system over worlds?