0
$\begingroup$

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

$\endgroup$
11

0

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.