Decidability of MLSSPF
The analysis of the decision problem for MLSSPF is rather different from that for MLSSP. First of all, an MLSSPF-formula can contain an explicit literal that forces the model to be infinite (e.g., ¬Finite(x)), therefore MLSSPF cannot enjoy the small model property. The second different aspect of this application is that we shall not look for any particular shadow process since we use the same process of the previous application.
Unable to display preview. Download preview PDF.