Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912990699192320 |
|---|---|
| author | Lyon, Tim S. |
| author_facet | Lyon, Tim S. |
| contents | This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-checking method that detects repeating nested sequents using homomorphisms, thereby bounding the height of derivations during proof-search. Due to the non-invertibility of some inference rules, the algorithm does not construct a single derivation, but a generalized structure we call a 'computation tree.' We show how proofs and counter-models can be extracted from computation trees when proof-search succeeds or fails, respectively. This establishes the finite model property for each ITL of the form IKt + A with A a subset of {T,B,D}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_29424 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents Lyon, Tim S. Logic in Computer Science This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-checking method that detects repeating nested sequents using homomorphisms, thereby bounding the height of derivations during proof-search. Due to the non-invertibility of some inference rules, the algorithm does not construct a single derivation, but a generalized structure we call a 'computation tree.' We show how proofs and counter-models can be extracted from computation trees when proof-search succeeds or fails, respectively. This establishes the finite model property for each ITL of the form IKt + A with A a subset of {T,B,D}. |
| title | Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.29424 |