Syntax Splitting Exploratorium: Construct, explore, and split - formal reasoning made interactive.
The Syntax Splitting Exploratorium (SSE) is an interactive web tool for constructing total preorders, ranking functions, and conditional knowledge bases and exploring their (conditional) syntax splittings via a partition-lattice visualization.
Built with infeR & Leptos (Rust)
What is Syntax Splitting ?
Syntax splitting is a foundational principle in knowledge representation: irrelevant knowledge should not affect inferences. When knowledge can be decomposed into independent sub-languages, inference about one part must depend only on the relevant sub-language.
Formally introduced by Rohit Parikh in 1999 for belief sets, the idea has been lifted to richer formalisms:
- 1999 - Parikh: Syntax splitting for propositional belief sets
- 2017 - Kern-Isberner & Brewka: Syntax splitting for total preorders and ranking functions
- 2020 - Kern-Isberner et al: Syntax splitting for conditional knowledge bases
- 2023 - Heyninck et al.: Conditional syntax splitting for conditional knowledge bases
- 2025 - Spiegel et al.: Refined conditional syntax splitting for conditional knowledge bases
This interface captures calculation of syntax splittings for three kinds of frameworks
1. Total Preorders (TPOs)
A total preorder ≼ on worlds induces plausibility. TPO-splitting factors ≼ into independent sub-preorders.
2. Ranking Functions (OCFs, Ordinal Conditional Functions)
OCFs assign integers κ(ω) That as well as total preorders induce plausibility. OCF-splitting yields a partition where the global rank is the marginal-sum of local ranks.
3. Conditional Knowledge Bases (CKBs)
A CKB Δ is a set of conditionals (B|A), read “A typically implies B”. Conditional syntax splitting decomposes Δ into sub-bases Δ1,…,Δk that are conditionally independent given a subsignature Σ′. For any query whose atoms lie in Vj ⊆ Σ′, only the Σ′-relevant part Δ|Σ′ (conditionals that mention at least one atom from Σ′) is used, irrelevant defaults outside Σ′ cannot affect the answer. This concept is further refined into generalised safe conditional syntax splitting, allowing even weaker independence requirements while preserving the same irrelevance guarantee.
Web Interface Features
🔍TPO & OCF Construction + Simple Reversal
Construct total preorders or ranking functions by simply dragging and dropping complete conjunctions into a fitting ordinal structure. Reverse the order on click.
📑Conditional Syntax Splitting of CKBs
Construct a conditional knowledge base and provide the subsignature that it should split conditionally on via dragging and dropping the according propositional variables.
🔄Import & Export
Upload / download TPOs, OCFs, CKBs
.cl .pl .json .ron .toml .pklSupported file formats
🖱️SVG Splitting Lattice
View all syntax splittings of your chosen framework and structure in a neat SVG showing a splitting lattice. For total preorders you can also click any partition to construct an OCF via a marginal-sum approach!
How marginal-sum works
- Map TPO layer-indices → ranks 0,1,2,…
- Marginalise this trivial ranking function onto each block
- Sum marginals → exact OCF for the chosen split
Heredity of Syntax Splittings
TPO-splittings have the special feature that the unique finest syntax splitting does not necessarily imply that all coarsenings of this partition are also splittings. This peculiarity can be captured and characterised with heredity.
This heredity is indicated in the splitting lattice by thick blue incoming edges if the incoming edge originates from a hereditary splitting. Since the trivial splitting, i.e. the signature itself, is trivially a splitting and hereditary as the coarsest splitting, all edges originating from here are thick and blue.