Hi, I’m a beginner and i’m learning to use Prolog and would like to implement logical tableau. How can I do? For example i’d like if I give Prolog the following formula: (X+!Y)*!X he returns me the tableau tree and tells me for what evaluations the formula is satisfied. Thanks for your suggestions.
This is covered, amongst other places, in First-Order Logic and Automated Theorem Proving, Second Edition by Melvin Fitting (Springer 1996). The book is not freely available, but the Prolog code for it is here on the author’s website, and it contains an implementation of tableau.
1 Like