diff --git a/dev/NOTE/index.html b/dev/NOTE/index.html index 2672a5f9..cf892b4a 100644 --- a/dev/NOTE/index.html +++ b/dev/NOTE/index.html @@ -1,2 +1,2 @@ -- · SoleLogics.jl

Quick start

make.jl structure is inspired by the official julia language repo: https://github.com/JuliaLang/julia/blob/master/doc/make.jl

Move inside this folder (doc) and run julia --project=. make.jl to build documentation; a new private "build" folder will be created if no errors occur.

This is Documenter.jl documentation: https://documenter.juliadocs.org/stable/man/guide/

Troubleshooting

The command make can generate very large warning logs. Here it is a list of common mistakes.

Missing docstring

If the documentation is generated properly but some yellow frames "Missing docstring" appears, check if the definition is exported from your Package entry (e.g. SoleLogics.jl). If it is not exported, the following block

```@doc AbstractFormula ```

has to be rewritten like this, for example

```@doc SoleLogics.AbstractFormula ```

Note that if we want to specify a specific dispatch docstring, the same rule applies, for example

```@doc SoleLogics.propositions(f::SoleLogics.AbstractFormula) ```

instead of

```@doc SoleLogics.propositions(f::AbstractFormula) ```

+- · SoleLogics.jl

Quick start

make.jl structure is inspired by the official julia language repo: https://github.com/JuliaLang/julia/blob/master/doc/make.jl

Move inside this folder (doc) and run julia --project=. make.jl to build documentation; a new private "build" folder will be created if no errors occur.

This is Documenter.jl documentation: https://documenter.juliadocs.org/stable/man/guide/

Troubleshooting

The command make can generate very large warning logs. Here it is a list of common mistakes.

Missing docstring

If the documentation is generated properly but some yellow frames "Missing docstring" appears, check if the definition is exported from your Package entry (e.g. SoleLogics.jl). If it is not exported, the following block

```@doc AbstractFormula ```

has to be rewritten like this, for example

```@doc SoleLogics.AbstractFormula ```

Note that if we want to specify a specific dispatch docstring, the same rule applies, for example

```@doc SoleLogics.propositions(f::SoleLogics.AbstractFormula) ```

instead of

```@doc SoleLogics.propositions(f::AbstractFormula) ```

diff --git a/dev/base/alphabets/index.html b/dev/base/alphabets/index.html index 97f51282..5dc0d20d 100644 --- a/dev/base/alphabets/index.html +++ b/dev/base/alphabets/index.html @@ -16,6 +16,6 @@ └ @ SoleLogics ... true

Implementation

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

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

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

function propositions(a::AbstractAlphabet)::AbstractVector{propositionstype(a)}

By default, an alphabet is considered finite:

Base.isfinite(::Type{<:AbstractAlphabet}) = true
 Base.isfinite(a::AbstractAlphabet) = Base.isfinite(typeof(a))
-Base.in(p::Proposition, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, propositions(a)) : error(...)
source
Base.inFunction
Base.in(tok::AbstractSyntaxToken, f::AbstractFormula)::Bool

Return whether a syntax token appears in a formula.

See also AbstractSyntaxToken.

source
Base.in(tok::AbstractSyntaxToken, tree::SyntaxTree)::Bool

Return whether a token appears in a syntax tree or not.

See also tokens, SyntaxTree.

source
Base.in(t::SyntaxTree, g::AbstractGrammar)::Bool

Return whether a formula, encoded as a SyntaxTree, belongs to a grammar.

See also AbstractGrammar, SyntaxTree.

source
Missing docstring.

Missing docstring for Base.isiterable. Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.isfinite. Check Documenter's build log for details.

SoleLogics.ExplicitAlphabetType
struct ExplicitAlphabet{A} <: AbstractAlphabet{A}
+Base.in(p::Proposition, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, propositions(a)) : error(...)
source
Base.inFunction
Base.in(tok::AbstractSyntaxToken, f::AbstractFormula)::Bool

Return whether a syntax token appears in a formula.

See also AbstractSyntaxToken.

source
Base.in(tok::AbstractSyntaxToken, tree::SyntaxTree)::Bool

Return whether a token appears in a syntax tree or not.

See also tokens, SyntaxTree.

source
Base.in(t::SyntaxTree, g::AbstractGrammar)::Bool

Return whether a formula, encoded as a SyntaxTree, belongs to a grammar.

See also AbstractGrammar, SyntaxTree.

source
Missing docstring.

Missing docstring for Base.isiterable. Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.isfinite. Check Documenter's build log for details.

SoleLogics.ExplicitAlphabetType
struct ExplicitAlphabet{A} <: AbstractAlphabet{A}
     propositions::Vector{Proposition{A}}
-end

An alphabet wrapping propositions in a (finite) Vector.

See also propositions, AbstractAlphabet.

source
SoleLogics.AlphabetOfAnyType
struct AlphabetOfAny{A} <: AbstractAlphabet{A} end

An implicit, infinite alphabet that includes all propositions with atoms of a subtype of A.

See also AbstractAlphabet.

source
+end

An alphabet wrapping propositions in a (finite) Vector.

See also propositions, AbstractAlphabet.

source
SoleLogics.AlphabetOfAnyType
struct AlphabetOfAny{A} <: AbstractAlphabet{A} end

An implicit, infinite alphabet that includes all propositions with atoms of a subtype of A.

See also AbstractAlphabet.

source
diff --git a/dev/base/formulas/index.html b/dev/base/formulas/index.html index af23982c..15f4974c 100644 --- a/dev/base/formulas/index.html +++ b/dev/base/formulas/index.html @@ -5,7 +5,7 @@ children::NTuple{N,Union{AbstractSyntaxToken,MyCustomFormulaType}}, )::AbstractFormula where {N} # Composed formula -end

See also Formula, SyntaxTree, AbstractSyntaxStructure, AbstractLogic.

source
SoleLogics.joinformulasMethod
joinformulas(
+end

See also Formula, SyntaxTree, AbstractSyntaxStructure, AbstractLogic.

source
SoleLogics.joinformulasMethod
joinformulas(
     op::AbstractOperator,
     ::NTuple{N,F}
 )::F where {N,F<:AbstractFormula}

Return a new formula of type F by composing N formulas of the same type via an operator op. This function provides a way for composing formulas, but it allows to use operators for a more flexible composition; see the examples (and more in the extended help).

Examples

julia> f = parseformula("◊(p→q)");
@@ -38,14 +38,14 @@
     cs::Union{AbstractSyntaxToken,AbstractFormula}...
 )
     return ∨(c1, ∨(c2, c3, cs...))
-end

See also AbstractFormula, AbstractOperator.

source
Missing docstring.

Missing docstring for tokens(f::SoleLogics.AbstractFormula)::AbstractVector{<:SoleLogics.AbstractSyntaxToken}. Check Documenter's build log for details.

SoleLogics.operatorsMethod
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
+end

See also AbstractFormula, AbstractOperator.

source
Missing docstring.

Missing docstring for tokens(f::SoleLogics.AbstractFormula)::AbstractVector{<:SoleLogics.AbstractSyntaxToken}. Check Documenter's build log for details.

SoleLogics.operatorsMethod
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
 operators(f::AbstractFormula)::AbstractVector{<:AbstractOperator}
 propositions(f::AbstractFormula)::AbstractVector{<:Proposition}
 ntokens(f::AbstractFormula)::Integer
 noperators(f::AbstractFormula)::Integer
-npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
SoleLogics.propositionsMethod
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
+npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
SoleLogics.propositionsMethod
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
 operators(f::AbstractFormula)::AbstractVector{<:AbstractOperator}
 propositions(f::AbstractFormula)::AbstractVector{<:Proposition}
 ntokens(f::AbstractFormula)::Integer
 noperators(f::AbstractFormula)::Integer
-npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
Missing docstring.

Missing docstring for ntokens(f::SoleLogics.AbstractFormula). Check Documenter's build log for details.

Missing docstring.

Missing docstring for npropositions(f::SoleLogics.AbstractFormula). Check Documenter's build log for details.

Missing docstring.

Missing docstring for height. Check Documenter's build log for details.

+npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
Missing docstring.

Missing docstring for ntokens(f::SoleLogics.AbstractFormula). Check Documenter's build log for details.

Missing docstring.

Missing docstring for npropositions(f::SoleLogics.AbstractFormula). Check Documenter's build log for details.

Missing docstring.

Missing docstring for height. Check Documenter's build log for details.

diff --git a/dev/base/grammars/index.html b/dev/base/grammars/index.html index c08e6944..dd0f3e27 100644 --- a/dev/base/grammars/index.html +++ b/dev/base/grammars/index.html @@ -1,7 +1,7 @@ -Grammar · SoleLogics.jl

Grammar

Missing docstring.

Missing docstring for Base.in(tok::SoleLogics.AbstractSyntaxToken, g::SoleLogics.AbstractGrammar). Check Documenter's build log for details.

SoleLogics.propositionsFunction
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
+Grammar · SoleLogics.jl

Grammar

Missing docstring.

Missing docstring for Base.in(tok::SoleLogics.AbstractSyntaxToken, g::SoleLogics.AbstractGrammar). Check Documenter's build log for details.

SoleLogics.propositionsFunction
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
 operators(f::AbstractFormula)::AbstractVector{<:AbstractOperator}
 propositions(f::AbstractFormula)::AbstractVector{<:Proposition}
 ntokens(f::AbstractFormula)::Integer
 noperators(f::AbstractFormula)::Integer
-npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
propositions(t::SyntaxTree)::AbstractVector{Proposition}

List all propositions appearing in a syntax tree.

See also npropositions, operators, tokens, Proposition.

source
propositions(a::AbstractAlphabet)::AbstractVector{propositionstype(a)}

List the propositions of a finite alphabet.

See also AbstractAlphabet, Base.isfinite.

source
+npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
propositions(t::SyntaxTree)::AbstractVector{Proposition}

List all propositions appearing in a syntax tree.

See also npropositions, operators, tokens, Proposition.

source
propositions(a::AbstractAlphabet)::AbstractVector{propositionstype(a)}

List the propositions of a finite alphabet.

See also AbstractAlphabet, Base.isfinite.

source
diff --git a/dev/base/operators/index.html b/dev/base/operators/index.html index 07e08795..b9d5ca6c 100644 --- a/dev/base/operators/index.html +++ b/dev/base/operators/index.html @@ -1,12 +1,12 @@ -Operators · SoleLogics.jl

Operators

SoleLogics.AbstractOperatorType
abstract type AbstractOperator <: AbstractSyntaxToken end

An operator is a logical constant which establishes a relation between propositions (i.e., facts). For example, the boolean operators AND, OR and IMPLIES (stylized as ∧, ∨ and →) are used to connect propositions and/or formulas to express derived concepts.

Since operators display very different algorithmic behaviors, all structs that are subtypes of AbstractOperator must be parametric singleton types, which can be dispatched upon.

Implementation

When implementing a new type for a commutative operator O with arity higher than 1, please provide a method iscommutative(::Type{O}). This can help model checking operations.

See also AbstractSyntaxToken, NamedOperator, check.

source
SoleLogics.iscommutativeMethod
iscommutative(::Type{AbstractOperator})
+Operators · SoleLogics.jl

Operators

SoleLogics.AbstractOperatorType
abstract type AbstractOperator <: AbstractSyntaxToken end

An operator is a logical constant which establishes a relation between propositions (i.e., facts). For example, the boolean operators AND, OR and IMPLIES (stylized as ∧, ∨ and →) are used to connect propositions and/or formulas to express derived concepts.

Since operators display very different algorithmic behaviors, all structs that are subtypes of AbstractOperator must be parametric singleton types, which can be dispatched upon.

Implementation

When implementing a new type for a commutative operator O with arity higher than 1, please provide a method iscommutative(::Type{O}). This can help model checking operations.

See also AbstractSyntaxToken, NamedOperator, check.

source
SoleLogics.iscommutativeMethod
iscommutative(::Type{AbstractOperator})
 iscommutative(o::AbstractOperator) = iscommutative(typeof(o))

Return whether it is known that an AbstractOperator is commutative.

Examples

julia> iscommutative(∧)
 true
 
 julia> iscommutative(→)
-false

Note that nullary and unary operators are considered commutative.

See also AbstractOperator.

Implementation

When implementing a new type for a commutative operator O with arity higher than 1, please provide a method iscommutative(::Type{O}). This can help model checking operations.

source
SoleLogics.operatorsFunction
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
+false

Note that nullary and unary operators are considered commutative.

See also AbstractOperator.

Implementation

When implementing a new type for a commutative operator O with arity higher than 1, please provide a method iscommutative(::Type{O}). This can help model checking operations.

source
SoleLogics.operatorsFunction
tokens(f::AbstractFormula)::AbstractVector{<:AbstractSyntaxToken}
 operators(f::AbstractFormula)::AbstractVector{<:AbstractOperator}
 propositions(f::AbstractFormula)::AbstractVector{<:Proposition}
 ntokens(f::AbstractFormula)::Integer
 noperators(f::AbstractFormula)::Integer
-npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
operators(t::SyntaxTree)::AbstractVector{AbstractOperator}

List all operators appearing in a syntax tree.

See also noperators, propositions, tokens, AbstractOperator.

source
Missing docstring.

Missing docstring for noperators. Check Documenter's build log for details.

+npropositions(f::AbstractFormula)::Integer

Return the list or the number of (unique) syntax tokens/operators/propositions appearing in a formula.

See also AbstractSyntaxStructure.

source
operators(t::SyntaxTree)::AbstractVector{AbstractOperator}

List all operators appearing in a syntax tree.

See also noperators, propositions, tokens, AbstractOperator.

source
Missing docstring.

Missing docstring for noperators. Check Documenter's build log for details.

diff --git a/dev/base/syntax/index.html b/dev/base/syntax/index.html index 887b2d19..39011fac 100644 --- a/dev/base/syntax/index.html +++ b/dev/base/syntax/index.html @@ -1,15 +1,15 @@ -Syntax · SoleLogics.jl

Syntax

SoleLogics.arityMethod
arity(::Type{<:AbstractSyntaxToken})::Integer
-arity(tok::AbstractSyntaxToken)::Integer = arity(typeof(tok))

Return the arity of a syntax token. The arity of a syntax token is an integer representing the number of allowed children in a SyntaxTree. Tokens with arity equal to 0, 1 or 2 are called nullary, unary and binary, respectively.

See also AbstractSyntaxToken.

source
SoleLogics.syntaxstringMethod
syntaxstring(φ::AbstractFormula; kwargs...)::String
+Syntax · SoleLogics.jl

Syntax

SoleLogics.arityMethod
arity(::Type{<:AbstractSyntaxToken})::Integer
+arity(tok::AbstractSyntaxToken)::Integer = arity(typeof(tok))

Return the arity of a syntax token. The arity of a syntax token is an integer representing the number of allowed children in a SyntaxTree. Tokens with arity equal to 0, 1 or 2 are called nullary, unary and binary, respectively.

See also AbstractSyntaxToken.

source
SoleLogics.syntaxstringMethod
syntaxstring(φ::AbstractFormula; kwargs...)::String
 syntaxstring(tok::AbstractSyntaxToken; kwargs...)::String

Produces the string representation of a formula or syntax token by performing a tree traversal of the syntax tree representation of the formula. 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.

Examples

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

See also parsebaseformula, parsetree, SyntaxTree, AbstractSyntaxToken.

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 kwargs...) for every newly defined AbstractSyntaxToken (e.g., operators and Propositions), 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 Propositions, the function calls itself on the atom:

syntaxstring(p::Proposition; kwargs...) = syntaxstring(atom(p); kwargs...)

Then, the syntaxstring for a given atom can be defined. For example, with String atoms, the function can simply be:

syntaxstring(atom::String; kwargs...) = atom
Warning

The syntaxstring for syntax tokens (e.g., propositions, 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 parsebaseformula.

source
SoleLogics.PropositionType
struct Proposition{A} <: AbstractSyntaxToken
+"◊(→(∧(p, s), q))"

See also parsebaseformula, parsetree, SyntaxTree, AbstractSyntaxToken.

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 kwargs...) for every newly defined AbstractSyntaxToken (e.g., operators and Propositions), 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 Propositions, the function calls itself on the atom:

syntaxstring(p::Proposition; kwargs...) = syntaxstring(atom(p); kwargs...)

Then, the syntaxstring for a given atom can be defined. For example, with String atoms, the function can simply be:

syntaxstring(atom::String; kwargs...) = atom
Warning

The syntaxstring for syntax tokens (e.g., propositions, 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 parsebaseformula.

source
SoleLogics.PropositionType
struct Proposition{A} <: AbstractSyntaxToken
     atom::A
-end

A proposition, sometimes called a propositional letter (or simply letter), of type Proposition{A} wraps a value atom::A representing a fact which truth can be assessed on a logical interpretation.

Propositions are nullary tokens (i.e, they are at the leaves of a syntax tree). Note that their atom cannot be a Proposition.

See also AbstractSyntaxToken, AbstractInterpretation, check.

source
Missing docstring.

Missing docstring for negation(p::Proposition). Check Documenter's build log for details.

SoleLogics.SyntaxTreeType
struct SyntaxTree{
+end

A proposition, sometimes called a propositional letter (or simply letter), of type Proposition{A} wraps a value atom::A representing a fact which truth can be assessed on a logical interpretation.

Propositions are nullary tokens (i.e, they are at the leaves of a syntax tree). Note that their atom cannot be a Proposition.

See also AbstractSyntaxToken, AbstractInterpretation, check.

source
Missing docstring.

Missing docstring for negation(p::Proposition). Check Documenter's build log for details.

SoleLogics.SyntaxTreeType
struct SyntaxTree{
     T<:AbstractSyntaxToken,
 } <: AbstractSyntaxStructure
     token::T
     children::NTuple{N,SyntaxTree} where {N}
-end

A syntax tree encoding a logical formula. Each node of the syntax tree holds a token::T, and has as many children as the arity of the token.

This implementation is arity-compliant, in that, upon construction, the arity is checked against the number of children provided.

See also token, children, tokentype, tokens, operators, propositions, ntokens, npropositions, height, tokenstype, operatorstype, propositionstype, AbstractSyntaxToken, arity, Proposition, Operator.

source
Base.inMethod
Base.in(tok::AbstractSyntaxToken, f::AbstractFormula)::Bool

Return whether a syntax token appears in a formula.

See also AbstractSyntaxToken.

source
Missing docstring.

Missing docstring for ntokens. Check Documenter's build log for details.

+end

A syntax tree encoding a logical formula. Each node of the syntax tree holds a token::T, and has as many children as the arity of the token.

This implementation is arity-compliant, in that, upon construction, the arity is checked against the number of children provided.

See also token, children, tokentype, tokens, operators, propositions, ntokens, npropositions, height, tokenstype, operatorstype, propositionstype, AbstractSyntaxToken, arity, Proposition, Operator.

source
Base.inMethod
Base.in(tok::AbstractSyntaxToken, f::AbstractFormula)::Bool

Return whether a syntax token appears in a formula.

See also AbstractSyntaxToken.

source
Missing docstring.

Missing docstring for ntokens. Check Documenter's build log for details.

diff --git a/dev/index.html b/dev/index.html index 306131da..3e5858c5 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,2 +1,2 @@ -Home · SoleLogics.jl

SoleLogics

Welcome to the documentation for SoleLogics.

SoleLogics.jl provides a fresh codebase for computational logic, featuring easy manipulation of:

  • Propositional and (multi)modal logics (propositions, logical constants, alphabet, grammars, crisp/fuzzy algebras);
  • Logical formulas (random generation, parsing, minimization);
  • Logical interpretations (e.g., propositional valuations, Kripke structures);
  • Algorithms for model checking, that is, checking that a formula is satisfied by an interpretation.

SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning.

Modules = [SoleModels]
+Home · SoleLogics.jl

SoleLogics

Welcome to the documentation for SoleLogics.

SoleLogics.jl provides a fresh codebase for computational logic, featuring easy manipulation of:

  • Propositional and (multi)modal logics (propositions, logical constants, alphabet, grammars, crisp/fuzzy algebras);
  • Logical formulas (random generation, parsing, minimization);
  • Logical interpretations (e.g., propositional valuations, Kripke structures);
  • Algorithms for model checking, that is, checking that a formula is satisfied by an interpretation.

SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning.

Modules = [SoleModels]
diff --git a/dev/search/index.html b/dev/search/index.html index e17dd226..3b572ac1 100644 --- a/dev/search/index.html +++ b/dev/search/index.html @@ -1,2 +1,2 @@ -Search · SoleLogics.jl

Loading search...

    +Search · SoleLogics.jl

    Loading search...