diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index e5d8be5..921c943 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.11.1","generation_timestamp":"2024-11-08T15:38:52","documenter_version":"1.7.0"}} \ No newline at end of file +{"documenter":{"julia_version":"1.11.1","generation_timestamp":"2024-11-08T15:39:34","documenter_version":"1.7.0"}} \ No newline at end of file diff --git a/dev/base-logic/index.html b/dev/base-logic/index.html index 4e53ae9..5a59a60 100644 --- a/dev/base-logic/index.html +++ b/dev/base-logic/index.html @@ -16,37 +16,37 @@ └ @ SoleLogics ... true

Interface

Utility functions

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.

source
Base.isfinite — Method
Base.isfinite(a::AbstractAlphabet)

Return true if the alphabet is finite, false otherwise.

See AbstractAlphabet.

source
SoleLogics.atoms — Method
atoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}

List the atoms of a finite alphabet.

See also AbstractAlphabet.

source
SoleLogics.natoms — Method
natoms(a::AbstractAlphabet)::Integer

Return the number of atoms of a finite alphabet.

See also randatom, AbstractAlphabet.

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

Return whether an atom belongs to an alphabet.

See also AbstractAlphabet, AbstractAtom.

source
SoleLogics.ExplicitAlphabet — Type
struct ExplicitAlphabet{V} <: AbstractAlphabet{V}
+Base.in(p::AbstractAtom, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, atoms(a)) : error(...)

See also AbstractGrammar, AlphabetOfAny, AbstractAtom, ExplicitAlphabet.

source
Base.isfinite — Method
Base.isfinite(a::AbstractAlphabet)

Return true if the alphabet is finite, false otherwise.

See AbstractAlphabet.

source
SoleLogics.atoms — Method
atoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}

List the atoms of a finite alphabet.

See also AbstractAlphabet.

source
SoleLogics.natoms — Method
natoms(a::AbstractAlphabet)::Integer

Return the number of atoms of a finite alphabet.

See also randatom, AbstractAlphabet.

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

Return whether an atom belongs to an alphabet.

See also AbstractAlphabet, AbstractAtom.

source
SoleLogics.ExplicitAlphabet — Type
struct ExplicitAlphabet{V} <: AbstractAlphabet{V}
     atoms::Vector{Atom{V}}
-end

An alphabet wrapping atoms in a (finite) Vector.

See also AbstractAlphabet, atoms.

source
SoleLogics.AlphabetOfAny — Type
struct AlphabetOfAny{V} <: AbstractAlphabet{V} end

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

See also AbstractAlphabet.

source

Grammar

SoleLogics.AbstractGrammar — Type
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.

source
SoleLogics.alphabet — Method
alphabet(g::AbstractGrammar{V} where {V})::V

Return the propositional alphabet of a grammar.

See also AbstractAlphabet, AbstractGrammar.

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

Return whether a SyntaxTree, belongs to a grammar.

See also AbstractGrammar, SyntaxTree.

source
SoleLogics.formulas — Method
formulas(
+end

An alphabet wrapping atoms in a (finite) Vector.

See also AbstractAlphabet, atoms.

source
SoleLogics.AlphabetOfAny — Type
struct AlphabetOfAny{V} <: AbstractAlphabet{V} end

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

See also AbstractAlphabet.

source

Grammar

SoleLogics.AbstractGrammar — Type
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.

source
SoleLogics.alphabet — Method
alphabet(g::AbstractGrammar{V} where {V})::V

Return the propositional alphabet of a grammar.

See also AbstractAlphabet, AbstractGrammar.

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

Return whether a SyntaxTree, belongs to a grammar.

See also AbstractGrammar, SyntaxTree.

source
SoleLogics.formulas — Method
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.

source
SoleLogics.CompleteFlatGrammar — Type
struct CompleteFlatGrammar{V<:AbstractAlphabet,O<:Operator} <: AbstractGrammar{V,O}
+)::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.

source
SoleLogics.CompleteFlatGrammar — Type
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.

source
SoleLogics.connectives — Method
connectives(g::AbstractGrammar)

List all connectives appearing in a grammar.

See also Connective, nconnectives.

source
SoleLogics.leaves — Method
leaves(g::AbstractGrammar)

List all leaves appearing in a grammar.

See also SyntaxLeaf, nleaves.

source
SoleLogics.formulas — Method
formulas(
+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.

source
SoleLogics.connectives — Method
connectives(g::AbstractGrammar)

List all connectives appearing in a grammar.

See also Connective, nconnectives.

source
SoleLogics.leaves — Method
leaves(g::AbstractGrammar)

List all leaves appearing in a grammar.

See also SyntaxLeaf, nleaves.

source
SoleLogics.formulas — Method
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.

source

Algebra

SoleLogics.AbstractAlgebra — Type
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.

source
SoleLogics.truthtype — Method
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.

source
SoleLogics.domain — Method
domain(a::AbstractAlgebra)

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

See also AbstractAlgebra.

source
SoleLogics.top — Method
top(a::AbstractAlgebra)

Return the top of a given algebra.

See also bot, AbstractAlgebra.

source
SoleLogics.bot — Method
bot(a::AbstractAlgebra)

Return the bottom of a given algebra.

See also top, AbstractAlgebra.

source
SoleLogics.iscrisp — Method
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.

source

Logic

SoleLogics.AbstractLogic — Type
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

Implementation

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

See also AbstractAlgebra, AbstractGrammar.

source
SoleLogics.grammar — Method
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.

source
SoleLogics.algebra — Method
algebra(l::AbstractLogic{G,V})::V where {G,V}

Return the algebra of a given logic.

See also AbstractAlgebra, AbstractLogic.

source

More on Connectives

SoleLogics.NamedConnective — Type
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{:∧}()
+)::Vector{SyntaxBranch}

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

See also AbstractGrammar, SyntaxBranch.

source

Algebra

SoleLogics.AbstractAlgebra — Type
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.

source
SoleLogics.truthtype — Method
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.

source
SoleLogics.domain — Method
domain(a::AbstractAlgebra)

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

See also AbstractAlgebra.

source
SoleLogics.top — Method
top(a::AbstractAlgebra)

Return the top of a given algebra.

See also bot, AbstractAlgebra.

source
SoleLogics.bot — Method
bot(a::AbstractAlgebra)

Return the bottom of a given algebra.

See also top, AbstractAlgebra.

source
SoleLogics.iscrisp — Method
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.

source

Logic

SoleLogics.AbstractLogic — Type
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

Implementation

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

See also AbstractAlgebra, AbstractGrammar.

source
SoleLogics.grammar — Method
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.

source
SoleLogics.algebra — Method
algebra(l::AbstractLogic{G,V})::V where {G,V}

Return the algebra of a given logic.

See also AbstractAlgebra, AbstractLogic.

source

More on Connectives

SoleLogics.NamedConnective — Type
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.

source
SoleLogics.collatetruth — Method
collatetruth(c::Connective, ts::NTuple{N,T where T<:Truth})::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.

source
SoleLogics.simplify — Method
simplify(c::Connective, ts::NTuple{N,F where F<:Formula})::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.

source

Propositional boolean logic

SoleLogics.NEGATION — Constant
const NEGATION = NamedConnective{:¬}()
+arity(::typeof(∧)) = 2

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

source
SoleLogics.collatetruth — Method
collatetruth(c::Connective, ts::NTuple{N,T where T<:Truth})::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.

source
SoleLogics.simplify — Method
simplify(c::Connective, ts::NTuple{N,F where F<:Formula})::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.

source

Propositional boolean logic

SoleLogics.NEGATION — Constant
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.

source
SoleLogics.CONJUNCTION — Constant
const CONJUNCTION = NamedConnective{:∧}()
+arity(::typeof(¬)) = 1

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

See also NamedConnective, Connective.

source
SoleLogics.CONJUNCTION — Constant
const CONJUNCTION = NamedConnective{:∧}()
 const ∧ = CONJUNCTION
-arity(::typeof(∧)) = 2

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

See also NamedConnective, Connective.

source
SoleLogics.DISJUNCTION — Constant
const DISJUNCTION = NamedConnective{:∨}()
+arity(::typeof(∧)) = 2

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

See also NamedConnective, Connective.

source
SoleLogics.DISJUNCTION — Constant
const DISJUNCTION = NamedConnective{:∨}()
 const ∨ = DISJUNCTION
-arity(::typeof(∨)) = 2

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

See also NamedConnective, Connective.

source
SoleLogics.IMPLICATION — Constant
const IMPLICATION = NamedConnective{:→}()
+arity(::typeof(∨)) = 2

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

See also NamedConnective, Connective.

source
SoleLogics.IMPLICATION — Constant
const IMPLICATION = NamedConnective{:→}()
 const → = IMPLICATION
-arity(::typeof(→)) = 2

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

See also NamedConnective, Connective.

source

Boolean logic Connectives are regrouped in a single collection.

SoleLogics.BASE_CONNECTIVES — Constant
const BASE_CONNECTIVES = [¬, ∧, ∨, →]

Basic logical operators.

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

source
SoleLogics.BooleanTruth — Type
struct BooleanTruth <: Truth
+arity(::typeof(→)) = 2

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

See also NamedConnective, Connective.

source

Boolean logic Connectives are regrouped in a single collection.

SoleLogics.BASE_CONNECTIVES — Constant
const BASE_CONNECTIVES = [¬, ∧, ∨, →]

Basic logical operators.

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

source
SoleLogics.BooleanTruth — Type
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.

source
SoleLogics.BooleanAlgebra — Type
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.

source
SoleLogics.BaseLogic — Type
struct BaseLogic{G<:AbstractGrammar,A<:AbstractAlgebra} <: AbstractLogic{G,A}
+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.

source
SoleLogics.BooleanAlgebra — Type
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.

source
SoleLogics.BaseLogic — Type
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.

source

A method is provided to simply access a propositional logic.

SoleLogics.propositionallogic — Method
propositionallogic(;
+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.

source

A method is provided to simply access a propositional logic.

SoleLogics.propositionallogic — Method
propositionallogic(;
     alphabet = AlphabetOfAny{String}(),
     operators = NamedConnective[¬, ∧, ∨, →],
     grammar = CompleteFlatGrammar(AlphabetOfAny{String}(), NamedConnective[¬, ∧, ∨, →]),
@@ -60,11 +60,11 @@
 julia> propositionallogic(; alphabet = ["p", "q"]);
 
 julia> propositionallogic(; alphabet = ExplicitAlphabet([Atom("p"), Atom("q")]));
-

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

source

Interpretations

Interpretations are nothing but dictionaries working with Truth values, or other types that can be ultimately converted to Truth.

SoleLogics.AbstractAssignment — Type
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.

source
Base.haskey — Method
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"))
+

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

source

Interpretations

Interpretations are nothing but dictionaries working with Truth values, or other types that can be ultimately converted to Truth.

SoleLogics.AbstractAssignment — Type
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.

source
Base.haskey — Method
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.

source
SoleLogics.TruthDict — Type
struct TruthDict{D<:AbstractDict{A where A<:Atom,T where T<:Truth}} <: AbstractAssignment
+true

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

source
SoleLogics.TruthDict — Type
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:
@@ -96,7 +96,7 @@
 
 julia> check(parseformula("a ∨ b"), t2)
 true
-
Note

If prompted for the value of an unknown atom, this throws an error. If boolean, integer, or float values are specified, they are converted to Truth values. If the structure is initialized as empty, BooleanTruth values are assumed.

See also AbstractAssignment, AbstractInterpretation, DefaultedTruthDict, BooleanTruth.

source
SoleLogics.DefaultedTruthDict — Type
struct DefaultedTruthDict{
+
Note

If prompted for the value of an unknown atom, this throws an error. If boolean, integer, or float values are specified, they are converted to Truth values. If the structure is initialized as empty, BooleanTruth values are assumed.

See also AbstractAssignment, AbstractInterpretation, DefaultedTruthDict, BooleanTruth.

source
SoleLogics.DefaultedTruthDict — Type
struct DefaultedTruthDict{
     D<:AbstractDict{A where A<:Atom,T where T<:Truth},
     T<:Truth
 } <: AbstractAssignment
@@ -117,11 +117,11 @@
 
 julia> check(parseformula("1 ∧ 5"), t1)
 false
-

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

source

To associate interpretations with their assignment, we can simply build a truth table.

SoleLogics.TruthTable — Type
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.

source
AbstractInterpretationSet
+

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

source

To associate interpretations with their assignment, we can simply build a truth table.

SoleLogics.TruthTable — Type
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.

source
AbstractInterpretationSet
 
 LogicalInstance{S<:AbstractInterpretationSet}
 
 check(φ::Formula, s::AbstractInterpretationSet, i_instance::Integer, args...; kwargs...)
 check(φ::Formula, s::AbstractInterpretationSet, args...; kwargs...)
 
-InterpretationVector{M<:AbstractInterpretation}
+InterpretationVector{M<:AbstractInterpretation} diff --git a/dev/getting-started/index.html b/dev/getting-started/index.html index c193d1b..bee4c09 100644 --- a/dev/getting-started/index.html +++ b/dev/getting-started/index.html @@ -1,5 +1,5 @@ -Getting started · SoleLogics.jl
GitHub

Getting started

In this introductory section you will learn about the main building blocks of SoleLogics. Their definition, usage examples and how to customize them to your own needs.

In short, you can consider this package as divided into two halves.:

  • the syntactical half, which defines structures to represent logical constructs such as assertions, logical constants, alphabets, grammars, crisp and fuzzy algebras, formulas etc. A consistent part of SoleLogics is devoted to randomly generate such structures, as well as parse and minimize formulas;
  • the semantic half, which defines rules to apply when interpreting a logical formulas. The "semantic heart" of SoleLogics is its finite model checking algorithm, whose purpose is to efficiently check whether a formula is satisfied by an interpretation or not.

Please, feel free to use the following tree structures to orient yourself in the reading of this section. More pieces will be added to this type-hierarchy tree in the following sections.

Type hierarchy

Also, two union types are defined:

Syntax Basics

SoleLogics.Syntactical — Type
abstract type Syntactical end

Master abstract type for all syntactical objects (e.g., formulas, connectives).

Interface

  • syntaxstring(s::Syntactical; kwargs...)::String

See also Formula, Connective.

source

To print out a generic Syntactical element, we must define how it is converted into a string. To do this, we can implement a custom syntaxstring.

SoleLogics.syntaxstring — Method
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"))
+Getting started · SoleLogics.jl
GitHub
Getting started
In this introductory section you will learn about the main building blocks of SoleLogics. Their definition, usage examples and how to customize them to your own needs. 
In short, you can consider this package as divided into two halves.:
  • the syntactical half, which defines structures to represent logical constructs such as assertions, logical constants, alphabets, grammars, crisp and fuzzy algebras, formulas etc. A consistent part of SoleLogics is devoted to randomly generate such structures, as well as parse and minimize formulas;
  • the semantic half, which defines rules to apply when interpreting a logical formulas. The "semantic heart" of SoleLogics is its finite model checking algorithm, whose purpose is to efficiently check whether a formula is satisfied by an interpretation or not.
Please, feel free to use the following tree structures to orient yourself in the reading of this section. More pieces will be added to this type-hierarchy tree in the following sections.
Type hierarchy
Also, two union types are defined:
Syntax Basics
SoleLogics.Syntactical — Type
abstract type Syntactical end
Master abstract type for all syntactical objects (e.g., formulas, connectives).
Interface
  • syntaxstring(s::Syntactical; kwargs...)::String
See also Formula, Connective.
source
To print out a generic Syntactical element, we must define how it is converted into a string. To do this, we can implement a custom syntaxstring.
SoleLogics.syntaxstring — Method
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)
@@ -15,15 +15,15 @@
 "◊((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.Connective — Type
abstract type Connective <: Syntactical end
Abstract type for logical connectives, that are used to express non-atomic statements; for example, CONJUNCTION, DISJUNCTION, NEGATION and IMPLICATION (stylized as ∧, ∨, ¬ and →).
Interface
  • arity(::Connective)::Int
  • iscommutative(::Connective)::Bool
  • precedence(::Connective)::Int
  • associativity(::Connective)::Symbol
  • collatetruth(::Connective, ::NTuple{N,Truth})::Truth
  • simplify(::Connective, ::NTuple{N,SyntaxTree})::SyntaxTree
  • dual(s::Connective)::Connective
  • hasdual(s::Connective)::Bool
  • See also Syntactical
Implementation
When implementing a new type C for a connective, please define its arity. For example, with a binary operator (e.g., ∨ or ∧):
arity(::C) = 2
When implementing a new type C for a commutative connective with arity higher than 1, please provide a method iscommutative(::C). This can speed up model checking operations.
When implementing a custom binary connective, one can override the default precedence and associativity (see here. If the custom connective is a NamedConnective and renders as something considered as a math symbol (for example, ⊙, see https://stackoverflow.com/a/60321302/5646732), by the Julia parser, Base.operator_precedence and Base.operator_associativity are used to define these behaviors, and you might want to avoid providing these methods at all.
The semantics of a propositional connective can be specified via collatetruth (see example below); in principle, the definition can rely on the partial order between truth values (specified via precedes).
Here is an example of a custom implementation of the xor (⊻) Boolean operator.
import SoleLogics: arity, iscommutative, collatetruth
+"◊(→(∧(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.Connective — Type
abstract type Connective <: Syntactical end
Abstract type for logical connectives, that are used to express non-atomic statements; for example, CONJUNCTION, DISJUNCTION, NEGATION and IMPLICATION (stylized as ∧, ∨, ¬ and →).
Interface
  • arity(::Connective)::Int
  • iscommutative(::Connective)::Bool
  • precedence(::Connective)::Int
  • associativity(::Connective)::Symbol
  • collatetruth(::Connective, ::NTuple{N,Truth})::Truth
  • simplify(::Connective, ::NTuple{N,SyntaxTree})::SyntaxTree
  • dual(s::Connective)::Connective
  • hasdual(s::Connective)::Bool
  • See also Syntactical
Implementation
When implementing a new type C for a connective, please define its arity. For example, with a binary operator (e.g., ∨ or ∧):
arity(::C) = 2
When implementing a new type C for a commutative connective with arity higher than 1, please provide a method iscommutative(::C). This can speed up model checking operations.
When implementing a custom binary connective, one can override the default precedence and associativity (see here. If the custom connective is a NamedConnective and renders as something considered as a math symbol (for example, ⊙, see https://stackoverflow.com/a/60321302/5646732), by the Julia parser, Base.operator_precedence and Base.operator_associativity are used to define these behaviors, and you might want to avoid providing these methods at all.
The semantics of a propositional connective can be specified via collatetruth (see example below); in principle, the definition can rely on the partial order between truth values (specified via precedes).
Here is an example of a custom implementation of the xor (⊻) Boolean operator.
import SoleLogics: arity, iscommutative, collatetruth
 const ⊻ = SoleLogics.NamedConnective{:⊻}()
 SoleLogics.arity(::typeof(⊻)) = 2
 SoleLogics.iscommutative(::typeof(⊻)) = true
 SoleLogics.collatetruth(::typeof(⊻), (t1, t2)::NTuple{N,T where T<:BooleanTruth}) where {N} = (count(istop, (t1, t2)) == 1)
Note that collatetruth must be defined at least for some truth value types T via methods accepting an NTuple{arity,T} as a second argument.
To make the operator work with incomplete interpretations (e.g., when the Truth value for an atom is not known), simplification rules for NTuple{arity,T where T<:Formula}s should be provided via methods for simplify. For example, these rules suffice for simplifying xors between TOP/BOT`s, and other formulas:
import SoleLogics: simplify
 simplify(::typeof(⊻), (t1, t2)::Tuple{BooleanTruth,BooleanTruth}) = istop(t1) == istop(t2) ? BOT : TOP
 simplify(::typeof(⊻), (t1, t2)::Tuple{BooleanTruth,Formula}) = istop(t1) ? ¬t2 : t2
-simplify(::typeof(⊻), (t1, t2)::Tuple{Formula,BooleanTruth}) = istop(t2) ? ¬t1 : t1
Beware of dispatch ambiguities!
See also arity, SyntaxBranch, associativity, precedence, check, iscommutative, NamedConnective, Syntactical.
source
If the definition above overwhelms you, don't worry: it will be clearer later. For now we are simply interested in understanding that Connectives are simply symbols used to concatenate other logical constructs with each other. 
Later, we will see some interesting example about how to equip these symbols with semantics, that is, what rules should be applied when interpreting connectives in a generic Formula. We will also understand how to define our own custom connectives.
SoleLogics.arity — Method
arity(φ::SyntaxTree)::Integer
-arity(tok::Connective)::Integer
Return the arity of a Connective or a SyntaxTree. The arity is an integer representing the number of allowed children for a node in a tree. Connectives with arity equal to 0, 1 or 2 are called nullary, unary and binary, respectively. SyntaxLeafs (Atoms and Truth values) are always nullary.
See also SyntaxLeaf, Connective, SyntaxBranch.
source
The vast majority of data structures involved in encoding a logical formula, are children of the Formula abstract type. When such data structures purely represents tree-shaped data structures (or single nodes in them), then they are also children of the SyntaxStructure abstract type.
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
See also tree, SyntaxStructure, SyntaxLeaf.
source
The following methods define Formula interface.
SoleLogics.tree — Method
tree(φ::Formula)::SyntaxTree
Return the SyntaxTree representation of a formula; note that this is equivalent to Base.convert(SyntaxTree, φ).
See also Formula, SyntaxTree.
source
If the definition above overwhelms you, don't worry: it will be clearer later. For now we are simply interested in understanding that Connectives are simply symbols used to concatenate other logical constructs with each other. 
Later, we will see some interesting example about how to equip these symbols with semantics, that is, what rules should be applied when interpreting connectives in a generic Formula. We will also understand how to define our own custom connectives.
SoleLogics.arity — Method
arity(φ::SyntaxTree)::Integer
+arity(tok::Connective)::Integer
Return the arity of a Connective or a SyntaxTree. The arity is an integer representing the number of allowed children for a node in a tree. Connectives with arity equal to 0, 1 or 2 are called nullary, unary and binary, respectively. SyntaxLeafs (Atoms and Truth values) are always nullary.
See also SyntaxLeaf, Connective, SyntaxBranch.
source
The vast majority of data structures involved in encoding a logical formula, are children of the Formula abstract type. When such data structures purely represents tree-shaped data structures (or single nodes in them), then they are also children of the SyntaxStructure abstract type.
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
See also tree, SyntaxStructure, SyntaxLeaf.
source
The following methods define Formula interface.
SoleLogics.tree — Method
tree(φ::Formula)::SyntaxTree
Return the SyntaxTree representation of a formula; note that this is equivalent to Base.convert(SyntaxTree, φ).
See also Formula, SyntaxTree.
source
SoleLogics.tokens — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -34,7 +34,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer
Return the list/number of (non-unique) SyntaxTokens, Atoms, etc... appearing in a formula.
See also Formula, SyntaxToken.
source
Now, let us see how to compose syntax elements, to express more complex concepts.
SoleLogics.composeformulas — Method
composeformulas(c::Connective, φs::NTuple{N,F})::F where {N,F<:Formula}
Return a new formula of type F by composing N formulas of the same type via a connective c. This function allows one to use connectives for flexibly composing formulas (see Implementation section).
Examples
julia> f = parseformula("◊(p→q)");
+noperators(φ::Formula)::Integer
Return the list/number of (non-unique) SyntaxTokens, Atoms, etc... appearing in a formula.
See also Formula, SyntaxToken.
source
Now, let us see how to compose syntax elements, to express more complex concepts.
SoleLogics.composeformulas — Method
composeformulas(c::Connective, φs::NTuple{N,F})::F where {N,F<:Formula}
Return a new formula of type F by composing N formulas of the same type via a connective c. This function allows one to use connectives for flexibly composing formulas (see Implementation section).
Examples
julia> f = parseformula("◊(p→q)");
 
 julia> p = Atom("p");
 
@@ -62,9 +62,9 @@
     cs::Formula...
 )
     return ∨(c1, ∨(c2, c3, cs...))
-end
Note
To allow for the composition of Formulas of different types, promotion rules should be provided.
See also Formula, Connective.
source
We are ready to see how logical formulas are represented using syntax trees
SoleLogics.SyntaxTree — Type
abstract type SyntaxTree <: SyntaxStructure end
Abstract type for syntax trees; that is, syntax leaves (see SyntaxLeaf, such as Truth values and Atoms), and their composition via Connectives (i.e., SyntaxBranch).
Note that SyntaxTree are ranked trees, and (should) implement AbstractTrees interface.
Interface
  • children(φ::SyntaxTree)::NTuple{N,SyntaxTree} where N
  • token(φ::SyntaxTree)::Connective
  • See also SyntaxStructure
Utility functions
  • tokentype(φ::SyntaxTree)
  • arity(φ::SyntaxTree)::Int
Other utility functions (requiring a walk of the tree)
  • Base.in(tok::SyntaxToken, φ::SyntaxTree)::Bool
  • height(φ::SyntaxTree)::Int
  • tokens(φ::SyntaxTree)::AbstractVector{<:SyntaxToken}
  • atoms(φ::SyntaxTree)::AbstractVector{<:AbstractAtom}
  • truths(φ::SyntaxTree)::AbstractVector{<:Truth}
  • leaves(φ::SyntaxTree)::AbstractVector{<:SyntaxLeaf}
  • connectives(φ::SyntaxTree)::AbstractVector{<:Connective}
  • operators(φ::SyntaxTree)::AbstractVector{<:Operator}
  • ntokens(φ::SyntaxTree)::Int
  • natoms(φ::SyntaxTree)::Int
  • ntruths(φ::SyntaxTree)::Int
  • nleaves(φ::SyntaxTree)::Int
  • nconnectives(φ::SyntaxTree)::Int
  • noperators(φ::SyntaxTree)::Int
  • tokenstype(φ::SyntaxTree)
  • atomstype(φ::SyntaxTree)
  • truthstype(φ::SyntaxTree)
  • leavestype(φ::SyntaxTree)
  • connectivestype(φ::SyntaxTree)
  • operatorstype(φ::SyntaxTree)
  • composeformulas(c::Connective, φs::NTuple{N,SyntaxTree})
See also SyntaxLeaf, SyntaxBranch, SyntaxStructure, Formula.
source
SoleLogics.SyntaxLeaf — Type
abstract type SyntaxLeaf <: SyntaxStructure end
An atomic logical element, like a Truth value or an Atom. SyntaxLeafs have arity equal to zero, meaning that they are not allowed to have children in tree-like syntactic structures.
Interface
  • syntaxstring(s::SyntaxLeaf; kwargs...)::String
  • dual(s::SyntaxLeaf)::SyntaxLeaf
  • hasdual(s::SyntaxLeaf)::Bool
See also SyntaxStructure,  arity, SyntaxBranch.
source
SoleLogics.dual — Method
dual(tok::SyntaxToken)
Return the dual of a syntax token.
If tok is an Operator of arity n, the dual dtok is such that, on a Boolean algebra, tok(ch_1, ..., ch_n) ≡ ¬dtok(¬ch_1, ..., ¬ch_n).
Duality can be used to perform syntactic simplifications on formulas. For example, since ∧ and ∨ are duals, ¬(¬p ∧ ¬q) can be simplified to (p ∧ q) (De Morgan's law). Duality also applies to operators with existential/universal semantics (◊/□), to Truth values (⊤/⊥), and to Atoms.
Implementation
When providing a dual for an operator of type O, please also provide:
hasdual(::O) = true
The dual of an Atom (that is, the atom with inverted semantics) is defined as:
dual(p::Atom{V}) where {V} = Atom(dual(value(p)))
As such, hasdual(::V) and dual(::V) should be defined when wrapping objects of type A.
See also normalize, SyntaxToken.
source
SoleLogics.Atom — Type
struct Atom{V} <: AbstractAtom
+end
Note
To allow for the composition of Formulas of different types, promotion rules should be provided.
See also Formula, Connective.
source
We are ready to see how logical formulas are represented using syntax trees
SoleLogics.SyntaxTree — Type
abstract type SyntaxTree <: SyntaxStructure end
Abstract type for syntax trees; that is, syntax leaves (see SyntaxLeaf, such as Truth values and Atoms), and their composition via Connectives (i.e., SyntaxBranch).
Note that SyntaxTree are ranked trees, and (should) implement AbstractTrees interface.
Interface
  • children(φ::SyntaxTree)::NTuple{N,SyntaxTree} where N
  • token(φ::SyntaxTree)::Connective
  • See also SyntaxStructure
Utility functions
  • tokentype(φ::SyntaxTree)
  • arity(φ::SyntaxTree)::Int
Other utility functions (requiring a walk of the tree)
  • Base.in(tok::SyntaxToken, φ::SyntaxTree)::Bool
  • height(φ::SyntaxTree)::Int
  • tokens(φ::SyntaxTree)::AbstractVector{<:SyntaxToken}
  • atoms(φ::SyntaxTree)::AbstractVector{<:AbstractAtom}
  • truths(φ::SyntaxTree)::AbstractVector{<:Truth}
  • leaves(φ::SyntaxTree)::AbstractVector{<:SyntaxLeaf}
  • connectives(φ::SyntaxTree)::AbstractVector{<:Connective}
  • operators(φ::SyntaxTree)::AbstractVector{<:Operator}
  • ntokens(φ::SyntaxTree)::Int
  • natoms(φ::SyntaxTree)::Int
  • ntruths(φ::SyntaxTree)::Int
  • nleaves(φ::SyntaxTree)::Int
  • nconnectives(φ::SyntaxTree)::Int
  • noperators(φ::SyntaxTree)::Int
  • tokenstype(φ::SyntaxTree)
  • atomstype(φ::SyntaxTree)
  • truthstype(φ::SyntaxTree)
  • leavestype(φ::SyntaxTree)
  • connectivestype(φ::SyntaxTree)
  • operatorstype(φ::SyntaxTree)
  • composeformulas(c::Connective, φs::NTuple{N,SyntaxTree})
See also SyntaxLeaf, SyntaxBranch, SyntaxStructure, Formula.
source
SoleLogics.SyntaxLeaf — Type
abstract type SyntaxLeaf <: SyntaxStructure end
An atomic logical element, like a Truth value or an Atom. SyntaxLeafs have arity equal to zero, meaning that they are not allowed to have children in tree-like syntactic structures.
Interface
  • syntaxstring(s::SyntaxLeaf; kwargs...)::String
  • dual(s::SyntaxLeaf)::SyntaxLeaf
  • hasdual(s::SyntaxLeaf)::Bool
See also SyntaxStructure,  arity, SyntaxBranch.
source
SoleLogics.dual — Method
dual(tok::SyntaxToken)
Return the dual of a syntax token.
If tok is an Operator of arity n, the dual dtok is such that, on a Boolean algebra, tok(ch_1, ..., ch_n) ≡ ¬dtok(¬ch_1, ..., ¬ch_n).
Duality can be used to perform syntactic simplifications on formulas. For example, since ∧ and ∨ are duals, ¬(¬p ∧ ¬q) can be simplified to (p ∧ q) (De Morgan's law). Duality also applies to operators with existential/universal semantics (◊/□), to Truth values (⊤/⊥), and to Atoms.
Implementation
When providing a dual for an operator of type O, please also provide:
hasdual(::O) = true
The dual of an Atom (that is, the atom with inverted semantics) is defined as:
dual(p::Atom{V}) where {V} = Atom(dual(value(p)))
As such, hasdual(::V) and dual(::V) should be defined when wrapping objects of type A.
See also normalize, SyntaxToken.
source
SoleLogics.Truth — Type
abstract type Truth <: SyntaxLeaf end
Abstract type for syntax leaves representing values of a lattice algebra. In Boolean logic, the two BooleanTruth values TOP (⊤) and BOT (⊥) are used.
See also BooleanTruth.
Interface
  • syntaxstring(s::Truth; kwargs...)::String
  • dual(s::Truth)::Truth
  • hasdual(s::Truth)::Bool
  • istop(t::Truth)::Bool
  • isbot(t::Truth)::Bool
  • precedes(t1::Truth, t2::Truth)::Bool
  • truthmeet(t1::Truth, t2::Truth)::Truth
  • truthjoin(t1::Truth, t2::Truth)::Truth
Implementation
A three-valued algebra, that is, an algebra with three truth values (top, bottom and unknown), can be based on the following Truth value definitions:
import SoleLogics: precedes
+end
Simplest atom implementation, wrapping a value.
See also AbstractAtom, value, check, SyntaxToken.
source
SoleLogics.Truth — Type
abstract type Truth <: SyntaxLeaf end
Abstract type for syntax leaves representing values of a lattice algebra. In Boolean logic, the two BooleanTruth values TOP (⊤) and BOT (⊥) are used.
See also BooleanTruth.
Interface
  • syntaxstring(s::Truth; kwargs...)::String
  • dual(s::Truth)::Truth
  • hasdual(s::Truth)::Bool
  • istop(t::Truth)::Bool
  • isbot(t::Truth)::Bool
  • precedes(t1::Truth, t2::Truth)::Bool
  • truthmeet(t1::Truth, t2::Truth)::Truth
  • truthjoin(t1::Truth, t2::Truth)::Truth
Implementation
A three-valued algebra, that is, an algebra with three truth values (top, bottom and unknown), can be based on the following Truth value definitions:
import SoleLogics: precedes
 
 abstract type ThreeVTruth <: Truth end
 
@@ -88,7 +88,7 @@
 precedes(::ThreeUnknown, ::ThreeTop) = true
 precedes(::ThreeTop, ::ThreeBot) = false
 precedes(::ThreeUnknown, ::ThreeBot) = false
-precedes(::ThreeTop, ::ThreeUnknown) = false
Note that precedes is used to define the (partial) order between Truth values.
See also Connective, BooleanTruth.
source
Similarly to the Connectives case, Truth explanation could be unfamiliar at first sight. At the moment, what is of our interest is that SoleLogics provides us a simple interface to create custom, complex at will, algebras without worrying about adapting all the underlying algorithms (e.g., formulas generation, parsing, model checking etc.).
SoleLogics.istop — Method
istop(::Truth)::Bool
Return true if the Truth value is the top of its algebra. For example, in the crisp case, with Bool truth values, it is:
istop(t::Bool)::Bool = (t == true)
See also isbot, Truth.
source
SoleLogics.isbot — Method
isbot(::Truth)::Bool
Return true if the Truth value is the bottom of its algebra. For example, in the crisp case, with Bool truth values, it is:
isbot(t::Bool)::Bool = (t == false)
See also istop, Truth.
source
The union of Connectives and Truth values are exactly what is called logical operators, or simply Operator. In SoleLogics, logical operators are splitted in two parts to highlight some differences that always holds (e.g., Truth values arity is always 0, while Connectives arity is always greater than 0); apart from this technical decision, many dispatches are defined using the more general union type Operator.
An Operator can be used to compose syntax tokens (e.g., Atoms), SyntaxTrees and/or Formulas.
    ¬(Atom(1)) ∨ Atom(1) ∧ ⊤
+precedes(::ThreeTop, ::ThreeUnknown) = false
Note that precedes is used to define the (partial) order between Truth values.
See also Connective, BooleanTruth.
source

Similarly to the Connectives case, Truth explanation could be unfamiliar at first sight. At the moment, what is of our interest is that SoleLogics provides us a simple interface to create custom, complex at will, algebras without worrying about adapting all the underlying algorithms (e.g., formulas generation, parsing, model checking etc.).

SoleLogics.istop — Method
istop(::Truth)::Bool

Return true if the Truth value is the top of its algebra. For example, in the crisp case, with Bool truth values, it is:

istop(t::Bool)::Bool = (t == true)

See also isbot, Truth.

source
SoleLogics.isbot — Method
isbot(::Truth)::Bool

Return true if the Truth value is the bottom of its algebra. For example, in the crisp case, with Bool truth values, it is:

isbot(t::Bool)::Bool = (t == false)

See also istop, Truth.

source

The union of Connectives and Truth values are exactly what is called logical operators, or simply Operator. In SoleLogics, logical operators are splitted in two parts to highlight some differences that always holds (e.g., Truth values arity is always 0, while Connectives arity is always greater than 0); apart from this technical decision, many dispatches are defined using the more general union type Operator.

An Operator can be used to compose syntax tokens (e.g., Atoms), SyntaxTrees and/or Formulas.

    ¬(Atom(1)) ∨ Atom(1) ∧ ⊤
     ∧(⊤,⊤)
     ⊤()

The internal nodes in a SyntaxTree definitely have ariety greater than 0, and thus, cannot wrap Atoms nor Truth values. To clearly distinguish internal nodes and leaves, the SyntaxBranch type is defined, making each SyntaxTree arity-complaint.

Semantics Basics

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

See also check, AbstractAssignment, AbstractKripkeStructure.

source

Semantics Basics

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

See also check, AbstractAssignment, AbstractKripkeStructure.

source
+false

See also interpret, Formula, AbstractInterpretation, TruthDict.

source diff --git a/dev/hands-on/index.html b/dev/hands-on/index.html index b6709a7..bfd9b9d 100644 --- a/dev/hands-on/index.html +++ b/dev/hands-on/index.html @@ -1,2 +1,2 @@ -Hands On · SoleLogics.jl
GitHub

    TODO: get inspiration from Gio pluto tutorial

    +Hands On · SoleLogics.jl
    GitHub

      TODO: get inspiration from Gio pluto tutorial

      diff --git a/dev/index.html b/dev/index.html index b78ba4b..4cf314f 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,3 +1,3 @@ Home · SoleLogics.jl
      GitHub

      SoleLogics

      Welcome to the documentation for SoleLogics.jl, a Julia package for computational logic. To let you better orient yourself while understanding SoleLogics' structure, each chapter will begin with a little summary of what you are going to learn, in the form of small type-hierarchy trees that will grow during your reading journey. To see a complete map of SoleLogics.jl types and structures, please refer to Complete Exports Map.

      Feature Summary

      SoleLogics.jl allows manipulation of:

      • Syntax tokens (e.g., atoms, logical constants (e.g., operators and truth values), etc.);
      • Alphabets & context-free logical grammars (e.g., normal forms);
      • Algebras (e.g., crisp, fuzzy, many-valued);
      • Logics (e.g., propositional, (multi)modal);
      • Formulas (e.g., syntax trees, DNFs, CNFs): random generation, parsing, minimization;
      • Interpretations (e.g., propositional assignments, Kripke structures);
      • Algorithms for evaluating the truth of a formula on an interpretation (model checking);
      • Interfaces to Z3, for evaluating the validity/satisfiability of a propositional formula.

      Installation

      To install SoleLogics.jl, use the Julia package manager:

      using Pkg
-Pkg.add("SoleLogics")

      About

      SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning, originally designed for machine learning based on modal logics (see Eduard I. Stan's PhD thesis 'Foundations of Modal Symbolic Learning' here).

      More on Sole:

      The package is developed by the ACLAI Lab @ University of Ferrara.

      Complete Types Hierarchy Map

      Here is a map of SoleLogics' most important types and structures. Feels overwhelming? Don't worry, if you are not practical with SoleLogics, this is useful to just know what definitions exist and hints at a glance how types are related to each other.

      +Pkg.add("SoleLogics")

      About

      SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning, originally designed for machine learning based on modal logics (see Eduard I. Stan's PhD thesis 'Foundations of Modal Symbolic Learning' here).

      More on Sole:

      The package is developed by the ACLAI Lab @ University of Ferrara.

      Complete Types Hierarchy Map

      Here is a map of SoleLogics' most important types and structures. Feels overwhelming? Don't worry, if you are not practical with SoleLogics, this is useful to just know what definitions exist and hints at a glance how types are related to each other.

      diff --git a/dev/many-valued-logics/index.html b/dev/many-valued-logics/index.html index 3ae75f2..2f62bc3 100644 --- a/dev/many-valued-logics/index.html +++ b/dev/many-valued-logics/index.html @@ -1,108 +1,108 @@ -Many-valued logics · SoleLogics.jl
      GitHub

      Introduction

      SoleLogics also provides tools to work with many-valued logics (e.g., fuzzy logics), that is, logics with more truth values other than the classical Boolean ones ⊤ and ⊥. With many-valued logics, the truth values are elements of a bounded lattice, providing a partial order between them, which encodes a truer than relation.

      Most of the tools for dealing with these logics can be accessed by importing the ManyValuedLogics submodule:

      using SoleLogics.ManyValuedLogics

      Operation

      SoleLogics.ManyValuedLogics.BinaryOperation — Type
      struct BinaryOperation{T<:Truth, D<:AbstractVector{T}} <: Operation
+Many-valued logics · SoleLogics.jl
      GitHub
      Introduction
      SoleLogics also provides tools to work with many-valued logics (e.g., fuzzy logics), that is, logics with more truth values other than the classical Boolean ones ⊤ and ⊥. With many-valued logics, the truth values are elements of a bounded lattice, providing a partial order between them, which encodes a truer than relation.
      Most of the tools for dealing with these logics can be accessed by importing the ManyValuedLogics submodule:
      using SoleLogics.ManyValuedLogics
      Operation
      SoleLogics.ManyValuedLogics.BinaryOperation — Type
      struct BinaryOperation{T<:Truth, D<:AbstractVector{T}} <: Operation
     domain::D
     truthtable::AbstractDict{Tuple{T, T}, T}
-end
      A binary operation on a set S is a mapping of the elements of the Cartesian product S × S → S. The closure property of a binary operation expresses the existence of a result for the operation given any pair of operands. Binary operations are required to be defined on all elements of S × S.
      See also Operation, arity.
      source
      Axiom
      SoleLogics.ManyValuedLogics.Axiom — Type
      struct Axiom{Symbol} end
      An axiom is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. Axioms aim to capture what is special about a particular structure (or set of structures).
      See also checkaxiom.
      source
      SoleLogics.ManyValuedLogics.checkaxiom — Function
      function checkaxiom(a::Axiom, args...)
      Check if axiom a is satisfied.
      See also Axiom.
      source
      function checkaxiom(
+end
      A binary operation on a set S is a mapping of the elements of the Cartesian product S × S → S. The closure property of a binary operation expresses the existence of a result for the operation given any pair of operands. Binary operations are required to be defined on all elements of S × S.
      See also Operation, arity.
      source
      Axiom
      SoleLogics.ManyValuedLogics.Axiom — Type
      struct Axiom{Symbol} end
      An axiom is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. Axioms aim to capture what is special about a particular structure (or set of structures).
      See also checkaxiom.
      source
      SoleLogics.ManyValuedLogics.checkaxiom — Function
      function checkaxiom(a::Axiom, args...)
      Check if axiom a is satisfied.
      See also Axiom.
      source
      function checkaxiom(
     ::typeof(Commutativity),
     o::BinaryOperation{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      A binary operation * on a set S is called commutative if x * y = y * x ∀ x, y ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      A binary operation * on a set S is called commutative if x * y = y * x ∀ x, y ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(Associativity),
     o::BinaryOperation{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      A binary operation * on a set S is called associative if it satisfies the associative law: (x * y) * z = x * (y * z) ∀ x, y, z ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      A binary operation * on a set S is called associative if it satisfies the associative law: (x * y) * z = x * (y * z) ∀ x, y, z ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(AbsorptionLaw),
     o1::BinaryOperation{T,D},
     o2::BinaryOperation{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      The absorption law or absorption identity is an identity linking a pair of binary operations. Two binary operations, * and ⋅, are said to be connected by the absotprion law if a * (a ⋅ b) = a ⋅ (a * b) = a.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      The absorption law or absorption identity is an identity linking a pair of binary operations. Two binary operations, * and ⋅, are said to be connected by the absotprion law if a * (a ⋅ b) = a ⋅ (a * b) = a.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(LeftIdentity),
     o::BinaryOperation{T,D},
     e::T
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a left identity if e * s = s ∀ s ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a left identity if e * s = s ∀ s ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(RightIdentity),
     o::BinaryOperation{T,D},
     e::T
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a right identity if s * e = s ∀ s ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a right identity if s * e = s ∀ s ∈ S.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(IdentityElement),
     o::BinaryOperation{T,D},
     e::T
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      An identity element or neutral element of a binary operation is an element that leaves unchanged every element when the operation is applied. I.e., let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a two-sided identity, or simply identity, if e is both a left identity and a right identity.
      See also Axiom, BinaryOperation, LeftIdentity, RightIdentity.
      source
      function checkaxiom(a::Axiom, m::Monoid{T,D}) where {T<:Truth, D<:AbstractVector{T}}
      Check if axiom a is satisfied by the operation of the monoid m.
      See also Axiom, Monoid.
      source
      function checkaxiom(
+}
      An identity element or neutral element of a binary operation is an element that leaves unchanged every element when the operation is applied. I.e., let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a two-sided identity, or simply identity, if e is both a left identity and a right identity.
      See also Axiom, BinaryOperation, LeftIdentity, RightIdentity.
      source
      function checkaxiom(a::Axiom, m::Monoid{T,D}) where {T<:Truth, D<:AbstractVector{T}}
      Check if axiom a is satisfied by the operation of the monoid m.
      See also Axiom, Monoid.
      source
      function checkaxiom(
     ::typeof(RightResidual),
     m::Monoid{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S such that x ⋅ y ≤ z.
      See also Axiom, Monoid.
      source
      function checkaxiom(
+}
      Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S such that x ⋅ y ≤ z.
      See also Axiom, Monoid.
      source
      function checkaxiom(
     ::typeof(LeftResidual),
     m::Monoid{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check that ∀ x ∈ S there exists for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.
      See also Axiom, Monoid.
      source
      function checkaxiom(
+}
      Check that ∀ x ∈ S there exists for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.
      See also Axiom, Monoid.
      source
      function checkaxiom(
     ::typeof(ResiduationProperty),
     m::Monoid{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S and for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.
      See also Axiom, Monoid.
      source
      function checkaxiom(
+}
      Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S and for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.
      See also Axiom, Monoid.
      source
      function checkaxiom(
     ::typeof(Implication1),
     o::BinaryOperation{T,D},
     top::Truth
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, a → a = ⊤ holds.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, a → a = ⊤ holds.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(Implication2),
     o1::BinaryOperation{T,D},
     o2::BinaryOperation{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and two binary operations ∧ (o1) and → (o2), a ∧ (a → b) = a ∧ b holds.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and two binary operations ∧ (o1) and → (o2), a ∧ (a → b) = a ∧ b holds.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(Implication3),
     o1::BinaryOperation{T,D},
     o2::BinaryOperation{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and two binary operations ∧ (o1) and → (o2), b ∧ (a → b) = b holds.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
+}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and two binary operations ∧ (o1) and → (o2), b ∧ (a → b) = b holds.
      See also Axiom, BinaryOperation.
      source
      function checkaxiom(
     ::typeof(DistributiveLaw),
     o1::BinaryOperation{T,D},
     o2::BinaryOperation{T,D}
 ) where {
     T<:Truth,
     D<:AbstractVector{T}
-}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ⋅ and *, ⋅ is distributive over * if ∀ a, b, c ∈ L: a ⋅ (b * c) = (a ⋅ b) * (a ⋅ c).
      See also Axiom, BinaryOperation.
      source
      Common axioms
      Finite algebra
      Monoid
      SoleLogics.ManyValuedLogics.Monoid — Type
      struct Monoid{T<:Truth, D<:AbstractVector{T}}
+}
      Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ⋅ and *, ⋅ is distributive over * if ∀ a, b, c ∈ L: a ⋅ (b * c) = (a ⋅ b) * (a ⋅ c).
      See also Axiom, BinaryOperation.
      source
      Common axioms
      Finite algebra
      Monoid
      SoleLogics.ManyValuedLogics.Monoid — Type
      struct Monoid{T<:Truth, D<:AbstractVector{T}}
     operation::BinaryOperation{T,D}
     identityelement::T
-end
      A monoid (S, ⋅, e) is a set S equipped with a binary operation S × S → S, denoted as ⋅, satisfying the following axiomatic identities:
      • (Associativity) ∀ a, b, c ∈ S, the equation (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c) holds.
      • (Identity element) There exists an element e ∈ L such that for every element a ∈ S, the equalities e ⋅ a = a and a ⋅ e = a hold. 
      The identity element of a monoid is unique.
      See also BinaryOperation, Axiom, checkaxiom, checkmonoidaxioms, Associativity, IdentityElement.
      source
      SoleLogics.ManyValuedLogics.CommutativeMonoid — Type
      struct CommutativeMonoid{T<:Truth, D<:AbstractVector{T}}
+end
      A monoid (S, ⋅, e) is a set S equipped with a binary operation S × S → S, denoted as ⋅, satisfying the following axiomatic identities:
      • (Associativity) ∀ a, b, c ∈ S, the equation (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c) holds.
      • (Identity element) There exists an element e ∈ L such that for every element a ∈ S, the equalities e ⋅ a = a and a ⋅ e = a hold. 
      The identity element of a monoid is unique.
      See also BinaryOperation, Axiom, checkaxiom, checkmonoidaxioms, Associativity, IdentityElement.
      source
      Finite lattice
      Finite lattice
      SoleLogics.ManyValuedLogics.FiniteLattice — Type
      struct FiniteLattice{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
     join::BinaryOperation{T,D}
     meet::BinaryOperation{T,D}
-end
      A finite lattice is a lattice defined over a finite set.
      A lattice is an algebraic structure (L, ∨, ∧) consisting of a set L and two binary, commutative and associative operations ∨ and ∧ on L satisfying the following axiomatic identities for all elements a, b ∈ L (sometimes called absorption laws):
      • a ∨ (a ∧ b) = a
      • a ∧ (a ∨ b) = a
      See also FiniteAlgebra, BinaryOperation.
      source
      SoleLogics.ManyValuedLogics.FiniteBoundedLattice — Type
      struct FiniteBoundedLattice{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
+end
      A finite lattice is a lattice defined over a finite set.
      A lattice is an algebraic structure (L, ∨, ∧) consisting of a set L and two binary, commutative and associative operations ∨ and ∧ on L satisfying the following axiomatic identities for all elements a, b ∈ L (sometimes called absorption laws):
      • a ∨ (a ∧ b) = a
      • a ∧ (a ∨ b) = a
      See also FiniteAlgebra, BinaryOperation.
      source
      SoleLogics.ManyValuedLogics.FiniteBoundedLattice — Type
      struct FiniteBoundedLattice{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
     join::BinaryOperation{T,D}
     meet::BinaryOperation{T,D}
     bot::T
     top::T
-end
      A finite bounded lattice is a bounded lattice defined over a finite set.
      A bounded lattice is an algebraic structure (L, ∨, ∧, ⊥, ⊤) such that (L, ∨, ∧) is a lattice, the bottom element ⊥ is the identity element for the join operation ∨, and the top element ⊤ is the identity element for the meet operation ∧:
      • a ∨ ⊥ = a
      • a ∧ ⊤ = a
      See also FiniteLattice.
      source
      SoleLogics.ManyValuedLogics.FiniteResiduatedLattice — Type
      struct FiniteResiduatedLattice{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
+end
      A finite bounded lattice is a bounded lattice defined over a finite set.
      A bounded lattice is an algebraic structure (L, ∨, ∧, ⊥, ⊤) such that (L, ∨, ∧) is a lattice, the bottom element ⊥ is the identity element for the join operation ∨, and the top element ⊤ is the identity element for the meet operation ∧:
      • a ∨ ⊥ = a
      • a ∧ ⊤ = a
      See also FiniteLattice.
      source
      SoleLogics.ManyValuedLogics.FiniteResiduatedLattice — Type
      struct FiniteResiduatedLattice{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
     domain::D
     join::BinaryOperation{T,D}
     meet::BinaryOperation{T,D}
@@ -111,7 +111,7 @@
     leftresidual::BinaryOperation{T,D}
     bot::T
     top::T
-end
      A residuated lattice is an algebraic structure L = (L, ∨, ∧, ⋅, e) such that:
      • (L, ∨, ∧) is a lattice
      • (L, ⋅, e) is a monoid
      • ∀ x ∈ L there exists for every x ∈ L a greatest y ∈ L and for every y ∈ L a greatest x ∈ L such that x ⋅ y ≤ z
      See also FiniteBoundedLattice, 
      source
      Finite algebra varieties
      SoleLogics.ManyValuedLogics.FiniteFLewAlgebra — Type
      struct FiniteFLewAlgebra{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
+end
      A residuated lattice is an algebraic structure L = (L, ∨, ∧, ⋅, e) such that:
      • (L, ∨, ∧) is a lattice
      • (L, ⋅, e) is a monoid
      • ∀ x ∈ L there exists for every x ∈ L a greatest y ∈ L and for every y ∈ L a greatest x ∈ L such that x ⋅ y ≤ z
      See also FiniteBoundedLattice, 
      source
      Finite algebra varieties
      SoleLogics.ManyValuedLogics.FiniteFLewAlgebra — Type
      struct FiniteFLewAlgebra{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
     domain::D
     join::BinaryOperation{T,D}
     meet::BinaryOperation{T,D}
@@ -119,14 +119,14 @@
     implication::BinaryOperation{T,D}
     bot::T
     top::T
-end
      An FLew-algebra is an algebra (L, ∨, ∧, ⋅, →, ⊥, ⊤), where
      • (L, ∨, ∧, ⊥, ⊤) is a bounded lattice with top element ⊤ and bottom element ⊥
      • (L, ⋅, ⊤) is a commutative monoid
      • The residuation property holds: x ⋅ y ≤ z iff x ≤ y → z
      See also FiniteBoundedLattice, CommutativeMonoid.
      source
      SoleLogics.ManyValuedLogics.FiniteHeytingAlgebra — Type
      struct FiniteHeytingAlgebra{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
+end
      An FLew-algebra is an algebra (L, ∨, ∧, ⋅, →, ⊥, ⊤), where
      • (L, ∨, ∧, ⊥, ⊤) is a bounded lattice with top element ⊤ and bottom element ⊥
      • (L, ⋅, ⊤) is a commutative monoid
      • The residuation property holds: x ⋅ y ≤ z iff x ≤ y → z
      See also FiniteBoundedLattice, CommutativeMonoid.
      source
      SoleLogics.ManyValuedLogics.FiniteHeytingAlgebra — Type
      struct FiniteHeytingAlgebra{T<:Truth, D<:AbstractVector{T}} <: FiniteAlgebra{T,D}
     domain::D
     join::BinaryOperation{T,D}
     meet::BinaryOperation{T,D}
     implication::BinaryOperation{T,D}
     bot::T
     top::T
-end
      A Heyting algebra (H, ∨, ∧, →, ⊥, ⊤) is a bounded lattice (H, ∨, ∧, ⊥, ⊤) equipped with a binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).
      Given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, these together form a Heyting algebra if and only if the following hold:
      • (Implication1) a → a = ⊤
      • (Implication2) a ∧ (a → b) = a ∧ b
      • (Implication3) b ∧ (a → b) = b
      • (Distributive law for →) a → (b ∧ c) = (a → b) ∧ (a → c)
      See also FiniteBoundedLattice, BinaryOperation.
      source
      Order utilities
      SoleLogics.ManyValuedLogics.precedeq — Function
      function precedeq(
+end
      A Heyting algebra (H, ∨, ∧, →, ⊥, ⊤) is a bounded lattice (H, ∨, ∧, ⊥, ⊤) equipped with a binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).
      Given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, these together form a Heyting algebra if and only if the following hold:
      • (Implication1) a → a = ⊤
      • (Implication2) a ∧ (a → b) = a ∧ b
      • (Implication3) b ∧ (a → b) = b
      • (Distributive law for →) a → (b ∧ c) = (a → b) ∧ (a → c)
      See also FiniteBoundedLattice, BinaryOperation.
      source
      Order utilities
      SoleLogics.ManyValuedLogics.precedeq — Function
      function precedeq(
     l::L,
     t1::T1,
     t2::T2
@@ -136,7 +136,7 @@
     L<:FiniteAlgebra{T,D},
     T1<:Truth,
     T2<:Truth
-}
      Return true if t1 ≤ t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.
      See also precedes, succeedes, succeedeq.
      source
      SoleLogics.ManyValuedLogics.precedes — Function
      function precedes(
     l::L,
     t1::T1,
     t2::T2
@@ -146,7 +146,7 @@
     L<:FiniteAlgebra{T,D},
     T1<:Truth,
     T2<:Truth
-}
      Return true if t1 < t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.
      See also precedeq, succeedes, succeedeq.
      source
      SoleLogics.ManyValuedLogics.succeedeq — Function
      function succeedeq(
     l::L,
     t1::T1,
     t2::T2
@@ -156,7 +156,7 @@
     L<:FiniteAlgebra{T,D},
     T1<:Truth,
     T2<:Truth
-}
      Return true if t1 ≥ t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.
      See also precedes, precedeq, succeedes.
      source
      SoleLogics.ManyValuedLogics.succeedes — Function
      function succeedeq(
     l::L,
     t1::T,
     t2::T
@@ -164,4 +164,4 @@
     T<:Truth,
     D<:AbstractVector{T},
     L<:FiniteAlgebra{T,D}
-}
      Return true if t1 > t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.
      See also precedes, precedeq, succeedeq.
      source
      
+}

      Return true if t1 > t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.

      See also precedes, precedeq, succeedeq.

      source
      diff --git a/dev/modal-logic/index.html b/dev/modal-logic/index.html index 5a8a295..455e0ce 100644 --- a/dev/modal-logic/index.html +++ b/dev/modal-logic/index.html @@ -18,17 +18,17 @@ phi = ∧(q, ∧(◊(p),◊(◊(q)))) # \wedge+TAB can also be written as CONJUNCTION, while \lozenge+TAB is called DIAMOND and is a modal operator -check(phi, kripkestructure, worlds[1]) # prints true

      By reading the following sections, you will better grasp how Worlds are defined, as well as relations (AbstractRelation), how those two concepts are bound togheter in AbstractFrames and KripkeStructures. You will also understand how to access one world from another by using (or implementing) Connectives such as ◊ (or DIAMOND) and the accessibles method.

      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.World — Type
      struct World{T} <: AbstractWorld
+check(phi, kripkestructure, worlds[1]) # prints true

      By reading the following sections, you will better grasp how Worlds are defined, as well as relations (AbstractRelation), how those two concepts are bound togheter in AbstractFrames and KripkeStructures. You will also understand how to access one world from another by using (or implementing) Connectives such as ◊ (or DIAMOND) and the accessibles method.

      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.World — Type
      struct World{T} <: AbstractWorld
     name::T
-end

      A world that is solely identified by its name. This can be useful when instantiating the underlying graph of a modal frame in an explicit way.

      See also OneWorld, AbstractWorld.

      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,),);
+end

      A world that is solely identified by its name. This can be useful when instantiating the underlying graph of a modal frame in an explicit way.

      See also OneWorld, AbstractWorld.

      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,),);
 
 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.

      See also issymmetric, isreflexive, istransitive, isgrounding, arity, syntaxstring, converse, hasconverse, istoone, identityrel, globalrel, accessibles, AbstractKripkeStructure, AbstractFrame, AbstractWorld.

      source
      SoleLogics.AbstractMultiModalFrame — Type
      abstract type AbstractMultiModalFrame{W<:AbstractWorld} <: AbstractFrame{W} end

      A frame of a multi-modal logic, that is, a modal logic based on a set of accessibility relations.

      Implementation

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

      See also AbstractUniModalFrame, AbstractFrame.

      source
      SoleLogics.AbstractMultiModalFrame — Type
      abstract type AbstractMultiModalFrame{W<:AbstractWorld} <: AbstractFrame{W} end

      A frame of a multi-modal logic, that is, a modal logic based on a set of accessibility relations.

      Implementation

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

      See also AbstractUniModalFrame, AbstractFrame.

      source
      SoleLogics.KripkeStructure — Type
      struct KripkeStructure{
     FR<:AbstractFrame,
     MAS<:AbstractDict
 } <: AbstractKripkeStructure
     frame::FR
     assignment::AS
-end

      Type for representing Kripke structures. explicitly; it wraps a frame, and an abstract dictionary that assigns an interpretation to each world.

      source
      SoleLogics.ismodal — Method
      ismodal(::Type{<:Connective})::Bool = false
+end

      Type for representing Kripke structures. explicitly; it wraps a frame, and an abstract dictionary that assigns an interpretation to each world.

      source
      SoleLogics.ismodal — Method
      ismodal(::Type{<:Connective})::Bool = false
 ismodal(c::Connective)::Bool = ismodal(typeof(c))

      Return whether it is known that an Connective is modal.

      Examples

      julia> ismodal(◊)
 true
 
 julia> ismodal(∧)
-false
      source
      SoleLogics.isbox — Method
      isbox(::Type{<:Connective})::Bool = false
 isbox(c::Connective)::Bool = isbox(typeof(c))

      Return whether it is known that an Connective is a box (i.e., universal) connective.

      Examples

      julia> SoleLogics.isbox(◊)
 false
 
@@ -116,13 +116,13 @@
 false
 
 julia> SoleLogics.isbox(□)
-true
      source
      SoleLogics.DIAMOND — Constant
      const DIAMOND = NamedConnective{:◊}()
 const ◊ = DIAMOND
 ismodal(::typeof(◊)) = true
-arity(::typeof(◊)) = 1

      Logical diamond connective, typically interpreted as the modal existential quantifier. See here.

      See also BOX, NamedConnective, Connective.

      source
      SoleLogics.AbstractRelationalConnective — Type
      abstract type AbstractRelationalConnective{R<:AbstractRelation} <: Connective end

      Abstract type for relational logical connectives. A relational connective allows for semantic quantification across relational structures (e.g., Kripke structures). It has arity equal to the arity of its underlying relation minus one.

      See, for example temporal modal logic.

      See also DiamondRelationalConnective, BoxRelationalConnective, AbstractKripkeStructure, AbstractFrame.

      source
      SoleLogics.relationtype — Method
      relationtype(::AbstractRelationalConnective{R}) where {R<:AbstractRelation} = R
-relation(op::AbstractRelationalConnective) = relationtype(op)()

      Return the underlying relation (and relation type) of the relational connective.

      See also AbstractFrame.

      source
      SoleLogics.AbstractRelationalConnective — Type
      abstract type AbstractRelationalConnective{R<:AbstractRelation} <: Connective end

      Abstract type for relational logical connectives. A relational connective allows for semantic quantification across relational structures (e.g., Kripke structures). It has arity equal to the arity of its underlying relation minus one.

      See, for example temporal modal logic.

      See also DiamondRelationalConnective, BoxRelationalConnective, AbstractKripkeStructure, AbstractFrame.

      source
      SoleLogics.relationtype — Method
      relationtype(::AbstractRelationalConnective{R}) where {R<:AbstractRelation} = R
+relation(op::AbstractRelationalConnective) = relationtype(op)()

      Return the underlying relation (and relation type) of the relational connective.

      See also AbstractFrame.

      source
      SoleLogics.DiamondRelationalConnective — Type
      struct DiamondRelationalConnective{R<:AbstractRelation} <: AbstractRelationalConnective{R} end
 struct BoxRelationalConnective{R<:AbstractRelation} <: AbstractRelationalConnective{R} end

      Singleton types for relational connectives, typically interpreted as the modal existential and universal quantifier, respectively.

      Both connectives can be easily instantiated with relation instances, such as DiamondRelationalConnective(rel), which is a shortcut for DiamondRelationalConnective{typeof(rel)}().

      Examples

      julia> syntaxstring(DiamondRelationalConnective(IA_A))
 "⟨A⟩"
 
@@ -130,9 +130,9 @@
 "[A]"
 
 julia> @assert DiamondRelationalConnective(IA_A) == SoleLogics.dual(BoxRelationalConnective(IA_A))
-

      See also DiamondRelationalConnective, BoxRelationalConnective, syntaxstring, dual, AbstractKripkeStructure, AbstractFrame.

      source
      SoleLogics.diamond — Method
      diamond() = DIAMOND
-diamond(r::AbstractRelation) = DiamondRelationalConnective(r)

      Return either the diamond modal connective from unimodal logic (i.e., ◊), or a a diamond relational connective from a multi-modal logic, wrapping the relation r.

      See also DiamondRelationalConnective, diamond, DIAMOND.

      source
      SoleLogics.box — Method
      box() = BOX
-box(r::AbstractRelation) = BoxRelationalConnective(r)

      Return either the box modal connective from unimodal logic (i.e., □), or a a box relational connective from a multi-modal logic, wrapping the relation r.

      See also BoxRelationalConnective, box, BOX.

      source
      SoleLogics.diamond — Method
      diamond() = DIAMOND
+diamond(r::AbstractRelation) = DiamondRelationalConnective(r)

      Return either the diamond modal connective from unimodal logic (i.e., ◊), or a a diamond relational connective from a multi-modal logic, wrapping the relation r.

      See also DiamondRelationalConnective, diamond, DIAMOND.

      source
      SoleLogics.box — Method
      box() = BOX
+box(r::AbstractRelation) = BoxRelationalConnective(r)

      Return either the box modal connective from unimodal logic (i.e., □), or a a box relational connective from a multi-modal logic, wrapping the relation r.

      See also BoxRelationalConnective, box, BOX.

      source
      SoleLogics.modallogic — Method
      modallogic(;
     alphabet = AlphabetOfAny{String}(),
     operators = [⊤, ⊥, ¬, ∧, ∨, →, ◊, □],
     grammar = CompleteFlatGrammar(AlphabetOfAny{String}(), [⊤, ⊥, ¬, ∧, ∨, →, ◊, □]),
@@ -151,8 +151,8 @@
 julia> modallogic(; alphabet = ["p", "q"]);
 
 julia> modallogic(; alphabet = ExplicitAlphabet([Atom("p"), Atom("q")]));
-

      See also propositionallogic, AbstractAlphabet, AbstractAlgebra.

      source
      SoleLogics.collateworlds — Method
      collateworlds(
     fr::AbstractFrame{W},
     op::Operator,
     t::NTuple{N,WS},
-)::AbstractVector{<:W} where {N,W<:AbstractWorld,WS<:AbstractWorlds}

      For a given crisp frame (truthtype == Bool), return the set of worlds where a composed formula op(φ1, ..., φN) is true, given the N sets of worlds where the each immediate sub-formula is true.

      See also check, iscrisp, Operator, AbstractFrame.

      source
      +)::AbstractVector{<:W} where {N,W<:AbstractWorld,WS<:AbstractWorlds}

      For a given crisp frame (truthtype == Bool), return the set of worlds where a composed formula op(φ1, ..., φN) is true, given the N sets of worlds where the each immediate sub-formula is true.

      See also check, iscrisp, Operator, AbstractFrame.

      source diff --git a/dev/more-on-formulas/index.html b/dev/more-on-formulas/index.html index bdb9372..b40c069 100644 --- a/dev/more-on-formulas/index.html +++ b/dev/more-on-formulas/index.html @@ -2,7 +2,7 @@ More on Formulas · SoleLogics.jl
      GitHub

      More on Formulas

      In this chapter, you are going to learn more on Formula representations that are alternative to syntax trees. As you will see, for example, formulas with specific structure (e.g., normal forms) can be represented in ways that make them more easy to handle, and can lead to great benefits in terms of both computational and memory load.

      We proceed by presenting the random formulae generation engine, parsing and some utility function.

      Recalling the type hierarchy presented in man-core, it is here enriched with the following new types and structures.

      Literals

      Linear Forms

      Linear Forms

      SoleLogics.LeftmostLinearForm — Type
      struct LeftmostLinearForm{C<:Connective,SS<:SyntaxStructure} <: SyntaxStructure
     children::Vector{<:SS}
 end

      A syntax structure representing the foldl of a set of other syntax structure of type SS by means of a connective C. This structure enables a structured instantiation of formulas in conjuctive/disjunctive forms, and conjuctive normal form (CNF) or disjunctive normal form (DNF), defined as:

      const LeftmostConjunctiveForm{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
 const LeftmostDisjunctiveForm{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}
@@ -39,7 +39,7 @@
 SyntaxBranch: ¬(p ∧ q)
 
 julia> tree(nconj ∧ nconj)
-SyntaxBranch: ¬(p ∧ q) ∧ ¬(p ∧ q)

      See also SyntaxStructure, SyntaxTree, LeftmostConjunctiveForm, LeftmostDisjunctiveForm, Literal.

      source

      <!–

      <!–

      SoleLogics.AnchoredFormula — Type
      struct AnchoredFormula{L<:AbstractLogic} <: Formula
     _logic::Base.RefValue{L}
     synstruct::SyntaxStructure
 end

      A formula anchored to a logic of type L, and wrapping a syntax structure. The structure encodes a formula belonging to the grammar of the logic, and the truth of the formula can be evaluated on interpretations of the same logic. Note that, here, the logic is represented by a reference.

      Upon construction, the logic can be passed either directly, or via a RefValue. Additionally, the following keyword arguments may be specified:

      • check_atoms::Bool = false: whether to perform or not a check that the atoms belong to the alphabet of the logic;
      • check_tree::Bool = false: whether to perform or not a check that the formula's syntactic structure honors the grammar (includes the check performed with check_atoms = true);

      Cool feature: a AnchoredFormula can be used for instating other formulas of the same logic. See the examples.

      Examples

      julia> φ = parseformula(AnchoredFormula, "◊(p→q)");
@@ -57,7 +57,7 @@
 julia> @assert ◊ in operators(logic(f2))
 
 julia> @assert ◊ isa operatorstype(logic(f2))
-

      See also AbstractLogic, logic, SyntaxToken, SyntaxBranch, tree.

      source
      SoleLogics.baseformula — Method
      function baseformula(
     φ::Formula;
     infer_logic = true,
     additional_operators::Union{Nothing,Vector{<:Operator}} = nothing,
@@ -77,7 +77,7 @@
  ∨
  →
  ◊
- □
      source
      SoleLogics.parseformula — Function
      parseformula(
     T::Type{AnchoredFormula},
     expr::String,
     additional_operators::Union{Nothing,Vector{<:Operator}} = nothing;
@@ -85,12 +85,12 @@
     grammar::Union{Nothing,AbstractGrammar} = nothing,
     algebra::Union{Nothing,AbstractAlgebra} = nothing,
     kwargs...
-)::AnchoredFormula

      Return a AnchoredFormula which is the result of parsing an expression via the Shunting yard algorithm. By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_CONNECTIVES; additional operators may be provided as a second argument.

      The grammar and algebra of the associated logic is inferred using the baseformula function from the operators encountered in the expression, and those in additional_operators.

      See parseformula, baseformula, BASE_PARSABLE_CONNECTIVES.

      source

      –>

      Random sampling and generation

      Base.rand — Method
      Base.rand(
+)::AnchoredFormula

      Return a AnchoredFormula which is the result of parsing an expression via the Shunting yard algorithm. By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_CONNECTIVES; additional operators may be provided as a second argument.

      The grammar and algebra of the associated logic is inferred using the baseformula function from the operators encountered in the expression, and those in additional_operators.

      See parseformula, baseformula, BASE_PARSABLE_CONNECTIVES.

      source

      –>

      Random sampling and generation

      SoleLogics.randatom — Function
      randatom(
     [rng::Union{Random.AbstractRNG,Integer},]
     a::AbstractAlphabet,
     args...;
@@ -99,7 +99,7 @@
 ExplicitAlphabet{Int64}(Atom{Int64}[Atom{Int64}: 1, Atom{Int64}: 2, Atom{Int64}: 3, Atom{Int64}: 4, Atom{Int64}: 5])
 
 julia> randatom(42, alphabet)
-Atom{Int64}: 4

      See also natoms, AbstractAlphabet.

      source
      randatom(
+Atom{Int64}: 4

      See also natoms, AbstractAlphabet.

      source
      randatom(
     [rng::Union{Random.AbstractRNG,Integer},]
     a::UnionAlphabet;
     atompicking_mode::Symbol=:uniform,
@@ -121,13 +121,13 @@
                 subalphabets_weights=[0.8,0.2]
             ) |> syntaxstring |> vcat |> print
         end
-["6"]["3"]["10"]["7"]["2"]["2"]["6"]["9"]["20"]["16"]

      See also UnionAlphabet.

      source
      StatsBase.sample — Method
      function StatsBase.sample(
     [rng::Union{Integer,AbstractRNG}=Random.GLOBAL_RNG,]
     alphabet::AbstractAlphabet,
     weights::AbstractWeights,
     args...;
     kwargs...
-)

      Sample an Atom from an alphabet, with probabilities proportional to the weights given in weights.

      See also AbstractAlphabet, AbstractWeights, Atom.

      source
      SoleLogics.randformula — Function
      function randformula(
     [T::Type{<:Formula}=SyntaxTree,]
     [rng::Union{Integer,AbstractRNG}=Random.GLOBAL_RNG,]
     height::Integer,
@@ -140,14 +140,14 @@
     alphabet_sample_kwargs::Union{Nothing,AbstractVector}=nothing,
     kwargs...
 )

      Return a pseudo-randomic formula of type T.

      Arguments

      • rng::Union{Intger,AbstractRNG}=Random.GLOBAL_RNG: random number generator;
      • height::Integer: height of the generated structure;
      • alphabet::AbstractAlphabet: collection from which atoms are chosen randomly;
      • operators::AbstractVector{<:Operator}: vector from which legal operators are chosen.

      Keyword Arguments

      • modaldepth::Integer: maximum modal depth;
      • atompicker::Union{Nothing,Function,AbstractWeights,AbstractVector{<:Real}}: method used to pick a random element. For example, this could be Base.rand, StatsBase.sample or an array of integers or an array of StatsBase.AbstractWeights;
      • opweights::Union{Nothing,AbstractWeights,AbstractVector{<:Real}}: operators are sampled with probabilities proportional to this vector (see AbstractWeights of StatsBase package).
      • alphabet_sample_kwargs::AbstractVector: pool of atoms to pull from if the given alphabet is not finite.

      Examples

      julia> syntaxstring(randformula(4, ExplicitAlphabet([1,2]), [NEGATION, CONJUNCTION, IMPLICATION]))
-"¬((¬(¬(2))) → ((1 → 2) → (1 → 2)))"

      See also AbstractAlphabet, AbstractWeights, Atom, Operator, SyntaxBranch, SyntaxTree.

      source
      function randformula(
+"¬((¬(¬(2))) → ((1 → 2) → (1 → 2)))"

      See also AbstractAlphabet, AbstractWeights, Atom, Operator, SyntaxBranch, SyntaxTree.

      source
      function randformula(
     [T::Type{<:Formula}=SyntaxTree,]
     [rng::Union{Integer,AbstractRNG}=Random.GLOBAL_RNG,]
     height::Integer,
     [g::AbstractGrammar,]
     args...;
     kwargs...
-)

      Fallback to randformula, specifying only the height (possibly also a grammar) of the generated SyntaxTree.

      See also AbstractGrammar, randformula(::Integer, ::Union{AbstractVector,AbstractAlphabet}, ::AbstractVector).

      source

      Parsing

      SoleLogics.BASE_PARSABLE_CONNECTIVES — Constant
      const BASE_PARSABLE_CONNECTIVES = SoleLogics.Syntactical[¬, ∧, ∨, →, ◊, □, ⟨G⟩, [G], ⟨=⟩, [=], ⊤, ⊥]

      Vector of (standard) operators that are automatically taken care of when parsing. These are ¬, ∧, ∨, →, ◊, □, ⟨G⟩, [G], ⟨=⟩, [=], ⊤ and ⊥.

      See also parseformula.

      source

      Parsing

      SoleLogics.BASE_PARSABLE_CONNECTIVES — Constant
      const BASE_PARSABLE_CONNECTIVES = SoleLogics.Syntactical[¬, ∧, ∨, →, ◊, □, ⟨G⟩, [G], ⟨=⟩, [=], ⊤, ⊥]

      Vector of (standard) operators that are automatically taken care of when parsing. These are ¬, ∧, ∨, →, ◊, □, ⟨G⟩, [G], ⟨=⟩, [=], ⊤ and ⊥.

      See also parseformula.

      source
      SoleLogics.parseformula — Function
      parseformula(
     [F::Type{<:Formula}=SyntaxTree],
     expr::String,
     additional_operators::Union{Nothing,AbstractVector} = nothing;
@@ -166,7 +166,7 @@
 "¬p ∧ q ∧ ¬s ∧ ¬z"
 
 julia> syntaxstring(parseformula("¬1→0"; atom_parser = (x -> Atom{Float64}(parse(Float64, x)))))
-"(¬1.0) → 0.0"
      Note

      For any Formula type F, this function should be the inverse of syntaxstring; that is, if φ::F then the following should hold, for at least some args, and for every kwargs allowing correct parsing: φ == parseformula(F, syntaxstring(φ, args...; kwargs...), args...; kwargs...).

      See also SyntaxTree, BASE_PARSABLE_CONNECTIVES, syntaxstring.

      source

      Utilities

      Utilities

      SoleLogics.treewalk — Method
      treewalk(
     st::SyntaxTree,
     args...;
     rng::AbstractRNG = Random.GLOBAL_RNG,
@@ -174,14 +174,14 @@
     toleaf::Bool = true,
     returnnode::Bool = false,
     transformnode::Function = nothing
-)::SyntaxTree

      Return a subtree of syntax tree, by following these options:

      • criterion: function used to compute the probability of stopping at a random node;
      • returnnode: true if only the subtree is to be returned;
      • transformnode: function that will be applied to the chosen subtree.
      source
      SoleLogics.subformulas — Method
      subformulas(f::Formula; sorted=true)

      Return all sub-formulas (sorted by size when sorted=true) of a given formula.

      Examples

      julia> syntaxstring.(SoleLogics.subformulas(parseformula("◊((p∧q)→r)")))
+)::SyntaxTree

      Return a subtree of syntax tree, by following these options:

      • criterion: function used to compute the probability of stopping at a random node;
      • returnnode: true if only the subtree is to be returned;
      • transformnode: function that will be applied to the chosen subtree.
      source
      SoleLogics.subformulas — Method
      subformulas(f::Formula; sorted=true)

      Return all sub-formulas (sorted by size when sorted=true) of a given formula.

      Examples

      julia> syntaxstring.(SoleLogics.subformulas(parseformula("◊((p∧q)→r)")))
 6-element Vector{String}:
  "p"
  "q"
  "r"
  "p ∧ q"
  "◊(p ∧ q)"
- "(◊(p ∧ q)) → r"

      See also SyntaxTree), Formula.

      source
      SoleLogics.normalize — Method
      normalize(
     f::Formula;
     profile = :readability,
     remove_boxes = nothing,
@@ -203,10 +203,10 @@
 "¬◊(q ∨ ¬p ∨ r)"
 
 julia> syntaxstring(SoleLogics.normalize(f; profile = :readability, allow_atom_flipping = false))
-"□(¬r ∧ p ∧ ¬q)"

      See also SyntaxTree), Formula.

      source
      SoleLogics.isgrounded — Method
      isgrounded(f::Formula)::Bool

      Return true if the formula is grounded, that is, if it can be inferred from its syntactic structure that, given any frame-based model, the truth value of the formula is the same on every world.

      Examples

      julia> f = parseformula("⟨G⟩p → [G]q");
+"□(¬r ∧ p ∧ ¬q)"

      See also SyntaxTree), Formula.

      source
      SoleLogics.isgrounded — Method
      isgrounded(f::Formula)::Bool

      Return true if the formula is grounded, that is, if it can be inferred from its syntactic structure that, given any frame-based model, the truth value of the formula is the same on every world.

      Examples

      julia> f = parseformula("⟨G⟩p → [G]q");
 
 julia> syntaxstring(f)
 "(⟨G⟩p) → ([G]q)"
 
 julia> SoleLogics.isgrounded(f)
-true

      See also isgrounding), SyntaxTree), Formula.

      source
      +true

      See also isgrounding), SyntaxTree), Formula.

      source diff --git a/dev/more-on-interpretations/index.html b/dev/more-on-interpretations/index.html index 9269603..2b0196d 100644 --- a/dev/more-on-interpretations/index.html +++ b/dev/more-on-interpretations/index.html @@ -1,2 +1,2 @@ -More on Interpretations · SoleLogics.jl
      GitHub
      +More on Interpretations · SoleLogics.jl
      GitHub
      diff --git a/dev/objects.inv b/dev/objects.inv index 1430b5e..da405ab 100644 Binary files a/dev/objects.inv and b/dev/objects.inv differ diff --git a/dev/old-code/many-valued-logics/heyting-algebras/index.html b/dev/old-code/many-valued-logics/heyting-algebras/index.html index af87969..6b9a543 100644 --- a/dev/old-code/many-valued-logics/heyting-algebras/index.html +++ b/dev/old-code/many-valued-logics/heyting-algebras/index.html @@ -11,4 +11,4 @@ HeytingTruth: ⊤ julia> collatetruth(→, (α, β), myalgebra) -HeytingTruth: β

      ```

      +HeytingTruth: β

      ```