Logical foundations

SoleLogics lays the logical foundations for this package. While the full reference for SoleLogics can be found here, these are the basic logical concepts needed for symbolic modelling.

SoleLogics.Atom — Type

struct Atom{V} <: AbstractAtom
    value::V
end

Simplest atom implementation, wrapping a value.

source

SoleLogics.CONJUNCTION — Constant

const CONJUNCTION = NamedConnective{:∧}()
const ∧ = CONJUNCTION
arity(::typeof(∧)) = 2

Logical conjunction. It can be typed by \wedge<tab>.

source

SoleLogics.DISJUNCTION — Constant

const DISJUNCTION = NamedConnective{:∨}()
const ∨ = DISJUNCTION
arity(::typeof(∨)) = 2

Logical disjunction. It can be typed by \vee<tab>.

source

SoleLogics.Formula — Type

abstract type Formula <: Syntactical end

Abstract type for logical formulas. Examples of Formulas are SyntaxLeafs (for example, Atoms and Truth values), SyntaxStructures (for example, SyntaxTrees and LeftmostLinearForms) and TruthTables ( enriched representation, which associates a syntactic structure with additional memoization structures, which can save computational time upon model checking).

Any formula can be converted into its SyntaxTree representation via tree; its height can be computed, and it can be queried for its syntax tokens, atoms, etc... It can be parsed from its syntaxstring representation via parseformula.

Interface

tree(φ::Formula)::SyntaxTree
composeformulas(c::Connective, φs::NTuple{N,F})::F where {N,F<:Formula}
See also Syntactical

Utility functions (requiring a walk of the tree)

Base.in(tok::SyntaxToken, φ::Formula)::Bool
height(φ::Formula)::Int
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
atoms(φ::Formula)::AbstractVector{<:AbstractAtom}
truths(φ::Formula)::AbstractVector{<:Truth}
leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
connectives(φ::Formula)::AbstractVector{<:Connective}
operators(φ::Formula)::AbstractVector{<:Operator}
ntokens(φ::Formula)::Int
natoms(φ::Formula)::Int
ntruths(φ::Formula)::Int
nleaves(φ::Formula)::Int
nconnectives(φ::Formula)::Int
noperators(φ::Formula)::Int

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))"

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 (',').

source

SoleLogics.AbstractAlphabet — Type

abstract type AbstractAlphabet{V} end

Abstract type for representing an alphabet of atoms with values of type V. An alphabet (or propositional alphabet) is a set of atoms (assumed to be countable).

Examples

julia> Atom(1) in ExplicitAlphabet(Atom.(1:10))
true

julia> Atom(1) in ExplicitAlphabet(1:10)
true

julia> Atom(1) in AlphabetOfAny{String}()
false

julia> Atom("mystring") in AlphabetOfAny{String}()
true

julia> "mystring" in AlphabetOfAny{String}()
┌ Warning: Please, use Base.in(Atom(mystring), alphabet::AlphabetOfAny{String}) instead of Base.in(mystring, alphabet::AlphabetOfAny{String})
└ @ SoleLogics ...
true

Interface

atoms(a::AbstractAlphabet)::AbstractVector
Base.isfinite(::Type{<:AbstractAlphabet})::Bool
randatom(rng::Union{Random.AbstractRNG, Integer}, a::AbstractAlphabet, args...; kwargs...)::AbstractAtom

Utility functions

natoms(a::AbstractAlphabet)::Bool
Base.in(p::AbstractAtom, a::AbstractAlphabet)::Bool
Base.eltype(a::AbstractAlphabet)
randatom(a::AbstractAlphabet, args...; kwargs...)::AbstractAtom
atomstype(a::AbstractAlphabet)
valuetype(a::AbstractAlphabet)

Implementation

When implementing a new alphabet type MyAlphabet, you should provide a method for establishing whether an atom belongs to it or not; while, in general, this method should be:

function Base.in(p::AbstractAtom, a::MyAlphabet)::Bool

in the case of finite alphabets, it suffices to define a method:

function atoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}

By default, an alphabet is considered finite:

Base.isfinite(::Type{<:AbstractAlphabet}) = true
Base.isfinite(a::AbstractAlphabet) = Base.isfinite(typeof(a))
Base.in(p::AbstractAtom, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, atoms(a)) : error(...)

source

SoleLogics.AbstractInterpretation — Type

abstract type AbstractInterpretation end

Abstract type for representing a logical interpretation. In the case of propositional logic, is essentially a map atom → truth value.

Properties expressed via logical formulas can be checked on logical interpretations.

Interface

valuetype(i::AbstractInterpretation)
truthtype(i::AbstractInterpretation)
interpret(φ::Formula, i::AbstractInterpretation, args...; kwargs...)::Formula

Utility functions

check(φ::Formula, i::AbstractInterpretation, args...; kwargs...)::Bool

source

SoleLogics.AbstractInterpretationSet — Type

abstract type AbstractInterpretationSet <: AbstractDataset end

Abstract type for ordered sets of interpretations. A set of interpretations, also referred to as a dataset in this context, is a collection of instances, each of which is an interpretation, and is identified by an index iinstance::Integer. These structures are especially useful when performing [model checking](https://en.wikipedia.org/wiki/Modelchecking).

Interface

Utility Functions

Utility Functions (with more-than-propositional logics)

See also Atom.

source

function check(
    φ::SyntaxTree,
    i::AbstractKripkeStructure,
    w::Union{Nothing,AnyWorld,<:AbstractWorld} = nothing;
    use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing,
    perform_normalization::Bool = true,
    memo_max_height::Union{Nothing,Int} = nothing,
)::Bool

Check a formula on a specific word in a KripkeStructure.

Examples

julia> using Graphs, Random

julia> @atoms String p q
2-element Vector{Atom{String}}:
 Atom{String}("p")
 Atom{String}("q")

julia> fmodal = randformula(Random.MersenneTwister(14), 3, [p,q], SoleLogics.BASE_MODAL_CONNECTIVES)
¬□(p ∨ q)

# A special graph, called Kripke Frame, is created.
# Nodes are called worlds, and the edges are relations between worlds.
julia> worlds = SoleLogics.World.(1:5) # 5 worlds are created, numerated from 1 to 5

julia> edges = Edge.([(1,2), (1,3), (2,4), (3,4), (3,5)])

julia> kframe = SoleLogics.ExplicitCrispUniModalFrame(worlds, Graphs.SimpleDiGraph(edges))

# A valuation function establishes which fact are true on each world
julia> valuation = Dict([
    worlds[1] => TruthDict([p => true, q => false]),
    worlds[2] => TruthDict([p => true, q => true]),
    worlds[3] => TruthDict([p => true, q => false]),
    worlds[4] => TruthDict([p => false, q => false]),
    worlds[5] => TruthDict([p => false, q => true]),
 ])

# Kripke Frame and valuation function are merged in a Kripke Structure
julia> kstruct = KripkeStructure(kframe, valuation)

julia> [w => check(fmodal, kstruct, w) for w in worlds]
5-element Vector{Pair{SoleLogics.World{Int64}, Bool}}:
 SoleLogics.World{Int64}(1) => 0
 SoleLogics.World{Int64}(2) => 1
 SoleLogics.World{Int64}(3) => 1
 SoleLogics.World{Int64}(4) => 0
 SoleLogics.World{Int64}(5) => 0

source

check(
    φ::Formula,
    s::AbstractInterpretationSet,
    i_instance::Integer,
    args...;
    kwargs...
)::Bool

Check a formula on the $i$-th instance of an AbstractInterpretationSet.

source

check(
    φ::Formula,
    s::AbstractInterpretationSet,
    args...;
    kwargs...
)::Vector{Bool}

Check a formula on all instances of an AbstractInterpretationSet.

source

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

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.

source

SoleLogics.GeometricalWorld — Type

abstract type GeometricalWorld <: AbstractWorld end

Abstract type for worlds with a geometrical interpretation.

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)

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))

source

SoleLogics.AbstractRelation — Type

abstract type AbstractRelation end

Abstract type for the relations of a multi-modal annotated accessibility graph (Kripke structure). Two noteworthy relations are identityrel and globalrel, which access the current world and all worlds, respectively.

Examples

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

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

Implementation

When implementing a new relation type R, please provide the methods:

arity(::R)::Int = ...
syntaxstring(::R; kwargs...)::String = ...

If the relation is symmetric, please specify its converse relation cr with:

hasconverse(::R) = true
converse(::R) = cr

If the relation is many-to-one or one-to-one, please flag it with:

istoone(::R) = true

If the relation is reflexive or transitive, flag it with:

isreflexive(::R) = true
istransitive(::R) = true

Most importantly, the logical semantics for R should be defined via accessibles methods; refer to the help for accessibles.

source

SoleLogics.globalrel — Constant

struct GlobalRel <: AbstractRelation end;
const globalrel  = GlobalRel();

Singleton type for the global relation. This is a binary relation via which a world accesses every other world within the frame. The relation is also symmetric, reflexive and transitive.

Examples

julia> syntaxstring(SoleLogics.globalrel)
"G"

julia> SoleLogics.converse(globalrel)
GlobalRel()

source

SoleLogics.IA_L — Constant

See IntervalRelation

source

SoleLogics.AbstractFrame — Type

abstract type AbstractFrame{W<:AbstractWorld} end

Abstract type for an accessibility graph (Kripke frame), that gives the topology to Kripke structures. A frame can be queried for its set of vertices (also called worlds, see allworlds), and it can be browsed via its accessibility relation(s) (see accessibles). Refer to FullDimensionalFrame as an example.

source

SoleLogics.AbstractKripkeStructure — Type

abstract type AbstractKripkeStructure <: AbstractInterpretation end

Abstract type for representing Kripke structures's. It comprehends a directed graph structure (Kripke frame), where nodes are referred to as worlds, and the binary relation between them is referred to as the accessibility relation. Additionally, each world is associated with a mapping from Atoms to Truth values.

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.

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 of 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 of 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}.

source