Many-Valued Multi-Modal Logic

isaManyValuedLinearOrder(
    mvlt::M,
    mveq::M,
    algebra::FiniteFLewAlgebra
) where {
    N,
    M<:SMatrix{N,N,FiniteTruth}
}

Return true if a domain of cardinality N enriched with two functions mveq and mvlt form a many-valued linear order, i.e., if the following axioms are satisfied:

1. ̃=(x,y) = ⊤ iff x = y
2. ̃=(x,y) = ̃=(y,x)
3. ̃<(x,x) = ⊥
4. ̃<(x,z) ⪰ ̃<(x,y) ⋅ ̃<(y,z)
5. if ̃<(x,y) ≻ 0 and ̃<(y,z) ≻ 0 then ̃<(x,z) ≻ 0
6. if ̃<(x,y) = 0 and ̃<(y,x) = 0 then ̃=(x,y) = 1
7. if ̃=(x,y) ≻ 0 then ̃<(x,y) ≺ 1

Return false otherwise.

checkManyValuedLinearOrder(
    mvlt::M,
    mveq::M,
    algebra::FiniteFLewAlgebra
) where {
    N,
    M<:SMatrix{N,N,FiniteTruth}
}

Check if a domain of cardinality N enriched with two functions mveq and mvlt form a many-valued linear order, i.e., if the following axioms are satisfied:

1. ̃=(x,y) = ⊤ iff x = y
2. ̃=(x,y) = ̃=(y,x)
3. ̃<(x,x) = ⊥
4. ̃<(x,z) ⪰ ̃<(x,y) ⋅ ̃<(y,z)
5. if ̃<(x,y) ≻ 0 and ̃<(y,z) ≻ 0 then ̃<(x,z) ≻ 0
6. if ̃<(x,y) = 0 and ̃<(y,x) = 0 then ̃=(x,y) = 1
7. if ̃=(x,y) ≻ 0 then ̃<(x,y) ≺ 1

struct ManyValuedLinearOrder{N, M<:SMatrix{N,N,FiniteTruth}}
    mvlt::M # ̃<
    mveq::M # ̃=
    algebra::FiniteFLewAlgebra
end

Given an algebra, a many-valued linear order is a structure of the type (D,̃<,̃=) where D is a domain enriched with two functions ̃<, ̃=: D×D→A, for which the following conditions apply for every x, y and z in the domain D:

1. ̃=(x,y) = ⊤ iff x = y
2. ̃=(x,y) = ̃=(y,x)
3. ̃<(x,x) = ⊥
4. ̃<(x,z) ⪰ ̃<(x,y) ⋅ ̃<(y,z)
5. if ̃<(x,y) ≻ 0 and ̃<(y,z) ≻ 0 then ̃<(x,z) ≻ 0
6. if ̃<(x,y) = 0 and ̃<(y,x) = 0 then ̃=(x,y) = 1
7. if ̃=(x,y) ≻ 0 then ̃<(x,y) ≺ 1

cardinality(o::ManyValuedLinearOrder)

Return the cardinality (i.e., number of Point1Ds), in the 'ManyValuedLinearOrder`.

show(io::IO, o::ManyValuedLinearOrder)

A ManyValuedLinearOrder is printed with the tables for the many-valued functions ̃< and ̃= that represent it.

struct Point1D
    index::UInt8
end

A Point1D is represented by its index in a many-valued linear order domain.

show(io::IO, p::Point1D)

A Point1D is printed as xi, where i is its index in the domain associated with the many-valued linear order it belongs to.

mvlt(x1::Point1D, x2::Point1D, o::ManyValuedLinearOrder)

Return the value for the ̃< function between two Point1Ds x1 and x2on the many-valued linear order o.

mvlt(x1::Point1D, x2::Point1D, o::ManyValuedLinearOrder)

Return the value for the ̃= function between two Point1Ds x1 and x2on the many-valued linear order o.

mvleq(x1::Point1D, x2::Point1D, o::ManyValuedLinearOrder)

Return the value for the ̃≤ function between two Point1Ds x1 and x2on the many-valued linear order o (i.e., ̃<(x1,x2) ∨ ̃=(x1,x2)).

function mveval(
    ::typeof(LTLFP_F),
    x1::Point1D,
    x2::Point1D,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function x1Rx2 = ̃<(x1,x2) for relation R=LTLFP_F in many-valued linear order o (how much x2 is in the future w.r.t. x1).

function mveval(
    ::typeof(LTLFP_P),
    x1::Point1D,
    x2::Point1D,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function x1Rx2 = ̃<(x2,x1) for relation R=LTLFP_P in many-valued linear order o (how much x2 is in the past w.r.t. x1).

struct Point2D
    px::Point1D
    py::Point1D
end

A Point2D is represented by a Point1D in a many-valued linear order Dx and another Point1D in a many-valued linear order Dy.

show(io::IO, p::Point2D)

A Point2D is printed as (xi,yj), where i is the index of the Point1D in the domain associated with the many-valued linear order Dx, and j is the index of the Point1D in the domain associated with the many-valued linear order Dy.

function mveval(
    ::typeof(CL_N),
    p1::Point2D,
    p2::Point2D,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function p1Rp2 = ̃=(p1x,p2x)⋅̃<(p1y,p2y) for relation R=CL_N in many-valued linear orders ox and oy (how much p2 is norther than p1).

function mveval(
    ::typeof(CL_S),
    p1::Point2D,
    p2::Point2D,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function p1Rp2 = ̃=(p1x,p2x)⋅̃<(p2y,p1y) for relation R=CL_S in many-valued linear orders ox and oy (how much p2 is souther than p1).

function mveval(
    ::typeof(CL_E),
    p1::Point2D,
    p2::Point2D,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function p1Rp2 = ̃<(p1x,p2x)⋅̃=(p1y,p2y) for relation R=CL_E in many-valued linear orders ox and oy (how much p2 is easter than p1).

function mveval(
    ::typeof(CL_W),
    p1::Point2D,
    p2::Point2D,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function p1Rp2 = ̃<(p2x,p1x)⋅̃=(p1y,p2y) for relation R=CL_W in many-valued linear orders ox and oy (how much p2 is wester than p1).

isaInterval(p1::Point1D, p2::Point1D, o::ManyValuedLinearOrder)

Return true if a two Point1Ds p1 and p1 form an interval in the many-valued linear order o, i.e., ̃<(p1,p2) ≻ ⊥; return false otherwise.

checkInterval(p1::Point1D, p2::Point1D, o::ManyValuedLinearOrder)

Check if a two Point1Ds p1 and p1 form an interval in the many-valued linear order o, i.e., ̃<(p1,p2) ≻ ⊥.

struct Interval
    p1::Point1D
    p1::Point1D
end

An Interval is represented by two Point1Ds in the same many-valued linear order.

show(io::IO, p::Interval)

An Interval is printed as [xi,xj], where i and j are the indexes of the Point1Ds p1 and p2 in the domain associated with the many-valued linear order they belong to.

function mveval(
    ::typeof(HS_A),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃=(i1p2,i2p1) for relation R=HS_A in many-valued linear order o (how much i2 is after i1).

function mveval(
    ::typeof(HS_L),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i1p2,i2p1) for relation R=HS_L in many-valued linear order o (how much i2 is later than i1).

function mveval(
    ::typeof(HS_B),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃=(i1p1,i2p1) ⋅ ̃<(i2p2,i1p2) for relation R=HS_B in many-valued linear order o (how much i2 is at the begin of i1).

function mveval(
    ::typeof(HS_E),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i1p1,i2p1) ⋅ ̃=(i1p2,i2p2) for relation R=HS_E in many-valued linear order o (how much i2 is at the end of i1).

function mveval(
    ::typeof(HS_D),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i1p1,i2p1) ⋅ ̃<(i2p2,i1p2) for relation R=HS_D in many-valued linear order o (how much i2 is during i1).

function mveval(
    ::typeof(HS_O),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i1p1,i2p1) ⋅ ̃<(i2p1,i1p2) ⋅ ̃<(i1p2, i2p2) for relation R=HS_O in many-valued linear order o (how much i2 is overlapping i1).

function mveval(
    ::typeof(HS_Ai),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃=(i2p2,i1p1) for relation R=HS_Ai in many-valued linear order o (how much i1 is after i2).

function mveval(
    ::typeof(HS_Li),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i2p2,i1p1) for relation R=HS_Li in many-valued linear order o (how much i1 is later than i2).

function mveval(
    ::typeof(HS_Bi),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃=(i1p1,i2p1) ⋅ ̃<(i1p2,i2p2) for relation R=HS_Bi in many-valued linear order o (how much i1 is at the begin of i2).

function mveval(
    ::typeof(HS_Ei),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i2p1,i1p1) ⋅ ̃=(i1p2,i2p2) for relation R=HS_Ei in many-valued linear order o (how much i1 is at the end of i2).

function mveval(
    ::typeof(HS_Di),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i2p1,i1p1) ⋅ ̃<(i1p2,i2p2) for relation R=HS_Di in many-valued linear order o (how much i1 is during i2).

function mveval(
    ::typeof(HS_Oi),
    i1::Interval,
    i2::Interval,
    o::ManyValuedLinearOrder
)

Many-valued evaluation function i1Ri2 = ̃<(i2p1,i1p1) ⋅ ̃<(i1p1,i2p2) ⋅ ̃<(i2p2, i1p2) for relation R=HS_Oi in many-valued linear order o (how much i1 is overlapping i2).

struct Rectangle
    ix::Interval
    iy::Interval
end

A Rectangle is represented by an Interval on a many-valued linear order Dx and another Interval on a many-valued linear order Dy.

A Rectangle is printed as ([xi,xj],[yk,yl]), where i and j are the indexes of the Point1Ds of the first Interval in the domain associated with the many-valued linear order Dx and k and l are the indexes of the Point1Ds of the second Interval in the domain associated with the many-valued linear order Dy.

function mveval(
    ::typeof(LRCC8_Rec_DC),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecDC in many-valued linear orders ox and oy (how much r2 is disconnected from r1).

function mveval(
    ::typeof(LRCC8_Rec_EC),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecEC in many-valued linear orders ox and oy (how much r2 is externally connected with r1).

function mveval(
    ::typeof(LRCC8_Rec_PO),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecPO in many-valued linear orders ox and oy (how much r2 is partially overlapping with r1).

function mveval(
    ::typeof(LRCC8_Rec_TPP),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecTPP in many-valued linear orders ox and oy (how much r2 is a tangential proper part of r1).

function mveval(
    ::typeof(LRCC8_Rec_NTPP),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecNTPP in many-valued linear orders ox and oy (how much r2 is a non-tangential proper part of r1).

function mveval(
    ::typeof(LRCC8_Rec_TPPi),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecTPPi in many-valued linear orders ox and oy (how much r1 is a tangential proper part of r2).

function mveval(
    ::typeof(LRCC8_Rec_NTPPi),
    r1::Rectangle,
    r2::Rectangle,
    (ox,oy)::NTuple{2,ManyValuedLinearOrder}
)

Many-valued evaluation function r1Rr2 for relation R=LRCC8RecNTPPi in many-valued linear orders ox and oy (how much r1 is a non-tangential proper part of r2).