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.
2021
2021
Fiorentini, C.; Ferrari, M.
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/2122619
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact