I'm really struggling on how to resolve a Semantic Tableaux in FOL. I've read a lot of explanations but in simple I really don't understand the exact algorithm and I have not found something similar.
I know the basic rules, like instantiation of different constants for different existential quantifiers, don't eliminate universally quantified formulas and so on...
I think my problem is that I don't understand how and with which criteria the constants are substituted in the universally quantified formula.
thanks for your time
