GitHub

Many-Valued Multi-Modal Tableau

The necessary components to reason about many-valued multi-modal logic using an Analytic Tableaux Technique, suitable for both $\alpha$-satisfiability and $\alpha$-validity, i.e., the counterparts of classical (crisp) satisfiability and authomated theorem proving, asking that the evaluation of a formula $\varphi$ has value at least $\alpha$ for one possible model in one possible world (resp, all possible models in all possible worlds). Classical satisfiability and validity are obtained setting $\alpha=1$.

SoleReasoners.ManyValuedMultiModalTableau — Type
abstract type ManyValuedMultiModalTableau <: AbstractTableau end

Tableau to reason about Many-Valued Multi-Modal Logic; a subtype of ManyValuedMultiModalTableau is expected to have at least a judgement, an assertion, a world, a frame, a father, an array of children, and two flags expanded and closed.

source
SoleReasoners.judgement — Method
judgement(t::T) where {T<:ManyValuedMultiModalTableau}

Return the judgement (either true or false) associated with the tableu t.

source
SoleReasoners.world — Method
world(t::T) where {T<:ManyValuedMultiModalTableau}

Return the world associated with a tableu t.

source
SoleReasoners.frame — Method
frame(t::T) where {T<:ManyValuedMultiModalTableau}

Return the frame associated with a tableu t.

source
SoleReasoners.worlds — Method
worlds(
    ::Type{T},
    frame::Union{ManyValuedLinearOrder, NTuple{2, ManyValuedLinearOrder}}
) where {
    T<:ManyValuedMultiModalTableau
}

Return all the worlds in the frame associated with a tableau t.

source
SoleReasoners.newframes — Method
newframes(
::Type{T},
algebra::FiniteFLewAlgebra

) where { T<:ManyValuedMultiModalTableau }

Return all the new possible frames for a tableau of type T.

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

A ManyValuedMultiModalTableau is printed as a decoration Q(α⪯φ,w,F) or Q(φ⪯α,w,F) where Q is a judgement, α⪯φ and φ⪯α are assertions on a world w, and F is a frame represented by either a ManyValuedLinearOrder or a tuple of two ManyValuedLinearOrders.

source

Each many-valued multi-modal logic is associated with a specific tableau structure subtype of ManyValuedMultiModalTableau, and must comprise a judgement, an assertion, a world, a frame, a father, an array of children, and two flags expanded and closed.

Different subtypes of ManyValuedMultiModalTableau usually differ for the type of world and frame, which can be either a ManyValuedLinearOrder or an NTuple{N,ManyValuedLinearOrder}, as well as the recursive fields (i.e., father and children), sharing the same subtype of ManyValuedMultiModalTableau.

All structures will be digested by the same algorithms, parameterized on the subtype of ManyValuedMultiModalTableau.

A tableau for Many-Valued Linear Temporal Logic with Future and Past

SoleReasoners.MVLTLFPTableau — Type
mutable struct MVLTLFPTableau <: ManyValuedMultiModalTableau
    const judgement::Bool
    const assertion::NTuple{2,Formula}
    const world::Point1D
    const frame::ManyValuedLinearOrder
    const father::Union{MVLTLFPTableau,Nothing}
    const children::Vector{MVLTLFPTableau}
    expanded::Bool
    closed::Bool
end

Tableau to reason about Many-Valued Linear Temporal Logic with Future and Past.

source

A tableau for Many-Valued Compass Logic

SoleReasoners.MVCLTableau — Type
mutable struct MVCLTableau <: ManyValuedMultiModalTableau
    const judgement::Bool
    const assertion::NTuple{2,Formula}
    const world::Point2D
    const frame::NTuple{2,ManyValuedLinearOrder}
    const father::Union{MVCLTableau,Nothing}
    const children::Vector{MVCLTableau}
    expanded::Bool
    closed::Bool
end

Tableau to reason about Many-Valued Compass Logic.

source

A tableau for Many-Valued Halpern and Shoham's modal logic of time

SoleReasoners.MVHSTableau — Type
mutable struct MVHSTableau <: ManyValuedMultiModalTableau
    const judgement::Bool
    const assertion::NTuple{2,Formula}
    const world::Interval
    const frame::ManyValuedLinearOrder
    const father::Union{MVHSTableau,Nothing}
    const children::Vector{MVHSTableau}
    expanded::Bool
    closed::Bool
end

Tableau to reason about Many-Valued Halpern and Shoham's modal logic of time intervals.

source

A tableau for Many-Valued Lutz and Wolter's modal logic of topological relations with rectangular areas aligned with the axes

SoleReasoners.MVLRCC8Tableau — Type

Tableau to reason about Many-Valued Lutz and Wolter's modal logic of topological relations with rectangular areas aligned with the axes.

source