  We encode a topological semantics for paraconsistent and paracomplete logics
enriched with recovery operators, by drawing upon early works on topological
Boolean algebras (by Kuratowski, Zarycki, McKinsey & Tarski, etc.). This work
exemplarily illustrates the shallow semantical embedding approach using
Isabelle/HOL and shows how we can effectively harness theorem provers, model
finders and "hammers" for reasoning with quantified non-classical logics.
