A logic question gets either proof or counterexample
- What it is
- A constructive method that aims to decide two modal logics by returning either a proof or a finite counterexample.
- Who did it
- Marianna Girlando, Roman Kuznets, Sonia Marin, and Lutz Straßburger
- What it could mean
- If the corrected proof-search method holds, it gives researchers a concrete way to turn a yes-or-no logical question into inspectable evidence either way.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A decision procedure for intuitionistic modal logic IS4 (and IK4) ↗See the proposed checks
Inspect the exact sequent system, loop-rule soundness/completeness conditions, termination argument, and finite-countermodel extraction; compare the corrected result precisely with the cited LICS 2023 formulation. Any executable proof-search replay must be independently implemented or source-locked in an isolated environment.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The abstract and conclusion say the procedure decides IS4 and IK4 by returning a proof of validity or finite countermodel, using loop rules in proof search, and that it fixes a mistake in the authors’ LICS 2023 contribution. A concrete proof/countermodel-producing method is a current, inspectable advance in the doing and checking of formal mathematics.
- Why this could matter
- A logic question gets either proof or counterexample Some mathematical statements are true in every allowed model; others fail somewhere. This paper claims a procedure that does not merely guess: for two specified logics, it returns a proof of truth or a finite model showing failure.
- If it holds up
- It would add a reusable proof-search pattern for deciding stated intuitionistic modal logics while making both positive and negative answers inspectable.
- If it does not
- A broken loop rule, termination argument, or countermodel construction would pinpoint why the promised decision procedure needs repair.
- Impact horizon
- Methods · Logic · Proof search · Mathematical verification
- Version
- submitted 2026-09-21 17:18:22 UTC
- Why we tracked it
- a newly posted, source-backed constructive proof-search method with an explicit correction to an earlier contribution. Intake does not independently establish the loop rules, completeness argument, or correction.
- Highest-risk dependency
- The advertised procedure depends on treating possibly unsound loop rules within a globally sound proof-search organization. A local rule reading, or a changed intuitionistic/modal frame convention, would not establish decidability or the finite-model claim.
- Available artifacts
- arXiv provides PDF, experimental HTML, and TeX source for a 26-page manuscript. The inspected primary record did not identify a Lean, Coq, Isabelle, proof-search implementation, certificate package, or repository. No artifact was downloaded, executed, or replayed.
- Current boundary
- Intake record only; examination not started.