Abstract
We introduce a generalized topological semantics for paraconsistent
and paracomplete logics by drawing upon early works on topological
Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey &
Tarski, etc.). In particular, this work exemplarily illustrates the
shallow semantical embeddings approach (SSE)
employing the proof assistant Isabelle/HOL. By means of the SSE
technique we can effectively harness theorem provers, model finders
and 'hammers' for reasoning with quantified non-classical
logics.
License
Topics
Session Topological_Semantics
- sse_boolean_algebra
- sse_boolean_algebra_quantification
- sse_operation_positive
- sse_operation_positive_quantification
- sse_operation_negative
- sse_operation_negative_quantification
- topo_operators_basic
- topo_operators_derivative
- topo_alexandrov
- topo_frontier_algebra
- topo_negation_conditions
- topo_negation_fixedpoints
- ex_LFIs
- topo_strict_implication
- ex_subminimal_logics
- topo_derivative_algebra
- ex_LFUs
- topo_border_algebra
- topo_closure_algebra
- topo_interior_algebra