GitHub

SoleData

Welcome to the documentation for SoleData.

Logical foundations

Here are some core concepts for symbolic artificial intelligence with propositional and modal logics.o

SoleLogics.AbstractWorld — Type
abstract type AbstractWorld end

Abstract type for the nodes of an annotated accessibility graph (Kripke structure). This is used, for example, in modal logic, where the truth of formulas is relativized to worlds, that is, nodes of a graph.

Implementing

When implementing a new world type, the logical semantics should be defined via accessibles methods; refer to the help for accessibles.

See also AbstractKripkeStructure, AbstractFrame.

source
SoleLogics.Interval — Type
struct Interval{T<:Real} <: GeometricalWorld
    x :: T
    y :: T
end

An interval in a 1-dimensional space, with coordinates of type T.

Examples

julia> SoleLogics.goeswithdim(SoleLogics.Interval(1,2),1)
true

julia> SoleLogics.goeswithdim(SoleLogics.Interval(1,2),2)
false

julia> collect(accessibles(SoleLogics.FullDimensionalFrame(5), Interval(1,2), SoleLogics.IA_L))
6-element Vector{Interval{Int64}}:
 (3−4)
 (3−5)
 (4−5)
 (3−6)
 (4−6)
 (5−6)

See also goeswithdim, accessibles, FullDimensionalFrame, Point, Interval2D, GeometricalWorld, AbstractWorld.

source
SoleLogics.Interval2D — Type
struct Interval2D{T<:Real} <: GeometricalWorld
    x :: Interval{T}
    y :: Interval{T}
end

A orthogonal rectangle in a 2-dimensional space, with coordinates of type T. This is the 2-dimensional Interval counterpart, that is, the combination of two orthogonal Intervals.

Examples

julia> SoleLogics.goeswithdim(SoleLogics.Interval2D((1,2),(3,4)),1)
false

julia> SoleLogics.goeswithdim(SoleLogics.Interval2D((1,2),(3,4)),2)
true

julia> collect(accessibles(SoleLogics.FullDimensionalFrame(5,5), Interval2D((2,3),(2,4)), SoleLogics.IA_LL))
3-element Vector{Interval2D{Int64}}:
 ((4−5)×(5−6))
 ((4−6)×(5−6))
 ((5−6)×(5−6))

See also goeswithdim, accessibles, FullDimensionalFrame, Point, Interval, GeometricalWorld, AbstractWorld.

source
SoleLogics.syntaxstring — Function
syntaxstring(s::Syntactical; kwargs...)::String

Return the string representation of any syntactic object (e.g., Formula, SyntaxTree, SyntaxToken, Atom, Truth, etc). Note that this representation may introduce redundant parentheses. kwargs can be used to specify how to display syntax tokens/trees under some specific conditions.

The following kwargs are currently supported:

  • function_notation = false::Bool: when set to true, it forces the use of function notation for binary operators (see here).
  • remove_redundant_parentheses = true::Bool: when set to false, it prints a syntaxstring where each syntactical element is wrapped in parentheses.
  • parenthesize_atoms = !remove_redundant_parentheses::Bool: when set to true, it forces the atoms (which are the leaves of a formula's tree structure) to be wrapped in parentheses.

Examples

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"))
"p ∧ q ∧ r ∧ s ∧ t"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), function_notation=true)
"∧(∧(∧(∧(p, q), r), s), t)"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), remove_redundant_parentheses=false)
"((((p) ∧ (q)) ∧ (r)) ∧ (s)) ∧ (t)"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), remove_redundant_parentheses=true, parenthesize_atoms=true)
"(p) ∧ (q) ∧ (r) ∧ (s) ∧ (t)"

julia> syntaxstring(parseformula("◊((p∧s)→q)"))
"◊((p ∧ s) → q)"

julia> syntaxstring(parseformula("◊((p∧s)→q)"); function_notation = true)
"◊(→(∧(p, s), q))"

See also parseformula, SyntaxBranch, SyntaxToken.

Implementation

In the case of a syntax tree, syntaxstring is a recursive function that calls itself on the syntax children of each node. For a correct functioning, the syntaxstring must be defined (including the kwargs... part!) for every newly defined SyntaxToken (e.g., SyntaxLeafs, that is, Atoms and Truth values, and Operators), in a way that it produces a unique string representation, since Base.hash and Base.isequal, at least for SyntaxTrees, rely on it.

In particular, for the case of Atoms, the function calls itself on the wrapped value:

syntaxstring(a::Atom; kwargs...) = syntaxstring(value(a); kwargs...)

The syntaxstring for any value defaults to its string representation, but it can be defined by defining the appropriate syntaxstring method.

Warning

The syntaxstring for syntax tokens (e.g., atoms, operators) should not be prefixed/suffixed by whitespaces, as this may cause ambiguities upon parsing. For similar reasons, syntaxstrings should not contain parentheses ('(', ')'), and, when parsing in function notation, commas (',').

See also SyntaxLeaf, Operator, parseformula.

source
SoleLogics.accessibles — Function
accessibles(fr::AbstractUniModalFrame{W}, w::W)::Worlds{W} where {W<:AbstractWorld}

Return the worlds in frame fr that are accessible from world w.

See also AbstractWorld, AbstractUniModalFrame.

source
accessibles(
    fr::AbstractMultiModalFrame{W},
    w::W,
    r::AbstractRelation
) where {W<:AbstractWorld}

Return the worlds in frame fr that are accessible from world w via relation r.

Examples

julia> fr = SoleLogics.FullDimensionalFrame((10,), Interval{Int});

julia> typeof(accessibles(fr, Interval(2,5), IA_L))
Base.Generator{...}

julia> typeof(accessibles(fr, globalrel))
Base.Generator{...}

julia> @assert SoleLogics.nworlds(fr) == length(collect(accessibles(fr, globalrel)))

julia> typeof(accessibles(fr, Interval(2,5), identityrel))
Vector{Interval{Int64}}

julia> Interval(8,11) in collect(accessibles(fr, Interval(2,5), IA_L))
true

Implementation

Since accessibles always returns an iterator to worlds of the same type W, the current implementation of accessibles for multi-modal frames delegates the enumeration to a lower level _accessibles function, which returns an iterator to parameter tuples that are, then, fed to the world constructor the using IterTools generators, as in:

function accessibles(
    fr::AbstractMultiModalFrame{W},
    w::W,
    r::AbstractRelation,
) where {W<:AbstractWorld}
    IterTools.imap(W, _accessibles(fr, w, r))
end

As such, when defining new frames, worlds, and/or relations, one should provide new methods for _accessibles. For example:

_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_A) = zip(Iterators.repeated(w.y), w.y+1:X(fr)+1)

This pattern is generally convenient; it can, however, be bypassed, although this requires defining two additional methods in order to resolve dispatch ambiguities. When defining a new frame type FR{W}, one can resolve the ambiguities and define a custom accessibles method by providing these three methods:

# access worlds through relation `r`
function accessibles(
    fr::FR{W},
    w::W,
    r::AbstractRelation,
) where {W<:AbstractWorld}
    ...
end

# access current world
function accessibles(
    fr::FR{W},
    w::W,
    r::IdentityRel,
) where {W<:AbstractWorld}
    [w]
end

# access all worlds
function accessibles(
    fr::FR{W},
    w::W,
    r::GlobalRel,
) where {W<:AbstractWorld}
    allworlds(fr)
end

In general, it should be true that collect(accessibles(fr, w, r)) isa AbstractWorlds{W}.

See also AbstractWorld, AbstractRelation, AbstractMultiModalFrame.

source
SoleData.minify — Function
minify(dataset::D1)::Tuple{D2,Function} where {D1,D2}

Return a minified version of a dataset, as well as a backmap for reverting to the original dataset. Dataset minification remaps each scalar values in the dataset to a new value such that the overall order of the values is preserved; the output dataset is smaller in size, since it relies on values of type UInt8, UInt16, UInt32, etc.

See also isminifiable.

source

See SoleLogics for more.

API

Ontop of the logical layer, we define features, conditions on features, logisets, and memosets.

SoleData.parsefeature — Method
parsefeature(FT::Type{<:AbstractFeature}, expr::AbstractString; kwargs...)

Parse a feature of type FT from its syntaxstring representation. Depending on FT, specifying keyword arguments such as featvaltype::Type may be required or recommended.

See also parsecondition.

source
SoleData.checkcondition — Method
checkcondition(c::AbstractCondition, args...; kwargs...)

Check a condition (e.g., on a world of a logiset instance).

This function must be implemented for each subtype of AbstractCondition.

Examples

# Checking a condition on a logiset created from a DataFrame
using SoleData, DataFrames

# Load the iris dataset
iris_df = DataFrame(load_iris());

# Convert the DataFrame to a logiset
iris_logiset = scalarlogiset(iris_df);

# Create a ScalarCondition
condition = ScalarCondition(:sepal_length, >, 5.0);

# Check the condition on the logiset
@assert checkcondition(condition, iris_logiset, 1) == true
source
SoleData.parsecondition — Method
parsecondition(C::Type{<:AbstractCondition}, expr::AbstractString; kwargs...)

Parse a condition of type C from its syntaxstring representation. Depending on C, specifying keyword arguments such as featuretype::Type{<:AbstractFeature}, and featvaltype::Type may be required or recommended.

See also parsefeature.

source
SoleData.AbstractModalLogiset — Type
abstract type AbstractModalLogiset{
    W<:AbstractWorld,
    U,
    FT<:AbstractFeature,
    FR<:AbstractFrame{W},
} <: AbstractLogiset end

Abstract type for logisets, that is, logical datasets for symbolic learning where each instance is a Kripke structure associating feature values to each world. Conditions (see AbstractCondition), and logical formulas with conditional letters can be checked on worlds of instances of the dataset.

Interface

  • readfeature(X::AbstractModalLogiset, featchannel::Any, w::W, feature::AbstractFeature)
  • featchannel(X::AbstractModalLogiset, i_instance::Integer, feature::AbstractFeature)
  • featvalue(feature::AbstractFeature, X::AbstractModalLogiset, i_instance::Integer, args...; kwargs...)
  • featvalue!(feature::AbstractFeature, X::AbstractModalLogiset{W}, featval, i_instance::Integer, w::W)
  • featvalues!(feature::AbstractFeature, X::AbstractModalLogiset{W}, featslice)
  • frametype(X::AbstractModalLogiset)
  • worldtype(X::AbstractModalLogiset)

See also AbstractCondition, AbstractFeature, SoleLogics.AbstractKripkeStructure, SoleLogics.AbstractInterpretationSet.

source

Utilities

Logisets

SoleData.Feature — Type
struct Feature{A} <: AbstractFeature
    atom::A
end

A feature solely identified by an atom (e.g., a string with its name, a tuple of strings, etc.)

See also AbstractFeature.

source
SoleData.ExplicitBooleanModalLogiset — Type
struct ExplicitBooleanModalLogiset{
    W<:AbstractWorld,
    FT<:AbstractFeature,
    FR<:AbstractFrame{W},
} <: AbstractModalLogiset{W,Bool,FT,FR}

    d :: Vector{Tuple{Dict{W,Vector{FT}},FR}}

end

A logiset where the features are boolean, and where each instance associates to each world the set of features with true.

See also AbstractModalLogiset.

source
SoleData.ExplicitModalLogiset — Type
struct ExplicitModalLogiset{
    W<:AbstractWorld,
    U,
    FT<:AbstractFeature,
    FR<:AbstractFrame{W},
} <: AbstractModalLogiset{W,U,FT,FR}

    d :: Vector{Tuple{Dict{W,Dict{FT,U}},FR}}

end

A logiset where the features are boolean, and where each instance associates to each world the set of features with true.

See also AbstractModalLogiset.

source
SoleData.ScalarOneStepMemoset — Type

One-step memoization structures for optimized check of formulas of type ⟨R⟩p, where p wraps a scalar condition, such as MyFeature ≥ 10. With such formulas, scalar one-step optimization can be performed.

For example, checking ⟨R⟩(MyFeature ≥ 10) on a world w of a Kripke structure involves comparing the maximum MyFeature across ws accessible worlds with 10; but the same maximum value can be reused to check sibling formulas such as ⟨R⟩(MyFeature ≥ 100). This sparks the idea of storing and reusing scalar aggregations (e.g., minimum/maximum) over the feature values. Each value refers to a specific world, and an object of type ⟨R⟩(f ⋈ ?), called a "scalar metacondition".

Similar cases arise depending on the relation and the test operator (or, better, its aggregator), and further optimizations can be applied for specific feature types (see representatives).

An immediate special case, however, arises when R is the global relation G since, in such case, a single aggregate value is enough for all worlds within the Kripke structure. Therefore, we differentiate between generic, relational memosets (see AbstractScalarOneStepRelationalMemoset), and global memosets (see AbstractScalarOneStepGlobalMemoset), which are usually much smaller.

Given a logiset X, a ScalarOneStepMemoset covers a set of relations and metaconditions, and it holds both a relational and a global memoset. It can be instantiated via:

ScalarOneStepMemoset(
    X                       :: AbstractModalLogiset{W,U},
    metaconditions          :: AbstractVector{<:ScalarMetaCondition},
    relations               :: AbstractVector{<:AbstractRelation};
    precompute_globmemoset  :: Bool = true,
    precompute_relmemoset   :: Bool = false,
    print_progress          :: Bool = false,
)

If precompute_relmemoset is false, then the relational memoset is simply initialized as an empty structure, and memoization is performed on it upon checking formulas. precompute_globmemoset works similarly.

See SupportedLogiset, ScalarMetaCondition, AbstractOneStepMemoset.

source
SoleLogics.check — Method
check(
    φ::SoleLogics.SyntaxTree,
    i::SoleLogics.LogicalInstance{<:AbstractModalLogiset{W,<:U}},
    w::Union{Nothing,AnyWorld,<:AbstractWorld} = nothing;
    kwargs...
)::Bool

Check whether a formula φ holds for a given instance i_instance of a logiset X, on a world w. Note that the world can be elided for grounded formulas (see isgrounded).

This implementation recursively evaluates the subformulas of φ and use memoization to store the results using Emerson-Clarke algorithm. The memoization structure is either the one stored in X itself (if X supports memoization) or a structure passed as the use_memo argument. If X supports onestep memoization, then it will be used for specific diamond formulas, up to an height equal to a keyword argument memo_max_height.

Arguments

  • φ::SoleLogics.SyntaxTree: the formula to check.
  • i::SoleLogics.LogicalInstance{<:AbstractModalLogiset{W,<:U}}: the instance of the logiset to check in.
  • w::Union{Nothing,AnyWorld,<:AbstractWorld} = nothing: the world to check in. If nothing, the method checks in all worlds of the instance.

Keyword arguments

  • use_memo::Union{Nothing,AbstractMemoset{<:AbstractWorld},AbstractVector{<:AbstractDict{<:FT,<:AbstractWorlds}}} = nothing: the memoization structure to use. If nothing, the method uses the one stored in X if X supports memoization. If AbstractMemoset, the method uses the i_instance-th element of the memoization structure. If AbstractVector, the method uses the i_instance-th element of the vector.
  • perform_normalization::Bool = true: whether to normalize the formula before checking it.
  • memo_max_height::Union{Nothing,Int} = nothing: the maximum height up to which onestep memoization should be used. If nothing, the method does not use onestep memoization.
  • onestep_memoset_is_complete = false: whether the onestep memoization structure is complete (i.e. it contains all possible values of the metaconditions in the structure).
source

Scalar Logisets

SoleData.@scalarformula — Macro
@scalarformula expr

Parse a logical formula on scalar conditions, such as V1 > 10. Note that logical operators take precedence over comparison operators, so it is often the case that expressions such as V1 > 10 must be wrapped in parentheses.

Examples

julia> φ = @scalarformula ((V1 > 10) ∧ (V2 < 0) ∧ (V2 < 0) ∧ (V2 <= 0)) ∨ ((V1 <= 0) ∧ ((V1 <= 3)) ∧ (V2 >= 2))
SyntaxBranch: (V1 > 10 ∧ V2 < 0 ∧ V2 < 0 ∧ V2 ≤ 0) ∨ (V1 ≤ 0 ∧ V1 ≤ 3 ∧ V2 ≥ 2)

See also parseformula, syntaxstring.

source
SoleData.MultivariateFeature — Type
struct MultivariateFeature{U} <: VarFeature
    f::Function
end

A dimensional feature represented by the application of a function to a dimensional channel. For example, it can wrap a scalar function computing how much a Interval2D world, when interpreted on an image, resembles a horse. Note that the image has a number of spatial variables (3, for the case of RGB), and "resembling a horse" may require a computation involving all variables.

See also SoleLogics.Interval, SoleLogics.Interval2D, AbstractUnivariateFeature, VarFeature, AbstractFeature.

source
SoleData.UnivariateFeature — Type
struct UnivariateFeature{U,I<:VariableId} <: AbstractUnivariateFeature
    i_variable::I
    f::Function
    fname::Union{Nothing,String}
end

A dimensional feature represented by the application of a generic function f to a single variable of a dimensional channel. For example, it can wrap a scalar function computing how much red a Interval2D world, when interpreted on an image, contains. Optionally, a feature name fname can be attached to the function, which can be useful for inspection (e.g., if f is an anonymous function, this avoids names such s "#47" or "#49".

See also SoleLogics.Interval, SoleLogics.Interval2D, AbstractUnivariateFeature, VarFeature, AbstractFeature.

source
SoleData.VarFeature — Type
abstract type VarFeature <: AbstractFeature end

Abstract type for feature functions that can be computed on (multi)variate data. Instances of multivariate datasets have values for a number of variables, which can be used to define logical features.

For example, with dimensional data (e.g., multivariate time series, digital images and videos), features can be computed as the minimum value for a given variable on a specific interval/rectangle/cuboid (in general, a SoleLogics.GeometricalWorld).

As an example of a dimensional feature, consider min[V1], which computes the minimum for variable 1 for a given world. ScalarConditions such as min[V1] >= 10 can be, then, evaluated on worlds.

See also scalarlogiset, featvaltype, computefeature, SoleLogics.Interval.

source
SoleData.VariableDistance — Type
struct VariableDistance{I<:VariableId,T} <: AbstractUnivariateFeature
    i_variable::I
    reference::T
    distance::Function
    featurename::Union{String,Symbol}
end

Univariate feature computing a distance function for a given variable, with respect to a certain reference structure.

By default, distance is set to be Euclidean distance.

Examples

julia> vd = VariableDistance(1, [1,2,3,4]; featurename="StrictMonotonicAscending");

julia> syntaxstring(vd)
"StrictMonotonicAscending[V1]"

julia> computeunivariatefeature(vd, [1,2,3,4])
0.0

julia> computeunivariatefeature(vd, [2,3,4,5])
2.0

See also SoleLogics.Interval, SoleLogics.Interval2D, AbstractUnivariateFeature, VariableMax, VariableMin, VarFeature, AbstractFeature.

source
SoleData.parsefeature — Method
parsefeature(FT::Type{<:VarFeature}, expr::AbstractString; kwargs...)

Parse a VarFeature of type FT from its syntaxstring representation.

Keyword Arguments

  • featvaltype::Union{Nothing,Type} = nothing: the feature's featvaltype (recommended for some features, e.g., UnivariateFeature);
  • opening_parenthesis::String = "[": the string signaling the opening of an expression block (e.g., "min[V2]");
  • closing_parenthesis::String = "]": the string signaling the closing of an expression block (e.g., "min[V2]");
  • additional_feature_aliases = Dict{String,Base.Callable}(): A dictionary mapping strings to callables, useful when parsing custom-made, non-standard features. By default, features such as "avg" or "min" are provided for (see SoleData.BASE_FEATURE_FUNCTIONS_ALIASES); note that, in case of clashing strings, the provided additional aliases will override the standard ones;
  • variable_names_map::Union{Nothing,AbstractDict,AbstractVector} = nothing: mapping from variable name to variable index, useful when parsing from syntaxstrings with variable names (e.g., "min[Heart rate]");
  • variable_name_prefix::String = "V": prefix used with variable indices (e.g., "V10").

Note that at most one argument in variable_names_map and variable_name_prefix should be provided.

Note

The default parentheses, here, differ from those of SoleLogics.parseformula, since features are typically wrapped into Atoms, and parseformula does not allow parenthesis characters in atoms' syntaxstrings.

See also VarFeature, featvaltype, parsecondition.

source
SoleData.variable_name — Method
variable_name(
    f::AbstractUnivariateFeature;
    variable_names_map::Union{Nothing,AbstractDict,AbstractVector} = nothing,
    variable_name_prefix::Union{Nothing,String} = "V",
)::String

Return the name of the variable targeted by a univariate feature. By default, an variable name is a number prefixed by "V"; however, variable_names_map or variable_name_prefix can be used to customize variable names. The prefix can be customized by specifying variable_name_prefix. Alternatively, a mapping from string to integer (either via a Dictionary or a Vector) can be passed as variable_names_map. Note that only one in variable_names_map and variable_name_prefix should be provided.

See also parsecondition, ScalarCondition, syntaxstring.

source
SoleData.TestOperator — Type
const TestOperator = Function

A test operator is a binary Julia Function used for comparing a feature value and a threshold. In a crisp (i.e., boolean, non-fuzzy) setting, the test operator returns a Boolean value, and <, >, ≥, ≤, !=, and == are typically used.

See also Aggregator, ScalarCondition.

source
SoleData.RangeScalarCondition — Type
struct RangeScalarCondition{U<:Number,FT<:AbstractFeature} <: AbstractScalarCondition{FT}

A condition specifying a range of values for a scalar feature.

Fields:

  • feature: the scalar feature
  • minval, maxval: the minimum and maximum values of the range
  • minincluded, maxincluded: whether to include the minimum and maximum values in the range, respectively

The range is specified using interval notation, where the minimum value is included if minincluded is true and excluded if it is false. Similarly, the maximum value is included if maxincluded is true and excluded if it is false.

For example, if minincluded == true and maxincluded == false, the range is [minval, maxval).

The checkcondition method checks whether the value of the feature is within the specified range.

The syntaxstring method returns a string representation of the condition in the form feature ∈ [minval, maxval], where the interval notation is used to indicate whether the minimum and maximum values are included or excluded.

source
SoleData.ScalarCondition — Type
struct ScalarCondition{U,FT<:AbstractFeature,M<:ScalarMetaCondition{FT}} <: AbstractScalarCondition{FT}
    metacond::M
    a::U
end

A scalar condition comparing a computed feature value (see ScalarMetaCondition) and a threshold value a. It can be evaluated on a world of an instance of a logical dataset.

For example: $min[V1] ≥ 10$, which translates to "Within this world, the minimum of variable 1 is greater or equal than 10." In this case, the feature a VariableMin object.

See also AbstractScalarCondition, ScalarMetaCondition.

source
SoleData.ScalarMetaCondition — Type
struct ScalarMetaCondition{FT<:AbstractFeature,O<:TestOperator} <: AbstractScalarCondition{FT}
    feature::FT
    test_operator::O
end

A metacondition representing a scalar comparison method. Here, the feature is a scalar function that can be computed on a world of an instance of a logical dataset. A test operator is a binary mathematical relation, comparing the computed feature value and an external threshold value (see ScalarCondition). A metacondition can also be used for representing the infinite set of conditions that arise with a free threshold (see UnboundedScalarAlphabet): ${min[V1] ≥ a, a ∈ ℝ}$.

See also AbstractScalarCondition, ScalarCondition.

source
SoleData.islogiseed — Method
islogiseed(dataset)::Bool

A logiseed is a dataset that can be converted to a logiset (e.g., via scalarlogiset). If the dataset is a unimodal logiseed, the following methods should be defined:

    islogiseed(::typeof(dataset)) = true
    initlogiset(dataset, features; kwargs...)
    ninstances(dataset)
    nvariables(dataset)
    frame(dataset, i_instance::Integer)
    featvalue(feature::VarFeature, dataset, i_instance::Integer, w::AbstractWorld)
    varnames(dataset)::Union{Nothing,Vector{<:Union{Integer, Symbol}}}
    vareltype(dataset, i_variable::Union{Integer, Symbol})

If dataset is a multimodal logiseed, the following methods should be defined, while its modalities (iterated via eachmodality) should provide the methods above:

    ismultilogiseed(::typeof(dataset)) = true
    nmodalities(logiseed)
    eachmodality(logiseed)

Examples

A DataFrame

julia> using DataFrames; df = DataFrame(rand(150, 4), :auto);


julia> SoleData.islogiseed(df)
true

julia> ninstances(df), nvariables(df)
(150, 4)

julia> SoleData.varnames(df)
4-element Vector{String}:
 "x1"
 "x2"
 "x3"
 "x4"

A Vector of multidimensional instances (i.e., instances that are Array{Number,N} with N ≥ 1, where the last dimension is that of variables)

julia> X = [rand(4) for i in 1:150];


julia> SoleData.islogiseed(X)
true

julia> ninstances(X), nvariables(X)
(150, 4)

julia> SoleData.varnames(X)
nothing

See also AbstractLogiset, scalarlogiset.

source
SoleData.naturalgrouping — Method
naturalgrouping(
    X::AbstractDataFrame;
    allow_variable_drop = false,
)::AbstractVector{<:AbstractVector{<:Symbol}}

Return variables grouped by their logical nature; the nature of a variable is automatically derived from its type (e.g., Real, Vector{<:Real} or Matrix{<:Real}) and frame. All instances must have the same frame (e.g., channel size/number of worlds).

source
SoleData.scalaralphabet — Method
scalaralphabet(a::AbstractAlphabet{<:ScalarCondition}, args...; kwargs...)

TODO explain args and kwargs...

  • sorted: whether to sort the atoms in the sub-alphabets (i.e., the threshold domains), by a truer-first policy (default: true)
  • test_operators: test operators to use (defaulted to [≤, ≥] for real-valued features, and [(==), (≠)] for other features, e.g., categorical)

Return a MultivariateScalarAlphabet from an alphabet of ScalarCondition's.

source
SoleData.scalarlogiset — Function
scalarlogiset(dataset, features; kwargs...)

Convert a dataset structure (with variables) to a logiset with scalar-valued features. Refer to islogiseed for the interface that dataset must adhere to.

Arguments

  • dataset: the dataset that will be transformed into a logiset. It should adhere to the islogiseed interface;
  • features: vector of features, corresponding to dataset columns;

Keyword Arguments

  • use_onestep_memoization::Union{Bool,Type{<:AbstractOneStepMemoset}}=!isnothing(conditions) && !isnothing(relations):

enable one-step memoization, optimizing the checking of specific, short formulas using specific scalar conditions and relations (see AbstractOneStepMemoset);

  • conditions::Union{Nothing,AbstractVector{<:AbstractCondition}}=nothing:

a set of conditions or metaconditions to be used in one-step memoization. If not provided, metaconditions given by minimum and maximum applied to each variable will be used (see ScalarMetaCondition);

  • relations::Union{Nothing,AbstractVector{<:AbstractRelation}}=nothing:

a set of relations to be used in one-step memoization (see AbstractRelation);

  • onestep_precompute_globmemoset::Bool = (use_onestep_memoization != false):

precompute the memoization set for global one-step formulas. This usually takes little time: in facto, because, global formulas are grounded, the intermediate check result does not depend on the number of worlds.

  • onestep_precompute_relmemoset::Bool = false:

precompute the memoization set for global one-step formulas. This may take a long time, depending on the relations and the number of worlds; it is usually not needed.

  • use_full_memoization::Union{Bool,Type{<:Union{AbstractOneStepMemoset,AbstractFullMemoset}}}=true:

enable full memoization, where every intermediate check result is cached to avoid recomputing. This can be used in conjunction with one-step memoization;

  • print_progress::Bool = false: print a progress bar;
  • allow_propositional::Bool = false: allows a tabular (i.e, non-relational) dataset to be instantiated as a PropositionalLogiset, instead of a modal logiset;
  • force_i_variables::Bool = false: when conditions are to be inferred (conditions = nothing), force (meta)conditions to refer to variables by their integer index, instead of their Symbol name (when available through varnames, see islogiseed).

Logiseed-specific Keyword Arguments

  • worldtype_by_dim::AbstractDict{<:Integer,<:Type} = Dict([0 => OneWorld, 1 => Interval, 2 => Interval2D]):

When the dataset is a MultiData.AbstractDimensionalDataset, this map between the dimensionality and the desired AbstractWorld type is used to infer the frame type. By default, dimensional datasets of dimensionalities 0, 1 and 2 will generate logisets based on OneWorld, Interval's, and Interval2D's, respectively.

Examples

julia> df = DataFrame(A = [36, 37, 38], B = [1, 2, 3])
3×2 DataFrame
 Row │ A      B
     │ Int64  Int64
─────┼──────────────
   1 │    36      1
   2 │    37      2
   3 │    38      3

julia> scalarlogiset(df; worldtype_by_dim=([0=>OneWorld]))
SupportedLogiset with 1 support (2.21 KBs)
├ worldtype:                   OneWorld
├ featvaltype:                 Int64
├ featuretype:                 VariableValue
├ frametype:                   SoleLogics.FullDimensionalFrame{0, OneWorld}
├ # instances:                 3
├ usesfullmemo:                true
├[BASE] UniformFullDimensionalLogiset of dimensionality 0 (688.0 Bytes)
│ ├ size × eltype:              (3, 2) × Int64
│ └ features:                   2 -> VariableValue[V1, V2]
└[SUPPORT 1] FullMemoset (0 memoized values, 1.5 KBs))

julia> pointlogiset = scalarlogiset( Xdf; worldtypeby_dim=Dict([1 => SoleLogics.Point1D, 2 => SoleLogics.Point2D]) )

See also AbstractModalLogiset, AbstractOneStepMemoset, SoleLogics.AbstractRelation, SoleLogics.AbstractWorld, ScalarCondition, VarFeature.

source
SoleData.PropositionalLogiset — Type
PropositionalLogiset(table) <: AbstractPropositionalLogiset

A logiset of propositional interpretations, wrapping a Tables' table of real/string/categorical values.

Examples

This structure can be used to check propositional formulas:

using SoleData, MLJBase

X = PropositionalLogiset(MLJBase.load_iris())

φ = parseformula(
    "sepal_length > 5.8 ∧ sepal_width < 3.0 ∨ target == "setosa"";
    atom_parser = a->Atom(parsecondition(SoleData.ScalarCondition, a; featuretype = SoleData.VariableValue))
)

check(φ, X, 10) # Check the formula on a single instance

satmask = check(φ, X) # Check the formula on the whole dataset

slicedataset(X, satmask)
slicedataset(X, (!).(satmask))

See also AbstractLogiset, AbstractAssignment.

source
SoleLogics.alphabet — Function
alphabet(
    X::PropositionalLogiset,
    sorted=true;
    test_operators::Union{Nothing,AbstractVector{<:TestOperator},Base.Callable}=nothing,
    discretizedomain=false,
    y::Union{Nothing, AbstractVector}=nothing,
)::MultivariateScalarAlphabet

Constructs an alphabet based on the provided PropositionalLogiset X, with optional parameters:

  • sorted: whether to sort the atoms in the sub-alphabets (i.e., the threshold domains), by a truer-first policy (default: true)
  • test_operators: test operators to use (defaulted to [≤, ≥] for real-valued features, and [(==), (≠)] for other features, e.g., categorical)
  • discretizedomain: whether to discretize the domain (default: false)
  • y: vector used for discretization (required if discretizedomain is true)

Returns a UnionAlphabet containing ScalarCondition and UnivariateScalarAlphabet.

source

Scalar Dimensional Logisets

SoleData.DimensionalDatasets.UniformFullDimensionalLogiset — Type
struct UniformFullDimensionalLogiset{
    U,
    W<:AbstractWorld,
    N,
    D<:AbstractArray{U},
    FT<:AbstractFeature,
    FR<:FullDimensionalFrame{N,W},
} <: AbstractUniformFullDimensionalLogiset{U,N,W,FT,FR}

Uniform scalar logiset with full dimensional frames of dimensionality N, storing values for each world in a ninstances × nfeatures array.

The size of the internal structure (or featstruct) depends on the (unique) world type considered.

Examples

Interval-based frames

With an interval-based, N-dimensional frame, the worlds are N-intervals, and have 2*N parameters, which are used to index an (N*2+2)-dimensional featstruct (recall that two dimensions are reserved for instances and features).

For example, consider the case of a 1-dimensional frame with three points: 1 2 3 ─────────────────────────

Given an instance and a feature, the featstruct will map the hyper-intervals across two dimensions: ┌───┬───────┬───────┬───────┐ │ │ 1 │ 2 │ 3 │ ├───┼───────┼───────┼───────┤ │ 1 │ [1,1] │ [1,2] │ [1,3] │ ├───┼───────┼───────┼───────┤ │ 2 │ │ [2,2] │ [2,3] │ ├───┼───────┼───────┼───────┤ │ 3 │ │ │ [3,3] │ └───┴───────┴───────┴───────┘

See also AbstractModalLogiset, AbstractUniformFullDimensionalLogiset, SoleLogics.FullDimensionalFrame.

source
SoleData.DimensionalDatasets.UniformFullDimensionalOneStepRelationalMemoset — Type

A relational memoset optimized for uniform scalar logisets with full dimensional frames of dimensionality N, storing values for each world in a ninstances × nmetaconditions × nrelations array. Each world is a hyper-interval, and its N*2 components are used to index different array dimensions, ultimately resulting in a (N*2+3)-dimensional array.

See also UniformFullDimensionalLogiset, FullDimensionalFrame, AbstractModalLogiset.

source
SoleData.initlogiset — Method
function initlogiset(
    dataset::AbstractDimensionalDataset,
    features::AbstractVector;
    worldtype_by_dim::Union{Nothing,AbstractDict{<:Integer,<:Type}}=nothing
)::UniformFullDimensionalLogiset

Given an AbstractDimensionalDataset, build a UniformFullDimensionalLogiset.

Keyword Arguments

  • worldtypebydim::Union{Nothing,AbstractDict{<:Integer,<:Type}}=nothing:

map between a dimensionality, as integer, and the AbstractWorld type associated; when unspecified, this is defaulted to Dict(0 => OneWorld, 1 => Interval, 2 => Interval2D).

See also AbstractDimensionalDataset, SoleLogics.AbstractWorld, MultiData.dimensionality, UniformFullDimensionalLogiset.

source

Multimodal Logisets

<!– ## MLJ Integration

–>

Optimizations

Representatives

SoleData.representatives — Method
representatives(
    fr::AbstractFrame{W},
    S::W,
    ::AbstractRelation,
    ::AbstractCondition
) where {W<:AbstractWorld}

Return an iterator to the (few) representative accessible worlds that are necessary for computing and propagating truth values through existential modal connectives. When this optimization is possible (e.g., when checking specific formulas on scalar conditions), it allows to further boost "one-step" optimizations (see AbstractOneStepMemoset).

For example, consider a Kripke structure with a 1-dimensional FullDimensionalFrame of length 100, and the problem of checking a formula "⟨L⟩(max[V1] ≥ 10)" on a SoleLogics.Interval SoleLogics.Interval{Int64}(1, 2) (with L being Allen's "Later" relation, see SoleLogics.IA_L). Comparing 10 with the (maximum) "max[V1]" computed on all worlds is the naïve strategy to check the formula. However, in this case, comparing 10 to the "max[V1]" computed on the single Interval SoleLogics.Interval{Int64}(2, 101) suffice to establish whether the structure satisfies the formula. Similar cases arise depending on the relation, feature and test operator (or, better, its aggregator).

Note that this method fallsback to accessibles.

See also SoleLogics.accessibles, ScalarCondition, SoleLogics.AbstractFrame.

source