Uniform Lyndon interpolation is shown for GLS via non-wellfounded proofs, closing a prior gap and yielding an alternative cut-elimination proof.
Solovay (1976): Provability interpretations of modal logic
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
years
2026 3verdicts
UNVERDICTED 3representative citing papers
A linearization method enables a PSPACE proof-search algorithm for GL on labeled tree sequents, with counter-model extraction from failed searches and a reduction to linear nested sequents.
Complete classification of additive and normal formulas in modal logics K, GL, Grz, S4, and S5 for diamond interpretations, with parameter versions for K, GL, and S5.
citing papers explorer
-
Uniform Lyndon Interpolation via Non-wellfounded Proofs
Uniform Lyndon interpolation is shown for GLS via non-wellfounded proofs, closing a prior gap and yielding an alternative cut-elimination proof.
-
Optimizing Proof-Search via Linearization for G\"odel-L\"ob Logic with Tree-Hypersequents
A linearization method enables a PSPACE proof-search algorithm for GL on labeled tree sequents, with counter-model extraction from failed searches and a reduction to linear nested sequents.
-
On Interpretations of Normal Modal Logics
Complete classification of additive and normal formulas in modal logics K, GL, Grz, S4, and S5 for diamond interpretations, with parameter versions for K, GL, and S5.