Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
This work addresses automated theorem proving and model checking for intuitionistic tense logics, which is incremental as it builds on existing nested sequent frameworks but introduces new techniques for loop-checking and counter-model extraction.
The paper tackles the problem of automated reasoning for intuitionistic tense logics by developing a novel nested sequent proof-search methodology that supports finite counter-model extraction, using a loop-checking method based on homomorphisms to bound derivation heights and enabling extraction of proofs or counter-models from computation trees.
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}.