check(::Atom, ::AbstractDict) returns nothing for an absent atom, but its docstring documents false

## Summary

`check(::Atom, ::AbstractDict)` returns `nothing` for an atom that is absent from the dictionary,
but its own docstring documents that case as returning `false`, and the public wrapper declares a
`Union{Bool, Vector{Bool}}` return. The documented example therefore cannot run.

## Evidence

The docstring in `src/utils/propositional-logic.jl` gives exactly this example:

```julia-repl
julia> check(Atom(3), Dict([1 => ⊤, 2 => ⊥]))
false
```

The implementation a few lines below returns `nothing` in that branch:

```julia
check(::CheckAlgorithm, a::Atom, i::AbstractDict) = haskey(a,i) ? Base.getindex(i, value(a)) : nothing
```

And the public entry point in `src/types/interpretation.jl` annotates the return:

```julia
function check(φ::Formula, args...; kwargs...)::Union{Bool, Vector{Bool}}
```

so the `nothing` cannot be converted. Running the documented example raises:

```
MethodError: Cannot convert an object of type Nothing to Union{Bool, Vector{Bool}}
```

with the stack trace pointing at `interpretation.jl:160`.

## Why it matters

An unassigned atom is the ordinary case of a partial assignment, and the documentation promises it
means `false`. Today the most basic query in the docstring throws instead of returning a usable
answer.

There is also a second, quieter risk in the same shape: where the value *does* survive to a caller,
`nothing` means *undetermined*, and a consumer must never read that as *false*. Whichever way this is
resolved, the two should not be silently interchangeable.

## What needs deciding first

This is an API semantics choice and belongs to the maintainers, not to a patch:

- **Closed-world**: an absent atom is `false`, matching the current docstring. Simple, and the
documented examples become true.
- **Three-valued**: an absent atom is genuinely undetermined, in which case the return type and the
docstring should say so explicitly and callers should be forced to handle it.

Either is defensible. The current state — documented as one, implemented as the other, and typed as
neither — is the only outcome that cannot be right.

## Done looks like

The chosen semantics implemented consistently for direct and compound checks, the docstring and the
declared return type agreeing with it, and a regression test covering the absent-atom case.

Happy to prepare the patch once the semantics are chosen.