exhibit: complete modal K, T, S4, and S5 decision procedures

[SMC17]

Objective

Restore the core normal modal family as separate complete finite-model exhibits rather than one finite-frame evaluator labeled S4.

Required architecture

• Shared validated modal formula AST and parser.
• Frame validators for arbitrary K, reflexive T, reflexive-transitive S4, and equivalence-frame S5.
• Sound and complete terminating tableau, filtration, or bounded-model construction appropriate to each named system.
• Serialized derivations for validity and concrete finite Kripke countermodels for invalidity.
• Independent evidence checker separated from search heuristics.

Acceptance gates

• Exact syntax and Kripke semantics documented per system.
• K/T/S4/S5 canonical axiom and separating-countermodel corpus.
• Exhaustive small-formula/frame differential oracle.
• Invalid frame-class claims fail closed.
• unknown is impossible for the complete admitted fragment or carries an explicit resource reason outside it.
• Mutation tests reject corrupted derivations and countermodels.
• Lean oracle formalizes frame conditions and at least the soundness of each characteristic axiom.
• Each system has its own evidence-backed museum contract.