{"id":"03544140-728d-47b1-81d1-8e7b53825a02","arxiv_id":"1908.03501","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Satisfiability for the modal logics K4×S5, S4×S5, and SSL is shown decidable in ESPACE, completing the proof of EXPSPACE-completeness.","lead":"The paper gives algorithms that decide whether formulas in three related modal logics are satisfiable in single-exponential space, improving a double-exponential upper bound. Together with a companion lower-bound proof, this confirms a twenty-year-old conjecture that these problems are EXPSPACE-complete.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified.","rationale":"The central claim is the ESPACE upper bound for K4×S5, S4×S5, and SSL. I checked the main proof chain: tableau-sets and tableau-clouds in Definitions 5.1 and 5.2, the tableau-model equivalence in Proposition 6.5, the correctness of the recursive algorithm in Proposition 7.2, and the space analysis in Sections 8 and 9. The recursion-depth bound in Proposition 8.3 is the most delicate part; its grouping into ≡X-blocks and use of Lemma 4.10 is coherent. Proposition 9.1's counting argument is loose but valid: even where it overcounts extension choices, it only needs upper bounds. The only visible blemish is a likely sign typo in the proof of Proposition 8.3, where χm∈G should read χm∉G to match condition (II); the surrounding argument supplies the correct reading. The sole external dependency is Lemma 2.7, the Gabbay-Shehtman commutator/product equivalence, together with the Dabrowski-Moss-Parikh cross-axiom characterization for SSL. These are standard published theorems, and I found no internal inconsistency or missing condition in how they are used. The reader's weakest-assumption analysis correctly identified this dependency, but I do not treat it as a live objection. The ACCEPT verdict stands.","tokens_in":25216,"tokens_out":47085,"duration_ms":532003,"concrete_test":"Independently re-derive the specific instance of Lemma 2.7 for K4×S5 and S4×S5 from [8, Theorem 7.12], ideally by constructing, from a finite rooted X×S5-commutator model, an X×S5-product model with a p-morphism onto it; if the construction works without extra conditions, the cited bridge is confirmed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The tableau construction, truth lemma, and space analysis are internally consistent. The only non-self-contained bridge is Lemma 2.7, which identifies X×S5-satisfiability in product frames with satisfiability in commutator frames and cites Gabbay-Shehtman [8, Theorem 7.12]; every subsequent step for K4×S5 and S4×S5 depends on it. If that cited equivalence had a hidden restriction, the ESPACE upper bounds would not apply to the product logics as standardly defined. I found no evidence of such a restriction, and the analogous SSL characterization by cross axiom models is likewise a standard published result. This is a verification dependency, not an identified flaw.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents deterministic single-exponential-space decision procedures for the satisfiability problems of the bimodal product logics K4×S5 and S4×S5 and of the subset space logic SSL. The main result, Theorem 3.1, states that K4×S5 satisfiability can be decided in space O(n·2^{3n}) and that S4×S5 and SSL satisfiability can be decided in space O(n·2^{2n}), where n is the input formula length. The algorithms are based on a tableau method using 'tableau-clouds', prefabricated sets of complete tableau-sets, and on recursive procedures similar to Ladner's algorithm for S4. The proof proceeds by establishing an equivalence between satisfiability and the existence of partial tableaux (Proposition 6.5), proving the correctness of the recursive algorithms (Propositions 7.2 and 7.4), and giving space bounds through a careful analysis of the recursion depth using combinatorial estimates on the maximum chain length of certain relations (Propositions 4.11, 8.1, 8.3, and Corollary 8.2). A separate counting argument (Proposition 9.1) improves the bound on the number of tableau-sets for S4×S5 and SSL, yielding the sharper O(n·2^{2n}) bound. The companion paper establishes EXPSPACE-hardness, so together the results show EXPSPACE-completeness.","tokens_in":9,"tokens_out":30849,"duration_ms":520888,"significance":"If the results are correct, they constitute a substantial improvement over the previously known N2EXPTIME upper bound for these three logics and settle the upper-bound side of Marx's conjecture that K4×S5 and S4×S5 are EXPSPACE-complete. The tableau-cloud framework and the combinatorial observations about maximum chain lengths (Section 4.2, especially Proposition 4.11) are likely to be of independent interest for other modal and description logics. The upper-bound proofs are largely self-contained, with the only external dependencies being the standard Gabbay-Shehtman equivalence between product and commutator frames (Lemma 2.7) and the Dabrowski-Moss-Parikh characterization of SSL by cross axiom models. The paper gives detailed, checkable proofs of the tableau-model equivalence, the correctness of the recursive algorithms, and the space bounds, including explicit high-level implementation sketches for the Turing-machine storage of tableau-sets and tableau-clouds.","major_comments":[],"minor_comments":[{"comment":"The Truth Lemma is stated as a biconditional for all points (F,F) in the model MT, but the proof of the 'only if' direction for the case ψ=□χ invokes 'the second condition in Definition 5.5', which applies only to F∈T\\{F0,...,F_{m-1}}. For a partial tableau for a one-point sequence (ϕ,F0), the condition does not apply to F0. This is not merely a gap in the proof: the statement is false. For example, take X=K4×S5, ϕ=□p, F0={{□p},∅}, and T={F0}. Then T is a partial tableau for (ϕ,F0), but in MT there are no ♦-successors from (F0,∅) (since F0≤XF0 fails because {□p}≼{□p} would require p∈{□p}), so MT,(F0,∅)|=□p vacuously, while □p∉∅. The 'if' direction, which is the direction used in Proposition 6.5, is correct. I recommend either restricting the 'only if' direction to points with F∉{F0,...,F_{m-1}}, or stating the lemma only in the direction actually needed.","section":"Lemma 6.4.2"},{"comment":"In the paragraph beginning 'Otherwise, as at least the first part of (II) is satisfied for m', the text reads 'there is some G∈F_{m+1} with F_m≼X G and χ_m∈G' and later 'χ_~m∈G'. These should be 'χ_m∉G' and 'χ_~m∉G', respectively, to match condition (II) in Definition 7.1, which requires that the successor tableau-set excludes the formula χ. The intended argument is clear, but the typos should be corrected.","section":"Proof of Proposition 8.3"},{"comment":"Twice, the alphabet for the length of a bimodal formula is given as '{(,),¬,∧,□,K,X,0,1}'. Since variables in Definition 2.1 are written with a lowercase 'x' (as in x0, x101), the alphabet should presumably include 'x' rather than 'X'.","section":"Remark 8.4"},{"comment":"The notation '2(2·n/3)' and similar expressions (e.g., '2(2·n/3)−1') are meant to denote powers 2^{2n/3} and 2^{(2n/3)−1}. The current notation is ambiguous and should be typeset with an explicit exponent.","section":"Proposition 9.1 and its proof"},{"comment":"The condition '{ψ∈L| □ψ∈F}⊆ G' uses the entire language L, but since F⊆sf(ϕ), the set is actually a subset of sf(ϕ). Rewriting it as '{ψ∈sf(ϕ)| □ψ∈F}⊆ G' would improve readability and avoid any confusion about infinite languages.","section":"Definition 5.2(1)(a)"},{"comment":"The space analysis is presented as a high-level implementation sketch. In particular, it would be helpful to explain how the recursion stack stores the sequence (F0,...,Fm) without storing the entire sequence in each activation record, e.g., by storing only the new cloud and traversing the stack to check the pairwise-difference condition. This is not a correctness concern, but it would make the O(n(n+A)^3) bound easier to verify.","section":"Section 8 (proof of Proposition 8.1)"}],"recommendation":"minor_revision","confidential_remarks":"The manuscript is a solid piece of work with detailed and largely correct proofs. The main concern is the false statement of Lemma 6.4.2; although the false direction is not used in the central argument, it should be fixed before publication to avoid misleading readers. The small typos and notation issues are straightforward to address. I see no obstacle to acceptance after these local revisions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Peter, if you want to know whether this paper is worth your time: yes. Hertling and Krommes give an ESPACE upper bound for K4×S5, S4×S5, and SSL, improving the standing N2EXPTIME bound and, with their companion lower-bound paper, establishing EXPSPACE-completeness for all three. The result itself is the main event and, as far as I can tell, correct.\n\nWhat's actually new: the tableau-cloud construction. Instead of building tableaux point by point, they work with prefabricated sets of tableau-sets—clouds—that mirror L-equivalence classes. This neatly handles both the diamond successors and the commutativity conditions. The recursive algorithm is similar in spirit to Ladner's for S4, but the cloud machinery is original. The combinatorial core is a set of observations about transitive relations and maximum chain length, culminating in Proposition 4.11, which bounds the chain length of the lifted preorder on the power set. On top of that they prove a counting lemma (Proposition 9.1) showing that for S4×S5 and SSL the number of tableau-sets is at most 2^{2n/3}, which yields the sharper O(n·2^{2n}) space bound. The counting argument is a little tedious but sound.\n\nWhere are the soft spots? The upper bound is proved for commutator models, not product models directly. They rely on Lemma 2.7, citing Gabbay–Shehtman, to equate X×S5-satisfiability in product frames with satisfiability in commutator frames, and on Dabrowski–Moss–Parikh for the SSL cross-axiom characterization. These are standard published results, so it's a verification dependency, not a flaw. But if either of those cited theorems had an unstated restriction, the result wouldn't apply to the logics as usually defined. I see no evidence of that.\n\nThe space analysis is an implementation sketch on a multi-tape Turing machine, not a formal proof with explicit tape counts. That's normal for this kind of paper; the bounds are plausible and the recursion-depth argument is transparent. The paper is also one half of a pair—the lower bound is in Part 2, so the abstract's completeness claim rests on the companion.\n\nOverall: this deserves a serious referee. I would send it to a good modal-logic journal and expect acceptance after minor comments. The main thing to check carefully is the transfer lemma and the counting induction.","headline":"A solid, careful upper-bound proof that settles a twenty-year-old question; the tableau-cloud method and counting lemma are genuinely new.","tokens_in":25857,"tokens_out":3499,"would_cite":true,"duration_ms":35052,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","68Q17","03D15"],"pacs":[],"model":"deepseek-v4-flash","headline":"The satisfiability problems of K4×S5, S4×S5, and the subset space logic SSL are decidable in single-exponential space, placing them in ESPACE.","keywords":["bimodal product logics","subset space logic","satisfiability problem","EXPSPACE-completeness","ESPACE","tableau algorithms","K4×S5","S4×S5"],"falsifier":"Exhibit a bimodal formula that is satisfiable in a K4×S5 commutator model but not in any K4×S5 product model (or the analogous counterexample for S4×S5, or a formula with a cross axiom model but no subset space model). No such counterexample is known, and the paper relies on the cited theorem that none exists.","tokens_in":24920,"feed_emoji":"🧮","tokens_out":6858,"duration_ms":61019,"temperature":0.7,"pith_summary":"The paper establishes that the satisfiability problems for the bimodal product logics K4×S5 and S4×S5 and for the subset space logic SSL are solvable by deterministic Turing machines using only single-exponential space, i.e., O($2^{{c n}}$) for a constant c. More precisely, K4×S5 is decided in O(n·$2^{{3n}}$) space, while S4×S5 and SSL are decided in O(n·$2^{{2n}}$) space. These are the first ESPACE upper bounds for the three problems, improving the previous N2EXPTIME bound. Together with the companion paper's EXPSPACE-hardness result, this settles a conjecture stated in the literature that these logics are EXPSPACE-complete.","feed_headline":"Single-exponential space decides K4×S5, S4×S5, and SSL","feed_subtitle":"That matches a companion lower bound, making all three satisfiability problems EXPSPACE-complete.","key_machinery":"The load-bearing objects are 'tableau-clouds': sets of complete tableau-sets that represent the equivalence classes of the K-modality, so that all K-formulas are satisfied inside one cloud and commutativity conditions are automatically satisfied when clouds are linked. The algorithms recursively assemble these clouds into partial tableaux, trying backwards loops to already built clouds before creating a new successor cloud. The proof of the space bound rests on the maximum-chain-length lemma for transitive relations lifted to the power set: a transitive relation on a finite set S induces a transitive relation on P(S) whose chains have length at most 2·|S_≡|, bounding how often the minimal-cloud set can change and hence bounding recursion depth.","core_discovery":"The central discovery is a decision method that replaces the search for a possibly infinite product model by the search for a finite object built from prefabricated parts called 'tableau-clouds' — collections of complete formula-sets that mirror the equivalence classes of the knowledge modality. The paper proves that a formula is satisfiable in the appropriate class of models exactly when such a partial tableau exists, and gives recursive algorithms that search for partial tableaux. The recursion depth is controlled by a combinatorial bound on chains in the induced relation on sets of tableau-sets, which yields O(n·|T|^3) space where T is the set of relevant tableau-sets. Since |T| ≤ 2^n, this gives O(n·$2^{{3n}}$) for K4×S5; an extra counting argument improves the bound to O(n·$2^{{2n}}$) for S4×S5 and SSL.","pith_inferences":["The maximum-chain-length bound in Proposition 4.11 is a general combinatorial tool that could give recursion-depth bounds for other tableau or mosaic methods without first constructing exponential-size models.","The counting argument bounding the number of tableau-sets might be refined further, especially for K4×S5 with a modified tableau definition, to lower the exponents below 3 and 2.","A natural testable extension is to adapt the tableau-cloud construction to other product combinations, such as products with transitive or Euclidean modalities; if the chain-length control survives, similar ESPACE bounds would follow.","For SSL, richer subset-space logics with additional modalities could be approached by extending cross-axiom tableau-clouds, although the paper does not address such extensions."],"forward_implications":["The three satisfiability problems are EXPSPACE-complete, once paired with the companion paper's EXPSPACE-hardness proof.","K4×S5 can be decided in O(n·2^{3n}) space, and S4×S5 and SSL in O(n·2^{2n}) space, by explicit deterministic algorithms.","The previous N2EXPTIME upper bound for these problems is superseded, and the conjectured EXPSPACE-completeness is confirmed.","Satisfiability in these logics is equivalent to existence of a finite partial tableau over at most 2^n tableau-sets, so an infinite-model search is replaced by a finite one.","Because ESPACE is closed under complements, the same space bounds apply to validity as well as satisfiability for these logics."],"supporting_citations":[{"why":"Establishes the equivalence between product and commutator frames used as Lemma 2.7, the bridge that lets the algorithms work on commutator models.","marker":"[8]"},{"why":"Provides the prior N2EXPTIME upper bound and doubly exponential bounded-model results that this paper improves, and records the EXPSPACE-completeness conjecture.","marker":"[18]"},{"why":"Shows SSL can be characterized by cross axiom models and supplies the doubly exponential small-model bound that the SSL algorithm replaces.","marker":"[4]"},{"why":"Supplies the recursive decision-algorithm pattern for modal logic S4 on which the tableau-cloud recursion is modeled.","marker":"[19]"},{"why":"Companion paper proving EXPSPACE-hardness, which together with these upper bounds yields EXPSPACE-completeness.","marker":"[14]"},{"why":"Poses the complexity question for S4×S5 whose answer this paper's upper bound completes.","marker":"[20]"},{"why":"Provides the mosaic idea that the tableau-cloud construction resembles.","marker":"[21]"}],"fun_headline_variants":["EXPSPACE-complete: K4×S5, S4×S5, SSL in single-exponential space","Tableau-clouds yield single-exponential space for K4×S5, S4×S5, SSL","EXPSPACE-complete for K4×S5, S4×S5, SSL via tableau-cloud search","Single-exponential space algorithms for K4×S5, S4×S5, SSL"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is the cited equivalence between satisfiability in product frames and satisfiability in the more general commutator frames (and, for SSL, between subset space models and cross axiom models); if that equivalence ever failed, the algorithms would decide the wrong class of models and the ESPACE upper bound would not apply to the logics as standardly defined.","fun_headline_variants_meta":{"raw":{"variants":["EXPSPACE-complete: K4×S5, S4×S5, SSL in single-exponential space","Tableau-clouds yield single-exponential space for K4×S5, S4×S5, SSL","EXPSPACE-complete for K4×S5, S4×S5, SSL via tableau-cloud search","Single-exponential space algorithms for K4×S5, S4×S5, SSL"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001117,"raw_usage":{"total_tokens":4585,"prompt_tokens":815,"completion_tokens":3770,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":431,"completion_tokens_details":{"reasoning_tokens":3656}},"tokens_in":431,"tokens_out":3770,"duration_ms":25788,"temperature":1.0,"reasoning_tokens":3656,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:11:46.288908+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a bimodal formula that is satisfiable in a K4×S5 commutator model but not in any K4×S5 product model (or the analogous counterexample for S4×S5, or a formula with a cross axiom model but no subset space model). No such counterexample is known, and the paper relies on the cited theorem that none exists.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the equivalence between product and commutator frames used as Lemma 2.7, the bridge that lets the algorithms work on commutator models."},{"cited_title":"Dabrowski, L","cited_arxiv_id":null,"evidence_quote":"Shows SSL can be characterized by cross axiom models and supplies the doubly exponential small-model bound that the SSL algorithm replaces."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the recursive decision-algorithm pattern for modal logic S4 on which the tableau-cloud recursion is modeled."},{"cited_title":"Hertling and G","cited_arxiv_id":null,"evidence_quote":"Companion paper proving EXPSPACE-hardness, which together with these upper bounds yields EXPSPACE-completeness."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Poses the complexity question for S4×S5 whose answer this paper's upper bound completes."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the mosaic idea that the tableau-cloud construction resembles."}],"review_version":1}