Document the nothing return, emit an extractable certificate, and state the decidable fragment

## Context

Evaluating SoleReasoners as the decision procedure behind an external verification tool ([reasonsmith](https://github.com/eduardstan/reasonsmith)), whose core requirement is that it must **independently re-check** an external engine's answer rather than trust it. Three things would make the tableau usable in that setting. All are additive.

## 1. Document the `nothing` return, and treat it as first-class

`alphasat` returns `true`, `false`, or `nothing`, where `nothing` signals the timeout / memory exit ([`alphasat.jl`](https://github.com/aclai-lab/SoleReasoners.jl/blob/main/src/many-valued-multi-modal-tableau/alphasat.jl)). A consumer must map that to an honest "not evaluated" rather than to a negative answer — conflating the two would be a soundness bug in the consumer, not in this library.

The return contract deserves to be documented explicitly, so nobody has to read the source to learn that a third outcome exists and what it means.

## 2. An extractable certificate for the decided directions

A Boolean cannot be re-checked. For the tool to report a *proved* result rather than a *trusted* one, it would need either:

- a **closed-tableau certificate** (or an equivalent proof object) for the unsatisfiable direction, and
- a **model / open branch** for the satisfiable direction,

in a form an independent checker can validate without re-running the tableau. Re-running SoleReasoners is not independent verification — it just relocates the trust.

The tableau already carries the structure internally (`father`, `children`, `world`, `frame`, `expanded`, `closed`); the ask is for a supported way to emit it. A custom `choosenode` can capture an open node today, but that is a bespoke callback rather than a stable format.

## 3. State the fragment and its guarantee

Which decidable Halpern–Shoham fragment does `MVHSTableau` decide, and what is its termination / complexity guarantee?

This is the question a consumer must answer before it can honestly promise anything: full HS satisfiability is undecidable, so "an HS tableau" alone does not tell a downstream tool whether a given duty shape terminates. Naming the fragment — and whether the guarantee holds over finite frames only — would let consumers map their problem onto it deliberately instead of hoping.

## One observed edge, for the docs

On a fresh runtime, a raw Boolean `¬` was not safe for `alphasat` until the documented `booleantofuzzy` transformation was applied; after transforming, `p ∧ (p → ⊥)` returned the expected unsatisfiable answer. That is correct behaviour as documented, but it is a sharp edge for a first-time caller and might deserve a prominent note.

Happy to help implement any of these.