diff --git a/dev/autodocs/index.html b/dev/autodocs/index.html index 1e6950ce..3ed8cc68 100644 --- a/dev/autodocs/index.html +++ b/dev/autodocs/index.html @@ -1,25 +1,25 @@ Full reference · SoleLogics.jl
Edit on GitHub

Full reference for SoleLogics.jl

Auto documentation for SoleLogics.jl.

SoleLogics.:¬ — 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.BASE_PARSABLE_OPERATORS — Constant
const BASE_PARSABLE_OPERATORS = SoleLogics.Syntactical[¬, ∧, ∨, →, ◊, □, ⟨G⟩, [G], ⟨=⟩, [=], ⊤, ⊥]

Vector of (standard) operators that are automatically taken care of when parsing.

See also parseformula.

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

Vector of (standard) operators that are automatically taken care of when parsing.

See also parseformula.

source
SoleLogics.BOT — Constant
struct Bot <: Truth end
 const BOT = Bot()
-const ⊥ = BOT

Canonical truth operator representing the value false. It can be typed by \bot<tab>.

See also TOP, Truth.

source
SoleLogics.BOX — Constant
const BOX = NamedConnective{:□}()
+const ⊥ = BOT

Canonical truth operator representing the value false. It can be typed by \bot<tab>.

See also TOP, Truth.

source
SoleLogics.DIAMOND — Constant
const DIAMOND = NamedConnective{:◊}()
 const ◊ = DIAMOND
 ismodal(::NamedConnective{:◊}) = true
-arity(::typeof(◊)) = 1

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

See also BOX, NamedConnective, Connective.

source
SoleLogics.IABase — Type
const IABase = Union{IntervalRelation,IdentityRel,GlobalRel}
 struct RectangleRelation{R1<:IABase,R2<:IABase} <: GeometricalRelation
     x :: R1
     y :: R2
@@ -33,37 +33,37 @@
  "A̅,E̅"
  "B̅,E"
  "E̅,D̅"
- "O̅,D"

See also Interval, Interval2D, IntervalRelation, [[GeometricalRelation`](@ref).

source
SoleLogics.Operator — Method
(op::Operator)(o::Any)

An Operator can be used to compose syntax tokens (e.g., atoms), syntax trees and/or formulas.

Examples

    ¬(Atom(1)) ∨ Atom(1) ∧ ⊤
+arity(::typeof(¬)) = 1

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

See also NamedConnective, Connective.

source
SoleLogics.Operator — Method
(op::Operator)(o::Any)

An Operator can be used to compose syntax tokens (e.g., atoms), syntax trees and/or formulas.

Examples

    ¬(Atom(1)) ∨ Atom(1) ∧ ⊤
     ∧(⊤,⊤)
-    ⊤()
source
SoleLogics.TOP — Constant
struct Top <: Truth end
 const TOP = Top()
-const ⊤ = TOP

Canonical truth operator representing the value true. It can be typed by \top<tab>.

See also BOT, Truth.

source
SoleLogics.globalrel — Constant
struct GlobalRel <: AbstractRelation end;
+const ⊤ = TOP

Canonical truth operator representing the value true. It can be typed by \top<tab>.

See also BOT, Truth.

source
SoleLogics.⊤ — Constant
struct Top <: Truth end
 const TOP = Top()
-const ⊤ = TOP

Canonical truth operator representing the value true. It can be typed by \top<tab>.

See also BOT, Truth.

source
SoleLogics.⊥ — Constant
struct Bot <: Truth end
+const ⊤ = TOP

Canonical truth operator representing the value true. It can be typed by \top<tab>.

See also BOT, Truth.

source
SoleLogics.⊥ — Constant
struct Bot <: Truth end
 const BOT = Bot()
-const ⊥ = BOT

Canonical truth operator representing the value false. It can be typed by \bot<tab>.

See also TOP, Truth.

source
SoleLogics.□ — Constant
const BOX = NamedConnective{:□}()
+const ⊥ = BOT

Canonical truth operator representing the value false. It can be typed by \bot<tab>.

See also TOP, Truth.

source
SoleLogics.◊ — Constant
const DIAMOND = NamedConnective{:◊}()
 const ◊ = DIAMOND
 ismodal(::NamedConnective{:◊}) = true
-arity(::typeof(◊)) = 1

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

See also BOX, NamedConnective, Connective.

source
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.

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.AbstractAlphabet — Type
abstract type AbstractAlphabet{V} end

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

Examples

julia> Atom(1) in ExplicitAlphabet(Atom.(1:10))
+arity(::typeof(◊)) = 1

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

See also BOX, NamedConnective, Connective.

source
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.

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.AbstractAlphabet — Type
abstract type AbstractAlphabet{V} end

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

Examples

julia> Atom(1) in ExplicitAlphabet(Atom.(1:10))
 true
 
 julia> Atom(1) in ExplicitAlphabet(1:10)
@@ -80,17 +80,17 @@
 └ @ SoleLogics ...
 true

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::Atom, 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::Atom, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, atoms(a)) : error(...)

See also AbstractGrammar, AlphabetOfAny, Atom, ExplicitAlphabet, atomstype, valuetype.

source
SoleLogics.AbstractInterpretationSet — Type
abstract type AbstractInterpretationSet{M<:AbstractInterpretation} <: AbstractDataset end

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

See also valuetype, truthtype, InterpretationSet.

source
SoleLogics.AbstractLogic — Type
abstract type AbstractLogic{G<:AbstractGrammar,V<:AbstractAlgebra} end

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

Implementation

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

See also AbstractAlgebra, AbstractGrammar.

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.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,),);
+} <: AbstractMultiModalFrame{W} end

Abstract type for dimensional frames. Given a N-dimensional array of size (X, Y, Z, ...) the corresponding dimensional frame is a graph where each vertex is an N-hyperrectangle (e.g., an Interval/Interval2D) in the space (1:X, 1:Y, 1:Z, ...).

See also Interval, Interval2D, IntervalRelation, AbstractDimensionalFrame, AbstractMultiModalFrame.

source
SoleLogics.AbstractInterpretationSet — Type
abstract type AbstractInterpretationSet{M<:AbstractInterpretation} <: AbstractDataset end

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

See also valuetype, truthtype, InterpretationSet.

source
SoleLogics.AbstractLogic — Type
abstract type AbstractLogic{G<:AbstractGrammar,V<:AbstractAlgebra} end

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

Implementation

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

See also AbstractAlgebra, AbstractGrammar.

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.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.AbstractSyntaxStructure — Type
abstract type AbstractSyntaxStructure <: Formula end

Abstract type for the purely-syntactic component of a logical formula (e.g., no fancy memoization structure associated). The typical representation is the SyntaxTree, however, different implementations can cover specific syntactic forms (e.g., conjuctive/disjuctive normal forms).

See also Formula, AbstractLogic, SyntaxTree, tree.

source
SoleLogics.AbstractWorld — Type
abstract type AbstractWorld end

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

Implementing

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

See also AbstractKripkeStructure, AbstractFrame.

source
SoleLogics.AbstractSyntaxStructure — Type
abstract type AbstractSyntaxStructure <: Formula end

Abstract type for the purely-syntactic component of a logical formula (e.g., no fancy memoization structure associated). The typical representation is the SyntaxTree, however, different implementations can cover specific syntactic forms (e.g., conjuctive/disjuctive normal forms).

See also Formula, AbstractLogic, SyntaxTree, tree.

source
SoleLogics.AbstractWorld — Type
abstract type AbstractWorld end

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

Implementing

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

See also AbstractKripkeStructure, AbstractFrame.

source
SoleLogics.AnchoredFormula — Type
struct AnchoredFormula{L<:AbstractLogic} <: Formula
     _logic::Base.RefValue{L}
     synstruct::AbstractSyntaxStructure
 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> f = parsebaseformula("◊(p→q)");
@@ -108,14 +108,14 @@
 julia> @assert ◊ in operators(logic(f2))
 
 julia> @assert ◊ isa operatorstype(logic(f2))
-

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

source
SoleLogics.Atom — Type
struct Atom{V} <: SyntaxLeaf
     value::V
-end

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

Atoms are nullary tokens (i.e, they are at the leaves of a syntax tree); note that their atoms cannot be Atoms.

See also AbstractInterpretation, check, SyntaxToken.

source
SoleLogics.BaseLogic — Type
struct BaseLogic{G<:AbstractGrammar,A<:AbstractAlgebra} <: AbstractLogic{G,A}
+end

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

Atoms are nullary tokens (i.e, they are at the leaves of a syntax tree); note that their atoms cannot be Atoms.

See also AbstractInterpretation, check, SyntaxToken.

source
SoleLogics.BooleanAlgebra — Type
struct BooleanAlgebra <: AbstractAlgebra{Bool} end

A boolean algebra, defined on the values Top (representing true) and Bot (for bottom, representing false). 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.BooleanAlgebra — Type
struct BooleanAlgebra <: AbstractAlgebra{Bool} end

A boolean algebra, defined on the values Top (representing true) and Bot (for bottom, representing false). 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.Bot — Type
struct Bot <: Truth end
 const BOT = Bot()
-const ⊥ = BOT

Canonical truth operator representing the value false. It can be typed by \bot<tab>.

See also TOP, Truth.

source
SoleLogics.CNF — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
+const ⊥ = BOT

Canonical truth operator representing the value false. It can be typed by \bot<tab>.

See also TOP, Truth.

source
SoleLogics.CNF — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
     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<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
 const LeftmostDisjunctiveForm{SS<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}
@@ -135,10 +135,10 @@
 
 julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa SoleLogics.DNF
 true
-
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.Connective — Type
abstract type Connective <: Syntactical end

Abstract type for logical connectives, that are used to express non-atomic statements; for example, CONJUNCTION, DISJUNCTION and IMPLICATION (stylized as ∧, ∨ and →).

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 https://docs.julialang.org/en/v1/manual/mathematical-operations/#Operator-Precedence-and-Associativity). 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.

See also arity, SyntaxBranch, associativity, precedence, check, iscommutative, NamedConnective, Syntactical.

source
SoleLogics.DNF — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
+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.Connective — Type
abstract type Connective <: Syntactical end

Abstract type for logical connectives, that are used to express non-atomic statements; for example, CONJUNCTION, DISJUNCTION and IMPLICATION (stylized as ∧, ∨ and →).

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 https://docs.julialang.org/en/v1/manual/mathematical-operations/#Operator-Precedence-and-Associativity). 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.

See also arity, SyntaxBranch, associativity, precedence, check, iscommutative, NamedConnective, Syntactical.

source
SoleLogics.DNF — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
     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<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
 const LeftmostDisjunctiveForm{SS<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}
@@ -158,7 +158,7 @@
 
 julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa SoleLogics.DNF
 true
-
source
SoleLogics.DiamondRelationalOperator — Type
struct DiamondRelationalOperator{R<:AbstractRelation} <: AbstractRelationalOperator{R} end
 struct BoxRelationalOperator{R<:AbstractRelation} <: AbstractRelationalOperator{R} end

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

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

Examples

julia> syntaxstring(DiamondRelationalOperator(IA_A))
 "⟨A⟩"
 
@@ -186,9 +186,9 @@
 "[A]"
 
 julia> @assert DiamondRelationalOperator(IA_A) == SoleLogics.dual(BoxRelationalOperator(IA_A))
-

See also DiamondRelationalOperator, BoxRelationalOperator, syntaxstring, dual, AbstractKripkeStructure, AbstractFrame.

source
SoleLogics.Formula — Type
abstract type Formula <: Syntactical end

Abstract type for logical formulas. Examples of Formulas are SyntaxLeafs (for example, Atoms and Truth values), AbstractSyntaxStructures (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.

See also tree, AbstractSyntaxStructure, SyntaxLeaf.

source
SoleLogics.Formula — Type
abstract type Formula <: Syntactical end

Abstract type for logical formulas. Examples of Formulas are SyntaxLeafs (for example, Atoms and Truth values), AbstractSyntaxStructures (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.

See also tree, AbstractSyntaxStructure, SyntaxLeaf.

source
SoleLogics.FullDimensionalFrame — Type
struct FullDimensionalFrame{N,W<:AbstractWorld} <: AbstractDimensionalFrame{N,W}
     channelsize::NTuple{N,Int}
 end

Abstract type for full dimensional frames. Given a N-dimensional array of size (X, Y, Z, ...) the corresponding full dimensional frame is a graph where there is exactly one vertex for each M-hyperrectangle in the space (1:X, 1:Y, 1:Z, ...), with M ≤ N.

Here, the M-hyperrectangle can be either a Point, or a N-tuple of intervals (e.g., Interval or Interval2D), where each interval is a pair of natural numbers (x,y) where: i) x > 0; ii) y > 0; iii) x < y.

The current implementation can handle N ∈ {0,1,2}.

Examples

julia> SoleLogics.allworlds(SoleLogics.FullDimensionalFrame((),))
 1-element Vector{OneWorld}:
@@ -205,19 +205,19 @@
  ((4−5)×(5−6))
  ((4−6)×(5−6))
  ((5−6)×(5−6))
-

See also OneWorld, Interval, Interval2D, IntervalRelation, IntervalRelation2D, accessibles, AbstractDimensionalFrame, AbstractMultiModalFrame.

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

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

Examples

julia> SoleLogics.goeswithdim(SoleLogics.Interval2D((1,2),(3,4)),1)
@@ -249,7 +249,7 @@
  ((4−5)×(5−6))
  ((4−6)×(5−6))
  ((5−6)×(5−6))
-

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

source
SoleLogics.IntervalRelation — Type
abstract type IntervalRelation <: GeometricalRelation end

Abstract type for interval binary relations. Originally defined by Allen in 1983, interval algebra comprehends 12 directional relations between intervals, plus the identity (i.e., identityrel).

The 12 relations are the 6 relations after, later, begins, ends, during, overlaps, and their inverses.

If we consider a reference interval (x,y), we can graphically represent the 6 base relations by providing an example of a world (z,t) that is accessible via each of them:

RELATION ABBR. x y PROPERTY |–––––––––-| . . . z t y = z After (A) . |––––| . . . . z t y < z Later (L) . . |––––-| . . z t . x = z, t < y Begins (B) |––-| . . . . z t y = t, x < z Ends (E) . |––-| . . . z t . x < z, t < y During (D) . |––––| . . . . z . t x < z < y < t Overlaps (O) . |––––––|

Coarser relations can be defined by union of these 12 relations.

Examples

julia> IARelations
+

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

source
SoleLogics.IntervalRelation — Type
abstract type IntervalRelation <: GeometricalRelation end

Abstract type for interval binary relations. Originally defined by Allen in 1983, interval algebra comprehends 12 directional relations between intervals, plus the identity (i.e., identityrel).

The 12 relations are the 6 relations after, later, begins, ends, during, overlaps, and their inverses.

If we consider a reference interval (x,y), we can graphically represent the 6 base relations by providing an example of a world (z,t) that is accessible via each of them:

RELATION ABBR. x y PROPERTY |–––––––––-| . . . z t y = z After (A) . |––––| . . . . z t y < z Later (L) . . |––––-| . . z t . x = z, t < y Begins (B) |––-| . . . . z t y = t, x < z Ends (E) . |––-| . . . z t . x < z, t < y During (D) . |––––| . . . . z . t x < z < y < t Overlaps (O) . |––––––|

Coarser relations can be defined by union of these 12 relations.

Examples

julia> IARelations
 12-element Vector{IntervalRelation}:
  _IA_A()
  _IA_L()
@@ -315,13 +315,13 @@
  "I"
  "L"
  "L̅"
-

See also IARelations, IA7Relations, IA3Relations, Interval, GeometricalRelation.

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

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

source
SoleLogics.LeftmostConjunctiveForm — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
+end

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

source
SoleLogics.LeftmostConjunctiveForm — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
     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<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
 const LeftmostDisjunctiveForm{SS<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}
@@ -341,7 +341,7 @@
 
 julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa SoleLogics.DNF
 true
-
source
SoleLogics.LeftmostDisjunctiveForm — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
     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<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
 const LeftmostDisjunctiveForm{SS<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}
@@ -361,7 +361,7 @@
 
 julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa SoleLogics.DNF
 true
-
source
SoleLogics.LeftmostLinearForm — Type
struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: AbstractSyntaxStructure
     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<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
 const LeftmostDisjunctiveForm{SS<:AbstractSyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}
@@ -381,21 +381,21 @@
 
 julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa SoleLogics.DNF
 true
-

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

source
SoleLogics.LogicalInstance — Type

TODO explain. In general, one may not be able to extract a single logical instance from a set, thus we represent it as a tuple of dataset + instance id (i_instance).

source
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 (logical conjuction) is defined as the subtype:

const CONJUNCTION = NamedConnective{:∧}()
+end

An atom, or its negation.

See also CNF, DNF, AbstractSyntaxStructure.

source
SoleLogics.LogicalInstance — Type

TODO explain. In general, one may not be able to extract a single logical instance from a set, thus we represent it as a tuple of dataset + instance id (i_instance).

source
SoleLogics.RCCRelation — Type
abstract type RCCRelation <: GeometricalRelation end

Topological binary relations from Region Connection Calculus. Region Connection Calculus (RCC) is most famous for RCC8, a set of 8 topological relations, which comprehends the identity relation (i.e., `identityrel'), and the following 7 relations:

  • Externally connected
  • Partially overlapping
  • Tangential proper part
  • Tangential proper part inverse
  • Non-tangential proper part
  • Non-tangential proper part inverse

If we consider a reference interval (x,y), we can graphically represent the 7 relations by providing an example of a world (z,t) that is accessible via each of them:

                                             x                   y

RELATION ABBR. |–––––––––-| . . . . z t Disconnected (DC) . . |––––| . . . z t Externally connected (EC) . |––––-| . . . z t Partially overlapping (PO) . |––-| . . . z t Tangential proper part (TPP) . |––-| . . z . t Tangential proper part inverse (T̅P̅P̅) |––––––––––––-| . . . z . Non-tangential proper part (NTPP) . |––-| . . . z . . t Non-tangential proper part inverse (N̅T̅P̅P̅) |–––––––––––-|

Methods for RCC8 relations and Interval2D's can be obtained by combining their 1D versions, according to the following composition rules:

             .-------------------------------------------------------.
+

See also goeswithdim, Interval, Interval2D, GeometricalWorld, AbstractWorld.

source
SoleLogics.RCCRelation — Type
abstract type RCCRelation <: GeometricalRelation end

Topological binary relations from Region Connection Calculus. Region Connection Calculus (RCC) is most famous for RCC8, a set of 8 topological relations, which comprehends the identity relation (i.e., `identityrel'), and the following 7 relations:

  • Externally connected
  • Partially overlapping
  • Tangential proper part
  • Tangential proper part inverse
  • Non-tangential proper part
  • Non-tangential proper part inverse

If we consider a reference interval (x,y), we can graphically represent the 7 relations by providing an example of a world (z,t) that is accessible via each of them:

                                             x                   y

RELATION ABBR. |–––––––––-| . . . . z t Disconnected (DC) . . |––––| . . . z t Externally connected (EC) . |––––-| . . . z t Partially overlapping (PO) . |––-| . . . z t Tangential proper part (TPP) . |––-| . . z . t Tangential proper part inverse (T̅P̅P̅) |––––––––––––-| . . . z . Non-tangential proper part (NTPP) . |––-| . . . z . . t Non-tangential proper part inverse (N̅T̅P̅P̅) |–––––––––––-|

Methods for RCC8 relations and Interval2D's can be obtained by combining their 1D versions, according to the following composition rules:

             .-------------------------------------------------------.
              |         DC   EC   PO   TPP   T̅P̅P̅   NTPP   N̅T̅P̅P̅    Id  |
              |-------------------------------------------------------|
              | DC   |  DC | DC | DC | DC  | DC  |  DC  |  DC  |  DC  |
@@ -444,7 +444,7 @@
  _Topo_DR()
  _Topo_PO()
  _Topo_PP()
- _Topo_PPi()

See also RCC8Relations, RCC5Relations, Interval, IntervalRelation, GeometricalRelation.

source
SoleLogics.SyntaxBranch — Type
struct SyntaxBranch{T<:Connective} <: SyntaxTree
     token::T
     children::NTuple{N,SyntaxTree} where {N}
-end

An internal node of a syntax tree encoding a logical formula. Such a node holds a syntax token (a Connective, and has as many children as the arity of the token.

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

See also token, children, arity, Connective, height, atoms, natoms, atomstype, operators, noperators, operatorstype, tokens, ntokens, tokenstype,

source
SoleLogics.ToCenteredRel — Type
struct ToCenteredRel <: AbstractRelation end;
+end

An internal node of a syntax tree encoding a logical formula. Such a node holds a syntax token (a Connective, and has as many children as the arity of the token.

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

See also token, children, arity, Connective, height, atoms, natoms, atomstype, operators, noperators, operatorstype, tokens, ntokens, tokenstype,

source
SoleLogics.Top — Type
struct Top <: Truth end
 const TOP = Top()
-const ⊤ = TOP

Canonical truth operator representing the value true. It can be typed by \top<tab>.

See also BOT, Truth.

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 tused.

Implementation

When implementing a custom Truth subtype, provide istop, isbot... TODO: write the interface to be implemented here, with an example.

See also Top, Bot, BooleanTruth, arity;

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

Canonical truth operator representing the value true. It can be typed by \top<tab>.

See also BOT, Truth.

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 tused.

Implementation

When implementing a custom Truth subtype, provide istop, isbot... TODO: write the interface to be implemented here, with an example.

See also Top, Bot, BooleanTruth, arity;

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:
@@ -497,21 +497,21 @@
 
 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 DefaultedTruthDict, AbstractAssignment, AbstractInterpretation.

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.Worlds — Type
const AbstractWorlds{W} = AbstractVector{W} where {W<:AbstractWorld}
-const Worlds{W} = Vector{W} where {W<:AbstractWorld}

Useful aliases for dealing with worlds sets/arrays.

See also accessibles, AbstractWorld.

source
SoleLogics.Worlds — Type
const AbstractWorlds{W} = AbstractVector{W} where {W<:AbstractWorld}
+const Worlds{W} = Vector{W} where {W<:AbstractWorld}

Useful aliases for dealing with worlds sets/arrays.

See also accessibles, AbstractWorld.

source
SoleLogics.WrapperMultiModalFrame — Type
struct WrapperMultiModalFrame{
     W<:AbstractWorld,
     D<:AbstractDict{<:AbstractRelation,<:AbstractUniModalFrame{W}}
 } <: AbstractMultiModalFrame{W}
     frames::D
-end

A multi-modal frame that is the superposition of many uni-modal frames. It uses a single AbstractUniModalFrame for each of relations.

See also AbstractRelation, AbstractUniModalFrame.

source
Base.rand — Method
Base.rand(
     [rng::AbstractRNG = Random.GLOBAL_RNG, ]
     alphabet,
     args...;
     kwargs...
-)::Atom

Randomly sample an atom from an alphabet, according to a uniform distribution.

Implementation

If the alphabet is finite, the function defaults to rand(rng, atoms(alphabet)); otherwise, it must be implemented, and additional keyword arguments should be provided in order to limit the (otherwise infinite) sampling domain.

See also isfinite, `AbstractAlphabet'.

source
SoleLogics.accessibles — Method
accessibles(
+)::Atom

Randomly sample an atom from an alphabet, according to a uniform distribution.

Implementation

If the alphabet is finite, the function defaults to rand(rng, atoms(alphabet)); otherwise, it must be implemented, and additional keyword arguments should be provided in order to limit the (otherwise infinite) sampling domain.

See also isfinite, `AbstractAlphabet'.

source
SoleLogics.arity — Method
arity(tok::Connective)::Integer
-arity(φ::SyntaxLeaf)::Integer # TODO extend to SyntaxTree SyntaxBranch

Return the arity of a Connective or an SyntaxLeaf. The arity is an integer representing the number of allowed children in a SyntaxBranch. 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
SoleLogics.arity — Method
arity(tok::Connective)::Integer
-arity(φ::SyntaxLeaf)::Integer # TODO extend to SyntaxTree SyntaxBranch

Return the arity of a Connective or an SyntaxLeaf. The arity is an integer representing the number of allowed children in a SyntaxBranch. 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
SoleLogics.associativity — Method
associativity(::Connective)

Return whether a (binary) connective is right-associative.

When using infix notation, and in the absence of parentheses, associativity establishes how binary connectives of the sameprecedenceare interpreted. This affects how formulas are shown (viasyntaxstring) and parsed (viaparseformula`).

By default, the value for a NamedConnective is derived from the Base.operator_precedence of its symbol (name); thus, for example, most connectives are left-associative (e.g., ∧ and ∨), while → is right-associative. Because of this, when dealing with a custom connective ⊙, it will be the case that parseformula("p ⊙ q ∧ r") == (@synexpr p ⊙ q ∧ r).

Examples

julia> associativity(∧)
+end

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

See also AbstractWorld, AbstractRelation, AbstractMultiModalFrame.

source
SoleLogics.arity — Method
arity(tok::Connective)::Integer
+arity(φ::SyntaxLeaf)::Integer # TODO extend to SyntaxTree SyntaxBranch

Return the arity of a Connective or an SyntaxLeaf. The arity is an integer representing the number of allowed children in a SyntaxBranch. 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
SoleLogics.arity — Method
arity(tok::Connective)::Integer
+arity(φ::SyntaxLeaf)::Integer # TODO extend to SyntaxTree SyntaxBranch

Return the arity of a Connective or an SyntaxLeaf. The arity is an integer representing the number of allowed children in a SyntaxBranch. 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
SoleLogics.associativity — Method
associativity(::Connective)

Return whether a (binary) connective is right-associative.

When using infix notation, and in the absence of parentheses, associativity establishes how binary connectives of the sameprecedenceare interpreted. This affects how formulas are shown (viasyntaxstring) and parsed (viaparseformula`).

By default, the value for a NamedConnective is derived from the Base.operator_precedence of its symbol (name); thus, for example, most connectives are left-associative (e.g., ∧ and ∨), while → is right-associative. Because of this, when dealing with a custom connective ⊙, it will be the case that parseformula("p ⊙ q ∧ r") == (@synexpr p ⊙ q ∧ r).

Examples

julia> associativity(∧)
 :left
 
 julia> associativity(→)
@@ -572,7 +572,7 @@
 "p → (q → r)"
 
 julia> syntaxstring(parseformula("p ∧ q ∨ r"); remove_redundant_parentheses = false)
-"(p ∧ q) ∨ r"

See also Connective, parseformula, precedence, syntaxstring.

source
SoleLogics.atoms — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -583,7 +583,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.baseformula — Method
function baseformula(
     φ::Formula;
     infer_logic = true,
     additional_operators::Union{Nothing,Vector{<:Operator}} = nothing,
@@ -603,7 +603,7 @@
  ∨
  →
  ◊
- □
source
SoleLogics.check — Function
function check(
     φ::SyntaxTree,
     i::AbstractKripkeStructure,
     w::Union{Nothing,<:AbstractWorld} = nothing;
@@ -646,7 +646,7 @@
  SoleLogics.World{Int64}(2) => 1
  SoleLogics.World{Int64}(3) => 1
  SoleLogics.World{Int64}(4) => 0
- SoleLogics.World{Int64}(5) => 0

See also SyntaxTree, AbstractWorld, KripkeStructure.

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
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)");
+)::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
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");
 
@@ -712,7 +712,7 @@
     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
SoleLogics.connectives — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -723,16 +723,16 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.dual — Method
dual(op::SyntaxToken)

Return the dual of an Operator. Given an operator op of arity n, the dual dop is such that, on a boolean algebra, op(ch_1, ..., ch_n) ≡ ¬dop(¬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). Duality also applies to Truth values (⊤/⊥), with existential/universal semantics (◊/□), and 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.dual — Method
dual(op::SyntaxToken)

Return the dual of an Operator. Given an operator op of arity n, the dual dop is such that, on a boolean algebra, op(ch_1, ..., ch_n) ≡ ¬dop(¬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). Duality also applies to Truth values (⊤/⊥), with existential/universal semantics (◊/□), and 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.formulas — Method
formulas(
     g::AbstractGrammar;
     maxdepth::Integer,
     nformulas::Union{Nothing,Integer} = nothing,
     args...
-)::Vector{<:SyntaxBranch}

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, SyntaxBranch.

source
SoleLogics.formulas — Method
formulas(
+)::Vector{<:SyntaxBranch}

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, SyntaxBranch.

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

Some worlds (dimensional worlds) can be interpreted on dimensional data, that is, n-dimensional arrays. The compatibility of a given world with respect of a structure of a given dimensionality must be specified via the following trait:

goeswithdim(w::AbstractWorld, d) = goeswithdim(typeof(w), d)
+)::Vector{SyntaxBranch}

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

See also AbstractGrammar, SyntaxBranch.

source
SoleLogics.goeswithdim — Method

Some worlds (dimensional worlds) can be interpreted on dimensional data, that is, n-dimensional arrays. The compatibility of a given world with respect of a structure of a given dimensionality must be specified via the following trait:

goeswithdim(w::AbstractWorld, d) = goeswithdim(typeof(w), d)
 goeswithdim(W::Type{<:AbstractWorld}, d::Integer) = goeswithdim(W, Val(d))
 goeswithdim(::Type{<:AbstractWorld}, ::Val) = false

Examples

julia> SoleLogics.goeswithdim(OneWorld, 0)
 true
@@ -748,7 +748,7 @@
 
 julia> all([SoleLogics.goeswithdim.(SoleLogics.Point{N}, N) for N in 1:10])
 true
-

See also OneWorld, World, Interval, Interval2D, GeometricalWorld, AbstractWorld.

source
SoleLogics.hasdual — Method
dual(op::SyntaxToken)

Return the dual of an Operator. Given an operator op of arity n, the dual dop is such that, on a boolean algebra, op(ch_1, ..., ch_n) ≡ ¬dop(¬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). Duality also applies to Truth values (⊤/⊥), with existential/universal semantics (◊/□), and 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.hasdual — Method
dual(op::SyntaxToken)

Return the dual of an Operator. Given an operator op of arity n, the dual dop is such that, on a boolean algebra, op(ch_1, ..., ch_n) ≡ ¬dop(¬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). Duality also applies to Truth values (⊤/⊥), with existential/universal semantics (◊/□), and 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.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
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
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) operator.

Examples

julia> SoleLogics.isbox(◊)
 false
 
@@ -776,22 +776,22 @@
 false
 
 julia> SoleLogics.isbox(□)
-true
source
SoleLogics.iscommutative — Method
iscommutative(c::Connective)

Return whether a connective is known to be commutative.

Examples

julia> iscommutative(∧)
+true
source
SoleLogics.iscommutative — Method
iscommutative(c::Connective)

Return whether a connective is known to be commutative.

Examples

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

Note that nullary and unary connectives are considered commutative.

See also Connective.

Implementation

When implementing a new type for a commutative connective C with arity higher than 1, please provide a method iscommutative(::C). This can help model checking operations.

See also Connective.

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
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");
+false

Note that nullary and unary connectives are considered commutative.

See also Connective.

Implementation

When implementing a new type for a commutative connective C with arity higher than 1, please provide a method iscommutative(::C). This can help model checking operations.

See also Connective.

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
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
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.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.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.leaves — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -802,7 +802,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

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

See also propositionallogic, AbstractAlphabet, AbstractAlgebra.

source
SoleLogics.natoms — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -832,7 +832,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.nconnectives — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.nconnectives — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -843,7 +843,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.nleaves — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.nleaves — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -854,7 +854,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.noperators — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.noperators — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -865,7 +865,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

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

See also SyntaxTree), Formula.

source
SoleLogics.ntokens — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -890,7 +890,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.ntruths — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.ntruths — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -901,7 +901,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.operators — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.operators — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -912,14 +912,14 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
SoleLogics.parsebaseformula — Method
parsebaseformula(
     expression::String,
     additional_operators::Union{Nothing,Vector{<:Operator}} = nothing;
     operators::Union{Nothing,Vector{<:Operator}},
     grammar::Union{Nothing,AbstractGrammar} = nothing,
     algebra::Union{Nothing,AbstractAlgebra} = nothing,
     kwargs...
-)::AnchoredFormula

Return a AnchoredFormula which is the result of parsing expression via the Shunting yard algorithm. By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_OPERATORS; 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.

source
SoleLogics.parseformula — Method
parseformula(expr::String, additional_operators = nothing; kwargs...)
+)::AnchoredFormula

Return a AnchoredFormula which is the result of parsing expression via the Shunting yard algorithm. By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_OPERATORS; 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.

source
SoleLogics.parseformula — Method
parseformula(expr::String, additional_operators = nothing; kwargs...)
 parseformula(F::Type{<:Formula}, expr::String, additional_operators = nothing; kwargs...)

Parse a formula of type F from a string expression (its syntaxstring). When F is not specified, it defaults to SyntaxTree.

By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_OPERATORS (e.g., ¬, ∧, ∨, →); additional, non-standard operators may be provided as a vector additional_operators, and their syntaxstring's will be used for parsing them. Note that, in case of clashing syntaxstring's, the provided additional operators will override the standard ones.

When parsing SyntaxTrees, the Shunting yard algorithm is used, and the method allows the following keywords arguments.

Keyword Arguments

  • function_notation::Bool = false: if set to true, the expression is considered in function notation (e.g., "⨁(arg1, arg2)"); otherwise, it is considered in infix notation (e.g., "arg1 ⨁ arg2");
  • atom_parser::Base.Callable = Atom{String}: a callable to be used for parsing atoms, once they are recognized in the expression. It must return the atom, or the Atom itself;
  • additional_whitespaces::Vector{Char} = Char[]: characters to be stripped out from each syntax token. For example, if '@' in additional_whitespaces, "¬@p@" is parsed just as "¬p".
  • opening_parenthesis::String = "(": the string signaling the opening of an expression block;
  • closing_parenthesis::String = ")": the string signaling the closing of an expression block;
  • arg_delim::String = ",": when function_notation = true, the string that delimits the different arguments of a function call.
Warning

For a proper functioning, the syntaxstring of any syntax token cannot be prefixed/suffixed by whitespaces. For example, for any operator ⨁, it should hold that syntaxstring(⨁) == strip(syntaxstring(⨁)). Also, syntaxstrings cannot contain special symbols (opening_parenthesis, closing_parenthesis, and arg_delim) as substrings.

Examples

julia> syntaxstring(parseformula("¬p∧q∧(¬s∧¬z)"))
 "¬p ∧ q ∧ ¬s ∧ ¬z"
 
@@ -927,7 +927,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, syntaxstring.

source
SoleLogics.precedence — Method
precedence(c::Connective)

Return the precedence of a binary connective.

When using infix notation, and in the absence of parentheses, precedence establishes how binary connectives are interpreted. A precedence value is a standard integer, and connectives with high precedence take precedence over connectives with lower precedences. This affects how formulas are shown (via syntaxstring) and parsed (via parseformula).

By default, the value for a NamedConnective is derived from the Base.operator_precedence of its symbol (name); there are some exceptions (e.g., ¬). Because of this, when dealing with a custom connective ⊙, it will be the case that parseformula("p ⊙ q ∧ r") == (@synexpr p ⊙ q ∧ r).

It is possible to assign a specific precedence to a connective type C by providing a method Base.operator_precedence(::C).

Examples

julia> precedence(∧) == Base.operator_precedence(:∧)
+"(¬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, syntaxstring.

source
SoleLogics.precedence — Method
precedence(c::Connective)

Return the precedence of a binary connective.

When using infix notation, and in the absence of parentheses, precedence establishes how binary connectives are interpreted. A precedence value is a standard integer, and connectives with high precedence take precedence over connectives with lower precedences. This affects how formulas are shown (via syntaxstring) and parsed (via parseformula).

By default, the value for a NamedConnective is derived from the Base.operator_precedence of its symbol (name); there are some exceptions (e.g., ¬). Because of this, when dealing with a custom connective ⊙, it will be the case that parseformula("p ⊙ q ∧ r") == (@synexpr p ⊙ q ∧ r).

It is possible to assign a specific precedence to a connective type C by providing a method Base.operator_precedence(::C).

Examples

julia> precedence(∧) == Base.operator_precedence(:∧)
 true
 
 julia> precedence(∧), precedence(∨), precedence(→)
@@ -940,7 +940,7 @@
 "(¬a) → (b ∧ c)"
 
 julia> syntaxstring(parseformula("a ∧ b → c ∧ d"))
-"(a ∧ b) → (c ∧ d)"

See also associativity, Connective.

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

See also modallogic, AbstractAlphabet, AbstractAlgebra.

source
SoleLogics.randbaseformula — Method
randformula(
     height::Integer,
     alphabet,
     operators::AbstractVector;
@@ -967,7 +967,7 @@
     g::AbstractGrammar;
     rng::Union{Integer,AbstractRNG} = Random.GLOBAL_RNG
 )::SyntaxTree

Return a pseudo-randomic SyntaxBranch.

Arguments

  • height::Integer: height of the generated structure;
  • alphabet::AbstractAlphabet: collection from which atoms are chosen randomly;
  • operators::AbstractVector: vector from which legal operators are chosen;
  • g::AbstractGrammar: alternative to passing alphabet and operators separately. (TODO explain?)

Keyword Arguments

  • rng::Union{Intger,AbstractRNG} = Random.GLOBAL_RNG: random number generator;
  • atompicker::Function = method used to pick a random element. For example, this could be Base.rand or StatsBase.sample.
  • opweights::AbstractWeights = weight vector over the set of operators (see StatsBase).

Examples

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

See also AbstractAlphabet, SyntaxBranch.

source
SoleLogics.randformula — Method
randformula(
     height::Integer,
     alphabet,
     operators::AbstractVector;
@@ -980,16 +980,16 @@
     g::AbstractGrammar;
     rng::Union{Integer,AbstractRNG} = Random.GLOBAL_RNG
 )::SyntaxTree

Return a pseudo-randomic SyntaxBranch.

Arguments

  • height::Integer: height of the generated structure;
  • alphabet::AbstractAlphabet: collection from which atoms are chosen randomly;
  • operators::AbstractVector: vector from which legal operators are chosen;
  • g::AbstractGrammar: alternative to passing alphabet and operators separately. (TODO explain?)

Keyword Arguments

  • rng::Union{Intger,AbstractRNG} = Random.GLOBAL_RNG: random number generator;
  • atompicker::Function = method used to pick a random element. For example, this could be Base.rand or StatsBase.sample.
  • opweights::AbstractWeights = weight vector over the set of operators (see StatsBase).

Examples

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

See also AbstractAlphabet, SyntaxBranch.

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

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

See also AbstractFrame.

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

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

See also AbstractFrame.

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)")))
+"¬((¬(¬(2))) → ((1 → 2) → (1 → 2)))"

See also AbstractAlphabet, SyntaxBranch.

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

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

See also AbstractFrame.

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

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

See also AbstractFrame.

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

See also SyntaxTree), Formula.

source
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)
@@ -1005,7 +1005,7 @@
 "◊((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 kwargs...) 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 SyntaxBranchs, 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.tokens — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+"◊(→(∧(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 kwargs...) 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 SyntaxBranchs, 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.tokens — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -1016,7 +1016,7 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

source
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.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.treewalk — Method
treewalk(
     st::SyntaxTree,
     args...;
     rng::AbstractRNG = Random.GLOBAL_RNG,
@@ -1024,7 +1024,7 @@
     toleaf::Bool = true,
     returnnode::Bool = false,
     transformnode::Function = nothing,
-)::SyntaxTree

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

  • criterion: function used to calculate 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.

TODO explain better TODO is this available in AbstractTrees?

source
SoleLogics.truths — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
+)::SyntaxTree

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

  • criterion: function used to calculate 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.

TODO explain better TODO is this available in AbstractTrees?

source
SoleLogics.truths — Method
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
 atoms(φ::Formula)::AbstractVector{<:Atom}
 truths(φ::Formula)::AbstractVector{<:Truth}
 leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
@@ -1035,15 +1035,15 @@
 ntruths(φ::Formula)::Integer
 nleaves(φ::Formula)::Integer
 nconnectives(φ::Formula)::Integer
-noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

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
StatsBase.sample — Function
StatsBase.sample(
+noperators(φ::Formula)::Integer

Return the list/number of (non-unique) SyntaxTokens, Atomss, etc... appearing in a formula.

See also Formula, SyntaxToken.

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
StatsBase.sample — Function
StatsBase.sample(
     [rng::AbstractRNG = Random.GLOBAL_RNG, ]
     g::AbstractGrammar,
     height::Integer,
     args...;
     kwargs...
-)::Formula

Randomly sample a logic formula of given height from a grammar g.

Implementation

This method for must be implemented, and additional keyword arguments should be provided in order to limit the (otherwise infinite) sampling domain.

See also `AbstractAlphabet'.

source
SoleLogics.@atoms — Macro
@atoms(ps...)

Instantiate a collection of Atoms and return them as a vector.

Info

Atoms instantiated with this macro are defined in the global scope as constants.

Examples

julia> SoleLogics.@atoms String p q r s
+)::Formula

Randomly sample a logic formula of given height from a grammar g.

Implementation

This method for must be implemented, and additional keyword arguments should be provided in order to limit the (otherwise infinite) sampling domain.

See also `AbstractAlphabet'.

source
SoleLogics.@atoms — Macro
@atoms(ps...)

Instantiate a collection of Atoms and return them as a vector.

Info

Atoms instantiated with this macro are defined in the global scope as constants.

Examples

julia> SoleLogics.@atoms String p q r s
 4-element Vector{Atom{String}}:
  Atom{String}("p")
  Atom{String}("q")
@@ -1051,11 +1051,11 @@
  Atom{String}("s")
 
 julia> p
-Atom{String}("p")
source
SoleLogics.@synexpr — Macro
@synexpr(expression)

Return an expression after automatically instantiating undefined Atoms.

Info

Every identified atom is of type Atom{String}.

Examples

julia> @synexpr x = p # Atom{String}("p") is assigned to the global variable x
+Atom{String}("p")
source
SoleLogics.@synexpr — Macro
@synexpr(expression)

Return an expression after automatically instantiating undefined Atoms.

Info

Every identified atom is of type Atom{String}.

Examples

julia> @synexpr x = p # Atom{String}("p") is assigned to the global variable x
 Atom{String}("p")
 
 julia> @synexpr st = p ∧ q → r
 (p ∧ q) → r
 
 julia> typeof(st)
-SyntaxBranch{SoleLogics.NamedConnective{:→}}
source
+SyntaxBranch{SoleLogics.NamedConnective{:→}}source diff --git a/dev/getting-started/index.html b/dev/getting-started/index.html index 1dc48d65..1d0963b4 100644 --- a/dev/getting-started/index.html +++ b/dev/getting-started/index.html @@ -50,7 +50,7 @@ "(¬a) → (b ∧ c)" julia> syntaxstring(parseformula("a ∧ b → c ∧ d")) -"(a ∧ b) → (c ∧ d)"

See also associativity, Connective.

source
SoleLogics.associativity — Function
associativity(::Connective)

Return whether a (binary) connective is right-associative.

When using infix notation, and in the absence of parentheses, associativity establishes how binary connectives of the sameprecedenceare interpreted. This affects how formulas are shown (viasyntaxstring) and parsed (viaparseformula`).

By default, the value for a NamedConnective is derived from the Base.operator_precedence of its symbol (name); thus, for example, most connectives are left-associative (e.g., ∧ and ∨), while → is right-associative. Because of this, when dealing with a custom connective ⊙, it will be the case that parseformula("p ⊙ q ∧ r") == (@synexpr p ⊙ q ∧ r).

Examples

julia> associativity(∧)
+"(a ∧ b) → (c ∧ d)"

See also associativity, Connective.

source
SoleLogics.associativity — Function
associativity(::Connective)

Return whether a (binary) connective is right-associative.

When using infix notation, and in the absence of parentheses, associativity establishes how binary connectives of the sameprecedenceare interpreted. This affects how formulas are shown (viasyntaxstring) and parsed (viaparseformula`).

By default, the value for a NamedConnective is derived from the Base.operator_precedence of its symbol (name); thus, for example, most connectives are left-associative (e.g., ∧ and ∨), while → is right-associative. Because of this, when dealing with a custom connective ⊙, it will be the case that parseformula("p ⊙ q ∧ r") == (@synexpr p ⊙ q ∧ r).

Examples

julia> associativity(∧)
 :left
 
 julia> associativity(→)
@@ -60,11 +60,11 @@
 "p → (q → r)"
 
 julia> syntaxstring(parseformula("p ∧ q ∨ r"); remove_redundant_parentheses = false)
-"(p ∧ q) ∨ r"

See also Connective, parseformula, precedence, syntaxstring.

source
SoleLogics.iscommutative — Function
iscommutative(c::Connective)

Return whether a connective is known to be commutative.

Examples

julia> iscommutative(∧)
+"(p ∧ q) ∨ r"

See also Connective, parseformula, precedence, syntaxstring.

source
SoleLogics.iscommutative — Function
iscommutative(c::Connective)

Return whether a connective is known to be commutative.

Examples

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

Note that nullary and unary connectives are considered commutative.

See also Connective.

Implementation

When implementing a new type for a commutative connective C with arity higher than 1, please provide a method iscommutative(::C). This can help model checking operations.

See also Connective.

source

To learn more about operators, refer to Propositional Logic and Modal Logic chapters.

Formulas

TODO: the following definition might be unclear, since "evaluation" and "logic" are not concepts already read by the user. When the Logic structure will be removed from SoleLogics, this section will be expanded with semantics-related concepts.

Missing docstring.

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

Note

SoleLogics.jl offers the possibility to implement a custom Formula subtype. To see an in-depth example, please refer to section Customization.

SoleLogics.composeformulas — Function
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)");
+false

Note that nullary and unary connectives are considered commutative.

See also Connective.

Implementation

When implementing a new type for a commutative connective C with arity higher than 1, please provide a method iscommutative(::C). This can help model checking operations.

See also Connective.

source

To learn more about operators, refer to Propositional Logic and Modal Logic chapters.

Formulas

TODO: the following definition might be unclear, since "evaluation" and "logic" are not concepts already read by the user. When the Logic structure will be removed from SoleLogics, this section will be expanded with semantics-related concepts.

Missing docstring.

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

Note

SoleLogics.jl offers the possibility to implement a custom Formula subtype. To see an in-depth example, please refer to section Customization.

SoleLogics.composeformulas — Function
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");
 
@@ -92,7 +92,7 @@
     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
Missing docstring.

Missing docstring for tokens(::Formula). Check Documenter's build log for details.

SoleLogics.height — Method
height(φ::Formula)::Integer

Return the height of a formula in its syntax tree representation.

See also SyntaxTree.

source
Missing docstring.

Missing docstring for SoleLogics.tree(::Formula). Check Documenter's build log for details.

Parsing & Printing

SoleLogics.jl allows you to:

These features are highly customizable, and leverage three properties of syntactical tokens: arity, connective precedence and connective associativity.

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

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

The following kwargs are currently supported:

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

Examples

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

To allow for the composition of Formulas of different types, promotion rules should be provided.

See also Formula, Connective.

source
Missing docstring.

Missing docstring for tokens(::Formula). Check Documenter's build log for details.

SoleLogics.height — Method
height(φ::Formula)::Integer

Return the height of a formula in its syntax tree representation.

See also SyntaxTree.

source
Missing docstring.

Missing docstring for SoleLogics.tree(::Formula). Check Documenter's build log for details.

Parsing & Printing

SoleLogics.jl allows you to:

These features are highly customizable, and leverage three properties of syntactical tokens: arity, connective precedence and connective associativity.

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

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

The following kwargs are currently supported:

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

Examples

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"))
 "p ∧ q ∧ r ∧ s ∧ t"
 
 julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), function_notation=true)
@@ -108,7 +108,7 @@
 "◊((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 kwargs...) 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 SyntaxBranchs, 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.parseformula — Function
parseformula(expr::String, additional_operators = nothing; kwargs...)
+"◊(→(∧(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 kwargs...) 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 SyntaxBranchs, 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.parseformula — Function
parseformula(expr::String, additional_operators = nothing; kwargs...)
 parseformula(F::Type{<:Formula}, expr::String, additional_operators = nothing; kwargs...)

Parse a formula of type F from a string expression (its syntaxstring). When F is not specified, it defaults to SyntaxTree.

By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_OPERATORS (e.g., ¬, ∧, ∨, →); additional, non-standard operators may be provided as a vector additional_operators, and their syntaxstring's will be used for parsing them. Note that, in case of clashing syntaxstring's, the provided additional operators will override the standard ones.

When parsing SyntaxTrees, the Shunting yard algorithm is used, and the method allows the following keywords arguments.

Keyword Arguments

  • function_notation::Bool = false: if set to true, the expression is considered in function notation (e.g., "⨁(arg1, arg2)"); otherwise, it is considered in infix notation (e.g., "arg1 ⨁ arg2");
  • atom_parser::Base.Callable = Atom{String}: a callable to be used for parsing atoms, once they are recognized in the expression. It must return the atom, or the Atom itself;
  • additional_whitespaces::Vector{Char} = Char[]: characters to be stripped out from each syntax token. For example, if '@' in additional_whitespaces, "¬@p@" is parsed just as "¬p".
  • opening_parenthesis::String = "(": the string signaling the opening of an expression block;
  • closing_parenthesis::String = ")": the string signaling the closing of an expression block;
  • arg_delim::String = ",": when function_notation = true, the string that delimits the different arguments of a function call.
Warning

For a proper functioning, the syntaxstring of any syntax token cannot be prefixed/suffixed by whitespaces. For example, for any operator ⨁, it should hold that syntaxstring(⨁) == strip(syntaxstring(⨁)). Also, syntaxstrings cannot contain special symbols (opening_parenthesis, closing_parenthesis, and arg_delim) as substrings.

Examples

julia> syntaxstring(parseformula("¬p∧q∧(¬s∧¬z)"))
 "¬p ∧ q ∧ ¬s ∧ ¬z"
 
@@ -116,13 +116,13 @@
 "¬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, syntaxstring.

source

Grammar

Missing docstring.

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

Note

SoleLogics.jl offers the possibility to implement a custom AbstractAlphabet concrete type. To see an in-depth example, please refer to section Customization.

Missing docstring.

Missing docstring for atoms(a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.in(p::Atom, a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.length(a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.iterate(a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

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

Missing docstring.

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

Missing docstring.

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

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(
+"(¬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, syntaxstring.

source

Grammar

Missing docstring.

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

Note

SoleLogics.jl offers the possibility to implement a custom AbstractAlphabet concrete type. To see an in-depth example, please refer to section Customization.

Missing docstring.

Missing docstring for atoms(a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.in(p::Atom, a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.length(a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

Missing docstring for Base.iterate(a::AbstractAlphabet). Check Documenter's build log for details.

Missing docstring.

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

Missing docstring.

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

Missing docstring.

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

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{<:SyntaxBranch}

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, SyntaxBranch.

source
Missing docstring.

Missing docstring for CompleteFlatGrammar{A<:AbstractAlphabet,O<:Operator}. Check Documenter's build log for details.

SoleLogics.formulas — Method
formulas(
+)::Vector{<:SyntaxBranch}

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, SyntaxBranch.

source
Missing docstring.

Missing docstring for CompleteFlatGrammar{A<:AbstractAlphabet,O<:Operator}. Check Documenter's build log for details.

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

Semantics

Customization

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nunc justo justo, finibus ac odio in, tempor fermentum augue. Vivamus ullamcorper lacus eget enim imperdiet, ac lobortis turpis elementum. Fusce non auctor eros. Duis scelerisque auctor volutpat. Morbi non luctus est. Orci varius natoque penatibus et magnis dis parturient montes, nascetur ridiculus mus. Pellentesque porttitor a est sit amet ornare. Aliquam faucibus fringilla imperdiet.

+)::Vector{SyntaxBranch}

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

See also AbstractGrammar, SyntaxBranch.

source

Semantics

Customization

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nunc justo justo, finibus ac odio in, tempor fermentum augue. Vivamus ullamcorper lacus eget enim imperdiet, ac lobortis turpis elementum. Fusce non auctor eros. Duis scelerisque auctor volutpat. Morbi non luctus est. Orci varius natoque penatibus et magnis dis parturient montes, nascetur ridiculus mus. Pellentesque porttitor a est sit amet ornare. Aliquam faucibus fringilla imperdiet.

diff --git a/dev/index.html b/dev/index.html index cb43fc66..75952225 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,3 +1,3 @@ Home · SoleLogics.jl
Edit on GitHub

SoleLogics

Introduction

Welcome to the documentation for SoleLogics, a Julia package for computational logic. SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning.

Installation

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

using Pkg
-Pkg.add("SoleLogics")

Feature Summary

SoleLogics.jl allows easy manipulation of:

  • Syntax tokens (e.g., atoms, logical constants/connectives, etc.);
  • Alphabets, grammars, algebras (e.g., crisp, fuzzy), logics (e.g., propositional and (multi)modal);
  • Formulas (e.g., syntax trees, DNFs, CNFs): random generation, parsing, minimization;
  • Interpretations (e.g., propositional assignments, Kripke structures);
  • Algorithms for evaluating the: validity/satisfiability of a formula, and truth of a formula on an interpretation (model checking).
+Pkg.add("SoleLogics")

Feature Summary

SoleLogics.jl allows easy manipulation of:

diff --git a/dev/modal-logic/index.html b/dev/modal-logic/index.html index 4682d515..99f4777b 100644 --- a/dev/modal-logic/index.html +++ b/dev/modal-logic/index.html @@ -1,2 +1,2 @@ -Modal logic · SoleLogics.jl
Edit on GitHub
+Modal logic · SoleLogics.jl
Edit on GitHub
diff --git a/dev/propositional-logic/index.html b/dev/propositional-logic/index.html index 8a433a0f..e69bbb6a 100644 --- a/dev/propositional-logic/index.html +++ b/dev/propositional-logic/index.html @@ -1,2 +1,2 @@ -Propositional logic · SoleLogics.jl
Edit on GitHub
+Propositional logic · SoleLogics.jl
Edit on GitHub
diff --git a/dev/search/index.html b/dev/search/index.html index c0e7be65..e35a8d72 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...