GitHub

Abstract Tableau

All tableaux structures are recursive structures resembling a tree structure. Each logic is associated with a specific tableau structure subtype of AbstractTableau, and must comprise at least a father, an array of children, and two flags expanded and closed.

SoleReasoners.AbstractTableau — Type
abstract type AbstractTableau end

Abstract type for all tableaux structures.

All tableaux structures are recursive structures resembling a tree structure. Each subtype T where T<:AbstractTableau is expected to have at least a field faher of the same type T (or Nothing in case it is the root), a field children comprising a vector of elements of type T, and two flags expanded and closed of type Bool claiming if the node has been expanded (resp. closed) or not.

source
SoleReasoners.expanded — Method
expanded(t::T) where {T<:AbstractTableau}

Return true if a tableu t has already been expanded, false otherwise.

source
SoleReasoners.closed — Method
closed(t::T) where {T<:AbstractTableau}

Return true if a tableu t has already been closed, false otherwise.

source
SoleReasoners.isroot — Method
isroot(t::T) where {T<:AbstractTableau}

Return true if a tableu t is the root of the tableau, false otherwise.

source
SoleReasoners.isleaf — Method
isleaf(t::T) where {T<:AbstractTableau}

Return true if a tableu t is a leaf of the tableau, false otherwise.

source
SoleReasoners.close! — Method
close!(t::T) where {T<:AbstractTableau}

Set the closed flag of t to true and recursevely close all its descendants; if t is not the root of the tableau, also remove it from the list of children of its father and if t does not have any simblings recursevely close it.

source
SoleReasoners.pushchild! — Method
pushchild!(father::T, child::T) where {T<:AbstractTableau}

Push new child tableau to the children of father tableau.

source
Base.show — Method
show(io::IO, _::T) where {T<:AbstractTableau}

Method to be overwritten with the signature of a specific tableaux structure.

source