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



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.