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

See also AbstractGrammar, AlphabetOfAny, AbstractAtom, ExplicitAlphabet.

Base.isfinite(a::AbstractAlphabet)

Return true if the alphabet is finite, false otherwise.

See AbstractAlphabet.

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

List the atoms of a finite alphabet.

See also AbstractAlphabet.

natoms(a::AbstractAlphabet)::Integer

Return the number of atoms of a finite alphabet.

See also randatom, AbstractAlphabet.

Base.in(p::AbstractAtom, a::AbstractAlphabet)::Bool

Return whether an atom belongs to an alphabet.

See also AbstractAlphabet, AbstractAtom.

struct ExplicitAlphabet{V} <: AbstractAlphabet{V}
    atoms::Vector{Atom{V}}
end

An alphabet wrapping atoms in a (finite) Vector.

See also AbstractAlphabet, atoms.

struct AlphabetOfAny{V} <: AbstractAlphabet{V} end

An implicit, infinite alphabet that includes all atoms with values of a subtype of V.

See also AbstractAlphabet.

abstract type AbstractGrammar{V<:AbstractAlphabet,O<:Operator} end

Abstract type for representing a context-free grammar based on a single alphabet of type V, and a set of operators that consists of all the (singleton) child types of O. V context-free grammar is a simple structure for defining formulas inductively.

Interface

• alphabet(g::AbstractGrammar)::AbstractAlphabet
• Base.in(::SyntaxTree, g::AbstractGrammar)::Bool
• formulas(g::AbstractGrammar; kwargs...)::Vector{<:SyntaxTree}

Utility functions

• Base.in(a::AbstractAtom, g::AbstractGrammar)
• atomstype(g::AbstractGrammar)
• tokenstype(g::AbstractGrammar)
• operatorstype(g::AbstractGrammar)
• alphabettype(g::AbstractGrammar)

See also alphabet, AbstractAlphabet, Operator.

alphabet(g::AbstractGrammar{V} where {V})::V

Return the propositional alphabet of a grammar.

See also AbstractAlphabet, AbstractGrammar.

Base.in(φ::SyntaxTree, g::AbstractGrammar)::Bool

Return whether a SyntaxTree, belongs to a grammar.

See also AbstractGrammar, SyntaxTree.

formulas(
    g::AbstractGrammar;
    maxdepth::Integer,
    nformulas::Union{Nothing,Integer} = nothing,
    args...
)::Vector{<:SyntaxTree}

Enumerate the formulas produced by a given grammar with a finite and iterable alphabet.

Implementation

Additional args can be used to model the function's behavior. At least these two arguments should be covered:

• a nformulas argument can be used to limit the size of the returned Vector;
• a maxdepth argument can be used to limit the syntactic component, represented as a syntax tree,

to a given maximum depth;

See also AbstractGrammar, AbstractSyntaxBranch.

struct CompleteFlatGrammar{V<:AbstractAlphabet,O<:Operator} <: AbstractGrammar{V,O}
    alphabet::V
    operators::Vector{<:O}
end

V grammar of all well-formed formulas obtained by the arity-complying composition of atoms of an alphabet of type V, and all operators in operators. With n operators, this grammar has exactly n+1 production rules. For example, with operators = [∧,∨], the grammar (in Backus-Naur form) is:

φ ::= p | φ ∧ φ | φ ∨ φ

with p ∈ alphabet. Note: it is flat in the sense that all rules substitute the same (unique and starting) non-terminal symbol φ.

See also AbstractGrammar, Operator, alphabet, formulas, connectives, operators, leaves.

connectives(g::AbstractGrammar)

List all connectives appearing in a grammar.

See also Connective, nconnectives.

leaves(g::AbstractGrammar)

List all leaves appearing in a grammar.

See also SyntaxLeaf, nleaves.

formulas(
    g::CompleteFlatGrammar{V,O} where {V,O};
    maxdepth::Integer,
    nformulas::Union{Nothing,Integer} = nothing
)::Vector{SyntaxBranch}

Generate all formulas whose SyntaxBranchs that are not taller than a given maxdepth.

See also AbstractGrammar, SyntaxBranch.

abstract type AbstractAlgebra{T<:Truth} end

Abstract type for representing algebras. Algebras are used for grounding the truth of atoms and the semantics of operators. They typically encode a lattice structure where two elements(or nodes) ⊤ and ⊥ are referred to as TOP (or maximum) and bot (or minimum). Each node in the lattice represents a truth value that an atom or a formula can have on an interpretation, and the semantics of operators is given in terms of operations between truth values.

Interface

• truthtype(a::AbstractAlgebra)
• domain(a::AbstractAlgebra)
• top(a::AbstractAlgebra)
• bot(a::AbstractAlgebra)

Utility functions

• iscrisp(a::AbstractAlgebra)

Implementation

When implementing a new algebra type, the methods domain, TOP, and bot should be implemented.

See also bot, BooleanAlgebra, Operator, TOP, collatetruth, domain, iscrisp, truthtype.

truthtype(::Type{<:AbstractAlgebra{T}}) where {T<:Truth} = T
truthtype(a::AbstractAlgebra) = truthtype(typeof(a))

The Julia type for representing truth values of the algebra.

See also AbstractAlgebra.

domain(a::AbstractAlgebra)

Return an iterator to the values in the domain of a given algebra.

See also AbstractAlgebra.

top(a::AbstractAlgebra)

Return the top of a given algebra.

See also bot, AbstractAlgebra.

bot(a::AbstractAlgebra)

Return the bottom of a given algebra.

See also top, AbstractAlgebra.

iscrisp(a::AbstractAlgebra) = iscrisp(typeof(a))

An algebra is crisp (or boolean) when its domain only has two values, namely, the top and the bottom. The antonym of crisp is fuzzy.

See also AbstractAlgebra.

abstract type AbstractLogic{G<:AbstractGrammar,A<:AbstractAlgebra} end

Abstract type of a logic, which comprehends a context-free grammar (syntax) and an algebra (semantics).

Interface

• grammar(l::AbstractLogic)::AbstractGrammar
• algebra(l::AbstractLogic)::AbstractAlgebra

Utility functions

• See also AbstractGrammar
• See also AbstractAlgebra

Implementation

When implementing a new logic type, the methods grammar and algebra should be implemented.

See also AbstractAlgebra, AbstractGrammar.

grammar(l::AbstractLogic{G})::G where {G<:AbstractGrammar}

Return the grammar of a given logic.

See also AbstractGrammar, AbstractLogic, algebra, alphabet, formulas, grammar, operators, truthtype.

algebra(l::AbstractLogic{G,V})::V where {G,V}

Return the algebra of a given logic.

See also AbstractAlgebra, AbstractLogic.

struct NamedConnective{Symbol} <: Connective end

A singleton type for representing connectives defined by a name or a symbol.

Examples

The AND connective (i.e., the logical conjunction) is defined as the subtype:

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

See also NEGATION, CONJUNCTION, DISJUNCTION, IMPLICATION, Connective.

collatetruth(c::Connective, ts::NTuple{N,T where T<:Truth}, args...)::Truth where {N}

Return the truth value for a composed formula c(t1, ..., tN), given the N with t1, ..., tN being Truth values.

See also simplify, Connective, Truth.

simplify(c::Connective, ts::NTuple{N,F where F<:Formula} args...)::Truth where {N}

Return a formula with the same semantics of a composed formula c(φ1, ..., φN), given the N immediate sub-formulas.

See also collatetruth, Connective, Formula.

const NEGATION = NamedConnective{:¬}()
const ¬ = NEGATION
arity(::typeof(¬)) = 1

Logical negation (also referred to as complement). It can be typed by \neg<tab>.

See also NamedConnective, Connective.

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

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

See also NamedConnective, Connective.

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

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

See also NamedConnective, Connective.

const IMPLICATION = NamedConnective{:→}()
const → = IMPLICATION
arity(::typeof(→)) = 2

Logical implication. It can be typed by \to<tab>.

See also NamedConnective, Connective.

const BASE_CONNECTIVES = [¬, ∧, ∨, →]

Basic logical operators.

See also NEGATION, CONJUNCTION, DISJUNCTION, IMPLICATION, Connective.

struct BooleanTruth <: Truth
    flag::Bool
end

Structure for representing the Boolean truth values ⊤ and ⊥. It wraps a flag which takes value true for ⊤ (TOP), and false for ⊥ (BOT)

See also BooleanAlgebra.

struct BooleanAlgebra <: AbstractAlgebra{Bool} end

A Boolean algebra, defined on the values TOP (representing truth) and BOT (for bottom, representing falsehood). For this algebra, the basic operators negation, conjunction and disjunction (stylized as ¬, ∧, ∨) can be defined as the complement, minimum and maximum, of the integer cast of true and false, respectively.

See also Truth.

struct BaseLogic{G<:AbstractGrammar,A<:AbstractAlgebra} <: AbstractLogic{G,A}
    grammar::G
    algebra::A
end

A basic logic based on a grammar and an algebra, where both the grammar and the algebra are instantiated.

See also grammar, algebra, AbstractGrammar, AbstractAlgebra, AbstractLogic.

propositionallogic(;
    alphabet = AlphabetOfAny{String}(),
    operators = NamedConnective[¬, ∧, ∨, →],
    grammar = CompleteFlatGrammar(AlphabetOfAny{String}(), NamedConnective[¬, ∧, ∨, →]),
    algebra = BooleanAlgebra()
)

Instantiate a propositional logic given a grammar and an algebra. Alternatively, an alphabet and a set of operators can be specified instead of the grammar.

Examples

julia> (¬) isa operatorstype(propositionallogic())
true

julia> (¬) isa operatorstype(propositionallogic(; operators = [∨]))
false

julia> propositionallogic(; alphabet = ["p", "q"]);

julia> propositionallogic(; alphabet = ExplicitAlphabet([Atom("p"), Atom("q")]));

See also modallogic, AbstractAlphabet, AbstractAlgebra, AlphabetOfAny, [CompleteFlatGrammar], BooleanAlgebra, BASE_PROPOSITIONAL_CONNECTIVES.

abstract type AbstractAssignment <: AbstractInterpretation end

Abstract type for assigments, that is, interpretations of propositional logic, encoding mappings from AbstractAtoms to Truth values.

Interface

• Base.haskey(i::AbstractAssignment, ::AbstractAtom)::Bool
• inlinedisplay(i::AbstractAssignment)::String
• interpret(a::AbstractAtom, i::AbstractAssignment, args...; kwargs...)::SyntaxLeaf

See also AbstractAssignment, AbstractAtom, AbstractInterpretation.

Base.haskey(i::AbstractAssignment, ::AbstractAtom)::Bool

Return whether an AbstractAssignment has a truth value for a given Atom. If any object is passed, it is wrapped in an Atom and then checked.

Examples

julia> haskey(TruthDict(["a" => true, "b" => false, "c" => true]), Atom("a"))
true

julia> haskey(TruthDict(1:4, false), Atom(3))
true

See also AbstractAssignment, AbstractInterpretation, AbstractAtom, TruthDict, Atom.

struct TruthDict{D<:AbstractDict{A where A<:Atom,T where T<:Truth}} <: AbstractAssignment
    truth::D
end

A logical interpretation instantiated as a dictionary, explicitly assigning truth values to a finite set of atoms.

Examples

julia> TruthDict(1:4)
TruthDict with values:
┌────────┬────────┬────────┬────────┐
│      4 │      2 │      3 │      1 │
│  Int64 │  Int64 │  Int64 │  Int64 │
├────────┼────────┼────────┼────────┤
│      ⊤ │      ⊤ │      ⊤ │      ⊤ │
└────────┴────────┴────────┴────────┘


julia> t1 = TruthDict(1:4, false); t1[5] = true; t1
TruthDict with values:
┌───────┬───────┬───────┬───────┬───────┐
│     5 │     4 │     2 │     3 │     1 │
│ Int64 │ Int64 │ Int64 │ Int64 │ Int64 │
├───────┼───────┼───────┼───────┼───────┤
│     ⊤ │     ⊥ │     ⊥ │     ⊥ │     ⊥ │
└───────┴───────┴───────┴───────┴───────┘

julia> t2 = TruthDict(["a" => true, "b" => false, "c" => true])
TruthDict with values:
┌────────┬────────┬────────┐
│      c │      b │      a │
│ String │ String │ String │
├────────┼────────┼────────┤
│      ⊤ │      ⊥ │      ⊤ │
└────────┴────────┴────────┘

julia> check(parseformula("a ∨ b"), t2)
true

See also AbstractAssignment, AbstractInterpretation, DefaultedTruthDict, BooleanTruth.

struct DefaultedTruthDict{
    D<:AbstractDict{A where A<:Atom,T where T<:Truth},
    T<:Truth
} <: AbstractAssignment
    truth::D
    default_truth::T
end

A truth table instantiated as a dictionary, plus a default value. This structure assigns truth values to a set of atoms and, when prompted for the value of an atom that is not in the dictionary, it returns default_truth.

Implementation

If you use interpret function and you pass a DefaultedTruthDict as AbstractAssignment and the Atom is not present in the dictionary, then the default dictionary value will be returned and not the Atom itself.

Here is an example of this.

julia> interpret(Atom(5), DefaultedTruthDict(string.(1:4), false))
⊥

Examples

julia> t1 = DefaultedTruthDict(string.(1:4), false); t1["5"] = false; t1
DefaultedTruthDict with default truth `⊥` and values:
┌────────┬────────┬────────┬────────┬────────┐
│      4 │      1 │      5 │      2 │      3 │
│ String │ String │ String │ String │ String │
├────────┼────────┼────────┼────────┼────────┤
│      ⊤ │      ⊤ │      ⊥ │      ⊤ │      ⊤ │
└────────┴────────┴────────┴────────┴────────┘

julia> check(parseformula("1 ∨ 2"), t1)
true

julia> check(parseformula("1 ∧ 5"), t1)
false

See also AbstractAssignment, AbstractInterpretation, interpret, Atom, TruthDict, DefaultedTruthDict.

struct TruthTable{A,T<:Truth}

Dictionary which associates an AbstractAssignments to the truth value of the assignment itself on a SyntaxStructure.

See also AbstractAssignment, SyntaxStructure, Truth.