on March 27, 2017
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.