It defines the type of a PL formula which can be a Literal, Double Negation, Alpha, Beta, Gamma (forall), Delta(exists) Insat or Taut

Defines the FOL Semantic Tableau type as a Graph whose node labels are pairs of an integer (0: internal node, 1: open leaf, -1: closed leaf) and a TableauNodeItem that contains some information for representation; and the edge labels are defined as TableauEdgeItem although some edges could not have any edge.

Defines the TableauNodeItem that is a record with the following features: 'f' the formula considered, 't' the type of the formula, 'u' the usability degree of the formula, 'ut': a list of terms with wich a gamma formula is solved, 'i':the index of the node (only for print the tableau), 'ps': the premises from which the formula is concluded

Defines the TableauEdgeItem that is a record with the following features 'r' the rule applied in the deduction, 'id' the set of indices over that the rule is applied, 'br' the identifier of the branch (only used in beta bifurcations), 's' the substitution done over the formula (only in gamma and delta rules).

It gives the class of a FOL formula. 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 gives the components of a unquantified formula for using them in the expansion of a semantic board

It gives the components of a quantified formula for using them in the expansion of a semantic board

It performs the Semantic Tableaux algorithm on a set of FOL formulas. As the algorithm can be infinite, you must indicate the maximum depth allowed. Specifically, you must specify the maximum number of times a gamma formula can be used and the absolute limit for the depth of the tree.

The free variables of the formulas are universally quantified: the tableau starts from their universal closures.

It checks if a tableau has all its branches closed. A branch cut by the depth limits counts as not closed, so False means "not refuted within the limits", not "satisfiable".

It Removes the Useless Nodes In Insatisfiable tableau, that are the nodes that don't participates in the way to lograte the unsatifiability.

It represents a FOL Semantic Tableau as a string: a node per line, indented by its depth, with the rule that produced it. Each formula is numbered by its depth in the branch: 5. ¬P(a) % α(4).

It represents a FOL Semantic Tableau as a DOT String renderable by GraphViz. Each formula is numbered by its depth in the branch, and the edges show the rules: α(4), β(4), γ(1){x/a}, δ(3){x/c₁}, ¬¬(2); a closed branch ends in ✕ (the edge ⊥(3,6) names the contradictory formulas), an open one in ◯ and one stopped by the limits in ⓤ.

It represents a FOL Semantic Tableau as a DOT String renderable by GraphViz, with custom styles.