In this brief article, we’re gonna discuss about Semantic Trees, or also called Proof Trees. A semantic tree is the skeleton of the PROPCompiler project. This tree allows the inference kernel to proof the logical truth  of certain set of formulas.Lastly, it works to notice, that  the semantic tree uses propositional logic to connect two nodes in a single node.

Nodes can be nested as much as we need, for example, the next figure shows a small semantic tree:

In the figure, you can see that we have two literal A and B, joined together by a implication operation. This combination creates a new node that is useful as operator for a further conjunction operation (with node C).

I hope you enjoy this article, write down comments if you have something to say, and visit our social media.


Leave a Reply

Your email address will not be published.