We propose an internal calculus to check the satisfiability of a set of formulas in ${oldsymbol {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
Fiorentini C.
;Ferrari M.
2021-01-01
Abstract
We propose an internal calculus to check the satisfiability of a set of formulas in ${oldsymbol {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
non disponibili
Tipologia:
Versione Editoriale (PDF)
Licenza:
Copyright dell'editore
Dimensione
1.77 MB
Formato
Adobe PDF
|
1.77 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
