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. Ferrari
Secondo
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.
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
29-mar-2021
Article (author)
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

Caricamento pubblicazioni consigliate

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/2434/838833
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact