More on Formulas

More on Formulas

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

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

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

Formula
- SyntaxStructure
  - Literal
  - LeftmostLinearForm

Literals

SoleLogics.Literal — Type

struct Literal{T<:SyntaxLeaf} <: SyntaxStructure
    ispos::Bool
    atom::T
end

An atom, or its negation.

See also CNF, DNF, SyntaxStructure.

source

Linear Forms

SoleLogics.LeftmostLinearForm — Type

struct LeftmostLinearForm{C<:Connective,SS<:SyntaxStructure} <: SyntaxStructure
    grandchildren::Vector{<:SS}
end

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

const LeftmostConjunctiveForm{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}
const LeftmostDisjunctiveForm{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}

const CNF{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∧),LeftmostLinearForm{typeof(∨),SS}}
const DNF{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∨),LeftmostLinearForm{typeof(∧),SS}}

Examples

julia> LeftmostLinearForm(→, parseformula.(["p", "q", "r"]))
LeftmostLinearForm{SoleLogics.NamedConnective{:→},Atom{String}}
    "(p) → (q) → (r)"

julia> LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))
LeftmostLinearForm{SoleLogics.NamedConnective{:∧},SyntaxTree}
    "(¬p) ∧ (q) ∧ (¬r)"

julia> LeftmostDisjunctiveForm{Literal}([Literal(false, Atom("p")), Literal(true, Atom("q")), Literal(false, Atom("r"))])
LeftmostLinearForm{SoleLogics.NamedConnective{:∨},Literal}
    "(¬p) ∨ (q) ∨ (¬r)"

julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa DNF
true

julia> conj = LeftmostConjunctiveForm(@atoms p q)
LeftmostConjunctiveForm with 2 Atom{String} grandchildren:
        p
        q

julia> tree(conj)
SyntaxBranch: p ∧ q

julia> nconj = NEGATION(conj)
LeftmostLinearForm with connective ¬ and 1 LeftmostConjunctiveForm{Atom{String}} grandchildren:
        (p) ∧ (q)

julia> tree(nconj)
SyntaxBranch: ¬(p ∧ q)

julia> tree(nconj ∧ nconj)
SyntaxBranch: ¬(p ∧ q) ∧ ¬(p ∧ q)

source

SoleLogics.LeftmostConjunctiveForm — Type

LeftmostConjunctiveForm{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∧),SS}

Specific instantiation of a LeftmostLinearForm, where Connectives are all CONJUNCTIONs.

source

SoleLogics.LeftmostDisjunctiveForm — Type

LeftmostDisjunctiveForm{SS<:SyntaxStructure} = LeftmostLinearForm{typeof(∨),SS}

Specific instantiation of a LeftmostLinearForm, where Connectives are all DISJUNCTIONs.

source

SoleLogics.CNF — Type

CNF{SS<:SyntaxStructure} = LeftmostConjunctiveForm{LeftmostDisjunctiveForm{SS}}

Conjunctive Normal Form of an SyntaxStructure.

source

SoleLogics.DNF — Type

DNF{SS<:SyntaxStructure} = LeftmostConjunctiveForm{LeftmostConjunctiveForm{SS}}

Disjunctive Normal Form of an SyntaxStructure.

source

<!–

AnchoredFormula

SoleLogics.AnchoredFormula — Type

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

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

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

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

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

Examples

julia> φ = parseformula(AnchoredFormula, "◊(p→q)");

julia> f2 = φ(parseformula("p"));

julia> syntaxstring(φ)
"◊(→(p, q))"

julia> syntaxstring(f2)
"p"

julia> @assert logic(φ) == logic(f2)

julia> @assert ◊ in operators(logic(f2))

julia> @assert ◊ isa operatorstype(logic(f2))

source

SoleLogics.logic — Method

logic(φ::AnchoredFormula)::AbstractLogic

Return the logic of an anchored formula

See AnchoredFormula.

source

SoleLogics.synstruct — Method

synstruct(φ::AnchoredFormula)::SyntaxStructure

Return the syntactic component of an anchored formula.

See AnchoredFormula.

source

SoleLogics.baseformula — Method

function baseformula(
    φ::Formula;
    infer_logic = true,
    additional_operators::Union{Nothing,Vector{<:Operator}} = nothing,
    kwargs...
)

Attempt at instantiating a AnchoredFormula from a syntax token/formula, by inferring the logic it belongs to. If infer_logic is true, then a canonical logic (e.g., propositional logic with all the BASE_PROPOSITIONAL_CONNECTIVES) is inferred; if it's false, then a logic with exactly the operators appearing in the syntax tree, plus the additional_operators is instantiated.

Examples

julia> t = parseformula("◊((p∧q)→r)");

julia> unique(operators(logic(SoleLogics.baseformula(t))))
3-element Vector{Union{SoleLogics.NamedConnective{:→}, SoleLogics.NamedConnective{:◊}, SoleLogics.NamedConnective{:∧}}}:
 ∧
 ◊
 →

julia> unique(operators(logic(SoleLogics.baseformula(t; additional_operators = SoleLogics.BASE_MODAL_CONNECTIVES))))
8-element Vector{Union{SoleLogics.BottomOperator, SoleLogics.NamedConnective{:¬}, SoleLogics.NamedConnective{:∧}, SoleLogics.NamedConnective{:∨}, SoleLogics.NamedConnective{:→}, SoleLogics.NamedConnective{:◊}, SoleLogics.NamedConnective{:□}, SoleLogics.TopOperator}}:
 ¬
 ∧
 ∨
 →
 ◊
 □

source

SoleLogics.parseformula — Function

parseformula(
    T::Type{AnchoredFormula},
    expr::AbstractString,
    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 an expression via the Shunting yard algorithm. By default, this function is only able to parse operators in SoleLogics.BASE_PARSABLE_CONNECTIVES; additional operators may be provided as a second argument.

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

See parseformula, baseformula, BASE_PARSABLE_CONNECTIVES.

source

–>

Random sampling and generation

Base.rand — Method

Base.rand(
    [rng::Union{Integer,AbstractRNG}=Random.GLOBAL_RNG,]
    alphabet::AbstractAlphabet,
    args...;
    kwargs...
)::Atom

Synonym for randatom(::AbstractAlphabet).

Randomly generate an Atom from a finite AbstractAlphabet according to a uniform distribution.

See also [AbstractAlphabet], randatom(::AbstractAlphabet).

source

SoleLogics.randatom — Function

randatom(
    [rng::Union{Random.AbstractRNG,Integer},]
    a::AbstractAlphabet,
    args...;
    kwargs...
)

Randomly generate an Atom from a finite AbstractAlphabet according to a uniform distribution.

Examples

julia> alphabet = ExplicitAlphabet(1:5)
ExplicitAlphabet{Int64}(Atom{Int64}[Atom{Int64}: 1, Atom{Int64}: 2, Atom{Int64}: 3, Atom{Int64}: 4, Atom{Int64}: 5])

julia> randatom(42, alphabet)
Atom{Int64}: 4

Parsing

SoleLogics.BASE_PARSABLE_CONNECTIVES — Constant

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

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

Utilities

SoleLogics.treewalk — Method

treewalk(
    st::SyntaxTree,
    args...;
    rng::AbstractRNG = Random.GLOBAL_RNG,
    criterion::Function = ntokens,
    toleaf::Bool = true,
    returnnode::Bool = false,
    transformnode::Function = nothing
)::SyntaxTree

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

criterion: function used to compute the probability of stopping at a random node;
returnnode: true if only the subtree is to be returned;
transformnode: function that will be applied to the chosen subtree.

source

SoleLogics.subformulas — Method

subformulas(f::Formula; sorted=true)

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

Examples

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