The Smullyan Uniform Notation for First Order formulas with equality

The expansion rules (according to Smullyan Uniform Notation) and others for indicating initial formulas and unexplored branches.

The structure that represents a tableau, that is, a Tree of STEQNode

The structure that represents a node of a tableau. It contains the information of the index of the node, its formula, the indices of nodes from it is derived, the substitution made (if it is derives from universal or existential formula), the simplifications made (with respect to equalities) and the expansion rule involved in the derivation

It gives the class of a FOLEQ formula (according to Smullyan Uniform Notation). Atoms (predicates) and their negations are literals, double negation are typed as DN, conjunction, equivalence are classified as ALPHA, disjunction and implications are classified as BETA. forall-like formulas are classified as GAMMA and existencial-like ones as DELTA The negation of an alpha formula is a beta and vice versa, and the same happens with forall and exists like ones.

It allows construct the Semantic Tableau of a set of formulas. It recieves two additional parameters that corresponds to the maximum generated constants and the maximum size of terms allowed, respectively.

It decides if the given tableau has all its branches closed.

It gives a String representation of a Semantic Tableau

It gives a DOT representation for the tableau.

It gives a DOT representation for the tableau, with custom styles.

It gives a JSON Tree representation for the tableau.