Expose a checkable witness and a serialization schema for external verification consumers

## Context

I have been evaluating SoleLogics as the interval-reasoning engine behind an external verification tool ([reasonsmith](https://github.com/eduardstan/reasonsmith)), which checks decision systems against formalised regulatory duties. Its core discipline is that the trusted core must **independently re-verify** whatever an external engine reports, rather than trusting it — so an engine's answer is only as useful as the evidence it can hand back.

SoleLogics is the most complete open interval-temporal model checker I know of, and the interval frames plus Allen relations are exactly the right vocabulary. Two gaps currently stop a soundness-first consumer from using it as more than a black box. Both are additive; neither changes existing behaviour.

## 1. A checkable witness alongside the Boolean

`check(φ, i, w)` returns a `Bool` ([`modal-logic.jl`](https://github.com/aclai-lab/SoleLogics.jl/blob/main/src/utils/modal-logic/modal-logic.jl), return contract in [`interpretation.jl`](https://github.com/aclai-lab/SoleLogics.jl/blob/main/src/types/interpretation.jl)). For an external checker that must confirm the verdict itself, a bare Boolean is not enough: there is nothing to replay.

What would unlock it is a **witness object on a decided formula** — the falsifying (or satisfying) world(s), the relation edges taken, and the valuation of the relevant atoms over those worlds: enough for an independent evaluator to re-derive the same answer over the same finite frame.

`use_memo` already exposes satisfying-world sets for subformulas, and pairing those with `accessibles` does reconstruct something usable — but that is caller-side archaeology against internals, not a stable contract. An opt-in keyword (`check(φ, i, w; witness=true)`) returning a documented structure would be enough, and would let downstream tools report *"verified against a re-checked witness"* instead of *"the engine said so."*

## 2. A serialization schema for frame, formula, result and witness

Today, using SoleLogics from outside Julia means embedding Julia. A documented wire format — JSON or equivalent — for a finite frame, a formula, the result, and the witness above would make it usable as a language-agnostic reference oracle, driven over a process boundary with a reproducible engine version.

This matters beyond one consumer: it is what lets other tools use SoleLogics for differential testing against their own implementations.

## Smaller note

The docs index advertises a Z3 / validity path, but `Project.toml` lists no Z3 dependency and I could not find a corresponding API in the release source. Either the path is optional and undocumented, or the claim is stale — worth clarifying so consumers do not plan around it.

## Not a blocker

To be clear about scope: nothing here blocks the work that prompted it. Our near-term duties are metric deadlines that need an event clock rather than Allen relations, and we built that separately. This is forward-looking — the hooks that would let a verification tool treat SoleLogics as a trusted component when a genuine interval-relation requirement appears.

Happy to help implement either of these.

The issue describes changes to the `check` function in `src/utils/modal-logic/modal-logic.jl` and its return contract in `src/types/interpretation.jl`. Start by understanding the existing memoization and accessible world structures. The goal is to design a witness data structure and a serialization format (likely JSON) for frames, formulas, and results. Review how `use_memo` and `accessibles` work to inform the witness design.

Escrito por el modelo de indexación a partir del texto del issue.