A forward internal calculus for model generation inS4
Camillo Fiorentini, Mauro Ferrari · Journal of Logic and Computation · 2021
Abstract We propose an internal calculus to check the satisfiability of a set of formulas in ${\boldsymbol {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.