A forward internal calculus for model generation in S4. (29th March 2021) - Fiorentini, Camillo; Ferrari, Mauro
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.