We propose an internal calculus to check the satisfiability of a set of formulas in S4. Our calculus directly supports model extraction and is designed so to implement a forward proof-search strategy that can be understood as a top-down construction of a model. We prove that the extracted models have minimal height.
A forward internal calculus for model generation in S4 / C. Fiorentini, M. Ferrari. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - (2021). [Epub ahead of print] [10.1093/logcom/exab014]
A forward internal calculus for model generation in S4
C. Fiorentini
Primo
;M. FerrariSecondo
2021
Abstract
We propose an internal calculus to check the satisfiability of a set of formulas in S4. Our calculus directly supports model extraction and is designed so to implement a forward proof-search strategy that can be understood as a top-down construction of a model. We prove that the extracted models have minimal height.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
exab014.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
1.72 MB
Formato
Adobe PDF
|
1.72 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
