diff --git a/src/algebras/frames/full-dimensional-frame/main.jl b/src/algebras/frames/full-dimensional-frame/main.jl
index bdd965b0..227b4b02 100644
--- a/src/algebras/frames/full-dimensional-frame/main.jl
+++ b/src/algebras/frames/full-dimensional-frame/main.jl
@@ -63,7 +63,7 @@ See also
 [`Interval`](@ref),
 [`Interval2D`](@ref),
 [`IntervalRelation`](@ref),
-[`IntervalRelation2D`](@ref),
+[`RectangleRelation`](@ref),
 [`accessibles`](@ref),
 [`AbstractDimensionalFrame`](@ref), [`AbstractMultiModalFrame`](@ref).
 """
diff --git a/src/anchored-formula.jl b/src/anchored-formula.jl
index 0e4bdb67..41b384d6 100644
--- a/src/anchored-formula.jl
+++ b/src/anchored-formula.jl
@@ -23,17 +23,17 @@ See the examples.
 
 # Examples
 ```julia-repl
-julia> f = parsebaseformula("◊(p→q)");
+julia> φ = parsebaseformula("◊(p→q)");
 
-julia> f2 = f(parseformula("p"));
+julia> f2 = φ(parseformula("p"));
 
-julia> syntaxstring(f)
+julia> syntaxstring(φ)
 "◊(→(p, q))"
 
 julia> syntaxstring(f2)
 "p"
 
-julia> @assert logic(f) == logic(f2)
+julia> @assert logic(φ) == logic(f2)
 
 julia> @assert ◊ in operators(logic(f2))
 
@@ -99,15 +99,31 @@ struct AnchoredFormula{L<:AbstractLogic} <: Formula
     end
 end
 
-_logic(f::AnchoredFormula) = f._logic
-logic(f::AnchoredFormula) = f._logic[]
-synstruct(f::AnchoredFormula) = f.synstruct
-tree(f::AnchoredFormula) = tree(f.synstruct)
+_logic(φ::AnchoredFormula) = φ._logic
 
-function Base.show(io::IO, f::AnchoredFormula)
-    println(io, "AnchoredFormula: $(syntaxstring(f))")
+"""
+    logic(φ::AnchoredFormula)::AbstractLogic
+
+Return the logic of an anchored formula
+
+See [`AnchoredFormula`](@ref).
+"""
+logic(φ::AnchoredFormula) = φ._logic[]
+
+"""
+    logic(φ::AnchoredFormula)::AbstractSyntaxStructure
+
+Return the syntactic component of an anchored formula.
+
+See [`AnchoredFormula`](@ref).
+"""
+synstruct(φ::AnchoredFormula) = φ.synstruct
+tree(φ::AnchoredFormula) = tree(φ.synstruct)
+
+function Base.show(io::IO, φ::AnchoredFormula)
+    println(io, "AnchoredFormula: $(syntaxstring(φ))")
     print(io, "Anchored to logic: ")
-    Base.show(io, logic(f))
+    Base.show(io, logic(φ))
 end
 
 # Note that, since `c` might not be in the logic of the child formulas,
@@ -124,7 +140,7 @@ function composeformulas(c::Connective, φs::NTuple{N,AnchoredFormula}) where {N
 end
 
 # When constructing a new formula from a syntax tree, the logic is passed by reference.
-(f::AnchoredFormula)(t::AbstractSyntaxStructure, args...) = AnchoredFormula(_logic(f), t, args...)
+(φ::AnchoredFormula)(t::AbstractSyntaxStructure, args...) = AnchoredFormula(_logic(φ), t, args...)
 
 # A logic can be used to instantiate `AnchoredFormula`s out of syntax trees.
 (l::AbstractLogic)(t::AbstractSyntaxStructure, args...) = AnchoredFormula(Base.RefValue(l), t; args...)
@@ -136,17 +152,17 @@ function Base._promote(x::AnchoredFormula, y::AbstractSyntaxStructure)
 end
 Base._promote(x::AbstractSyntaxStructure, y::AnchoredFormula) = reverse(Base._promote(y, x))
 
-iscrisp(f::AnchoredFormula) = iscrisp(logic(f))
-grammar(f::AnchoredFormula) = grammar(logic(f))
-algebra(f::AnchoredFormula) = algebra(logic(f))
+iscrisp(φ::AnchoredFormula) = iscrisp(logic(φ))
+grammar(φ::AnchoredFormula) = grammar(logic(φ))
+algebra(φ::AnchoredFormula) = algebra(logic(φ))
 
-syntaxstring(f::AnchoredFormula; kwargs...) = syntaxstring(f.synstruct; kwargs...)
+syntaxstring(φ::AnchoredFormula; kwargs...) = syntaxstring(φ.synstruct; kwargs...)
 
 ############################################################################################
 
 
-subformulas(f::AnchoredFormula; kwargs...) = f.(subformulas(tree(f); kwargs...))
-normalize(f::AnchoredFormula; kwargs...) = f(normalize(tree(f); kwargs...))
+subformulas(φ::AnchoredFormula; kwargs...) = φ.(subformulas(tree(φ); kwargs...))
+normalize(φ::AnchoredFormula; kwargs...) = φ(normalize(tree(φ); kwargs...))
 
 """
     function baseformula(
diff --git a/src/base-logic.jl b/src/base-logic.jl
index cc7a14a3..29cc09e3 100644
--- a/src/base-logic.jl
+++ b/src/base-logic.jl
@@ -373,7 +373,7 @@ end
 Basic logical operators.
 
 See also [`NEGATION`](@ref),
-[`CONJUCTION`](@ref),
+[`CONJUNCTION`](@ref),
 [`DISJUNCTION`](@ref),
 [`IMPLICATION`](@ref),
 [`Connective`](@ref).
diff --git a/src/core.jl b/src/core.jl
index b8fc2ce4..78e7ec2b 100644
--- a/src/core.jl
+++ b/src/core.jl
@@ -734,9 +734,9 @@ See also
 [`arity`](@ref),
 [`Connective`](@ref),
 [`height`](@ref),
-[`atoms`](@ref), [`natoms`](@ref), [`atomstype`](@ref),
-[`operators`](@ref), [`noperators`](@ref), [`operatorstype`](@ref),
-[`tokens`](@ref), [`ntokens`](@ref), [`tokenstype`](@ref),
+[`atoms`](@ref), [`natoms`](@ref),
+[`operators`](@ref), [`noperators`](@ref),
+[`tokens`](@ref), [`ntokens`](@ref),
 """
 struct SyntaxBranch{T<:Connective} <: SyntaxTree
 
diff --git a/src/interpretation-sets.jl b/src/interpretation-sets.jl
index 1c1d79ad..49535278 100644
--- a/src/interpretation-sets.jl
+++ b/src/interpretation-sets.jl
@@ -13,7 +13,7 @@ identified by an index i_instance::Integer.
 These structures are especially useful when performing
 [model checking](https://en.wikipedia.org/wiki/Model_checking).
 
-See also [`valuetype`](@ref), [`truthtype`](@ref),
+See also[`truthtype`](@ref),
 [`InterpretationVector`](@ref).
 """
 abstract type AbstractInterpretationSet{M<:AbstractInterpretation} <: AbstractDataset end
diff --git a/src/logics.jl b/src/logics.jl
index bcb36612..c59b0c7e 100644
--- a/src/logics.jl
+++ b/src/logics.jl
@@ -52,7 +52,7 @@ By default, an alphabet is considered finite:
     Base.in(p::Atom, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, atoms(a)) : error(...)
 
 See also [`AbstractGrammar`](@ref), [`AlphabetOfAny`](@ref), [`Atom`](@ref),
-[`ExplicitAlphabet`](@ref), [`atomstype`](@ref),  [`valuetype`](@ref).
+[`ExplicitAlphabet`](@ref).
 """
 abstract type AbstractAlphabet{V} end
 
@@ -76,7 +76,7 @@ Base.isfinite(a::AbstractAlphabet) = Base.isfinite(typeof(a))
 
 List the atoms of a *finite* alphabet.
 
-See also [`AbstractAlphabet`](@ref), [`Base.isfinite`](@ref).
+See also [`AbstractAlphabet`](@ref).
 """
 function atoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}
     if Base.isfinite(a)
@@ -214,8 +214,6 @@ that consists of all the (singleton) child types of `O`.
 V context-free grammar is a simple structure for defining formulas inductively.
 
 See also [`alphabet`](@ref),
-[`atomstype`](@ref), [`tokenstype`](@ref),
-[`operatorstype`](@ref), [`alphabettype`](@ref),
 [`AbstractAlphabet`](@ref), [`Operator`](@ref).
 """
 abstract type AbstractGrammar{V<:AbstractAlphabet,O<:Operator} end
diff --git a/src/modal-logic.jl b/src/modal-logic.jl
index bcc0ae5d..c04213e3 100644
--- a/src/modal-logic.jl
+++ b/src/modal-logic.jl
@@ -527,6 +527,13 @@ function interpret(
     return error("Please, provide method interpret(::$(typeof(φ)), ::$(typeof(i)), ::$(typeof(w))).")
 end
 
+"""
+    frame(i::AbstractKripkeStructure)::AbstractFrame
+
+Return the frame of a Kripke structure.
+
+See also [`AbstractFrame`](@ref), [`AbstractKripkeStructure`](@ref).
+"""
 function frame(i::AbstractKripkeStructure)::AbstractFrame
     return error("Please, provide method frame(i::$(typeof(i))).")
 end
diff --git a/src/random.jl b/src/random.jl
index 422733c4..7f5e9410 100644
--- a/src/random.jl
+++ b/src/random.jl
@@ -29,7 +29,6 @@ otherwise, it must be implemented, and additional keyword arguments should be pr
 in order to limit the (otherwise infinite) sampling domain.
 
 See also
-[`isfinite`](@ref),
 [`AbstractAlphabet'](@ref).
 """
 function Base.rand(alphabet::AbstractAlphabet, args...; kwargs...)