Introduction
At the end of this chapter, you are going to understand how Atoms and Truth values are arranged into alphabets and grammars.
You will also get an in-depth view of how boolean Truth values and boolean Connective's are defined from both a syntax and a syntactical standpoint of view.
Finally, you will get a clearer idea about how to represent and manipulate interpretations and their outcomes.
Recalling the type hierarchy presented in man-core, it is here enriched with the following new types and structures.
TruthConnectiveAbstractAlphabetAbstractGrammarAbstractAlgebraAbstractLogicAbstractInterpretationTruthTableLogicalInstance
Alphabet
SoleLogics.AbstractAlphabet — Typeabstract type AbstractAlphabet{V} endAbstract 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)
+true
+
+julia> Atom(1) in AlphabetOfAny{String}()
+false
+
+julia> Atom("mystring") in AlphabetOfAny{String}()
+true
+
+julia> "mystring" in AlphabetOfAny{String}()
+┌ Warning: Please, use Base.in(Atom(mystring), alphabet::AlphabetOfAny{String}) instead of Base.in(mystring, alphabet::AlphabetOfAny{String})
+└ @ SoleLogics ...
+trueInterface
atoms(a::AbstractAlphabet)::AbstractVectorBase.isfinite(::Type{<:AbstractAlphabet})::Boolrandatom(rng::Union{Random.AbstractRNG, Integer}, a::AbstractAlphabet, args...; kwargs...)::AbstractAtom
Utility functions
natoms(a::AbstractAlphabet)::BoolBase.in(p::AbstractAtom, a::AbstractAlphabet)::BoolBase.eltype(a::AbstractAlphabet)randatom(a::AbstractAlphabet, args...; kwargs...)::AbstractAtomatomstype(a::AbstractAlphabet)valuetype(a::AbstractAlphabet)
Implementation
When implementing a new alphabet type MyAlphabet, you should provide a method for establishing whether an atom belongs to it or not; while, in general, this method should be:
function Base.in(p::AbstractAtom, a::MyAlphabet)::Boolin the case of finite alphabets, it suffices to define a method:
function atoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}By default, an alphabet is considered finite:
Base.isfinite(::Type{<:AbstractAlphabet}) = true
+Base.isfinite(a::AbstractAlphabet) = Base.isfinite(typeof(a))
+Base.in(p::AbstractAtom, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, atoms(a)) : error(...)See also AbstractGrammar, AlphabetOfAny, AbstractAtom, ExplicitAlphabet.
Base.isfinite — MethodBase.isfinite(a::AbstractAlphabet)Return true if the alphabet is finite, false otherwise.
See AbstractAlphabet.
SoleLogics.atoms — Methodatoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}List the atoms of a finite alphabet.
See also AbstractAlphabet.
SoleLogics.natoms — Methodnatoms(a::AbstractAlphabet)::IntegerReturn the number of atoms of a finite alphabet.
See also randatom, AbstractAlphabet.
Base.in — MethodBase.in(p::AbstractAtom, a::AbstractAlphabet)::BoolReturn whether an atom belongs to an alphabet.
See also AbstractAlphabet, AbstractAtom.
SoleLogics.ExplicitAlphabet — Typestruct ExplicitAlphabet{V} <: AbstractAlphabet{V}
+ atoms::Vector{Atom{V}}
+endAn alphabet wrapping atoms in a (finite) Vector.
See also AbstractAlphabet, atoms.
SoleLogics.AlphabetOfAny — Typestruct AlphabetOfAny{V} <: AbstractAlphabet{V} endAn implicit, infinite alphabet that includes all atoms with values of a subtype of V.
See also AbstractAlphabet.
Grammar
SoleLogics.AbstractGrammar — Typeabstract type AbstractGrammar{V<:AbstractAlphabet,O<:Operator} endAbstract type for representing a context-free grammar based on a single alphabet of type V, and a set of operators that consists of all the (singleton) child types of O. V context-free grammar is a simple structure for defining formulas inductively.
Interface
alphabet(g::AbstractGrammar)::AbstractAlphabetBase.in(::SyntaxTree, g::AbstractGrammar)::Boolformulas(g::AbstractGrammar; kwargs...)::Vector{<:SyntaxTree}
Utility functions
Base.in(a::AbstractAtom, g::AbstractGrammar)atomstype(g::AbstractGrammar)tokenstype(g::AbstractGrammar)operatorstype(g::AbstractGrammar)alphabettype(g::AbstractGrammar)
See also alphabet, AbstractAlphabet, Operator.
SoleLogics.alphabet — Methodalphabet(g::AbstractGrammar{V} where {V})::VReturn the propositional alphabet of a grammar.
See also AbstractAlphabet, AbstractGrammar.
Base.in — MethodBase.in(φ::SyntaxTree, g::AbstractGrammar)::BoolReturn whether a SyntaxTree, belongs to a grammar.
See also AbstractGrammar, SyntaxTree.
SoleLogics.formulas — Methodformulas(
+ g::AbstractGrammar;
+ maxdepth::Integer,
+ nformulas::Union{Nothing,Integer} = nothing,
+ args...
+)::Vector{<:SyntaxTree}Enumerate the formulas produced by a given grammar with a finite and iterable alphabet.
Implementation
Additional args can be used to model the function's behavior. At least these two arguments should be covered:
- a
nformulasargument can be used to limit the size of the returnedVector; - a
maxdepthargument can be used to limit the syntactic component, represented as a syntax tree,
to a given maximum depth;
See also AbstractGrammar, AbstractSyntaxBranch.
SoleLogics.CompleteFlatGrammar — Typestruct CompleteFlatGrammar{V<:AbstractAlphabet,O<:Operator} <: AbstractGrammar{V,O}
+ alphabet::V
+ operators::Vector{<:O}
+endV 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.
SoleLogics.connectives — Methodconnectives(g::AbstractGrammar)List all connectives appearing in a grammar.
See also Connective, nconnectives.
SoleLogics.leaves — MethodSoleLogics.formulas — Methodformulas(
+ 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.
Algebra
SoleLogics.AbstractAlgebra — Typeabstract type AbstractAlgebra{T<:Truth} endAbstract type for representing algebras. Algebras are used for grounding the truth of atoms and the semantics of operators. They typically encode a lattice structure where two elements(or nodes) ⊤ and ⊥ are referred to as TOP (or maximum) and bot (or minimum). Each node in the lattice represents a truth value that an atom or a formula can have on an interpretation, and the semantics of operators is given in terms of operations between truth values.
Interface
truthtype(a::AbstractAlgebra)domain(a::AbstractAlgebra)top(a::AbstractAlgebra)bot(a::AbstractAlgebra)
Utility functions
iscrisp(a::AbstractAlgebra)
Implementation
When implementing a new algebra type, the methods domain, TOP, and bot should be implemented.
See also bot, BooleanAlgebra, Operator, TOP, collatetruth, domain, iscrisp, truthtype.
SoleLogics.truthtype — Methodtruthtype(::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.
SoleLogics.domain — Methoddomain(a::AbstractAlgebra)Return an iterator to the values in the domain of a given algebra.
See also AbstractAlgebra.
SoleLogics.top — MethodSoleLogics.bot — MethodSoleLogics.iscrisp — Methodiscrisp(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.
Logic
SoleLogics.AbstractLogic — Typeabstract type AbstractLogic{G<:AbstractGrammar,A<:AbstractAlgebra} endAbstract type of a logic, which comprehends a context-free grammar (syntax) and an algebra (semantics).
Interface
grammar(l::AbstractLogic)::AbstractGrammaralgebra(l::AbstractLogic)::AbstractAlgebra
Utility functions
- See also
AbstractGrammar - See also
AbstractAlgebra
Implementation
When implementing a new logic type, the methods grammar and algebra should be implemented.
See also AbstractAlgebra, AbstractGrammar.
SoleLogics.grammar — Methodgrammar(l::AbstractLogic{G})::G where {G<:AbstractGrammar}Return the grammar of a given logic.
See also AbstractGrammar, AbstractLogic, algebra, alphabet, formulas, grammar, operators, truthtype.
SoleLogics.algebra — Methodalgebra(l::AbstractLogic{G,V})::V where {G,V}Return the algebra of a given logic.
See also AbstractAlgebra, AbstractLogic.
More on Connectives
SoleLogics.NamedConnective — Typestruct NamedConnective{Symbol} <: Connective endA singleton type for representing connectives defined by a name or a symbol.
Examples
The AND connective (i.e., the logical conjunction) is defined as the subtype:
const CONJUNCTION = NamedConnective{:∧}()
+const ∧ = CONJUNCTION
+arity(::typeof(∧)) = 2See also NEGATION, CONJUNCTION, DISJUNCTION, IMPLICATION, Connective.
SoleLogics.collatetruth — Methodcollatetruth(c::Connective, ts::NTuple{N,T where T<:Truth})::Truth where {N}Return the truth value for a composed formula c(t1, ..., tN), given the N with t1, ..., tN being Truth values.
See also simplify, Connective, Truth.
SoleLogics.simplify — Methodsimplify(c::Connective, ts::NTuple{N,F where F<:Formula})::Truth where {N}Return a formula with the same semantics of a composed formula c(φ1, ..., φN), given the N immediate sub-formulas.
See also collatetruth, Connective, Formula.
Propositional boolean logic
SoleLogics.NEGATION — Constantconst NEGATION = NamedConnective{:¬}()
+const ¬ = NEGATION
+arity(::typeof(¬)) = 1Logical negation (also referred to as complement). It can be typed by \neg<tab>.
See also NamedConnective, Connective.
SoleLogics.CONJUNCTION — Constantconst CONJUNCTION = NamedConnective{:∧}()
+const ∧ = CONJUNCTION
+arity(::typeof(∧)) = 2Logical conjunction. It can be typed by \wedge<tab>.
See also NamedConnective, Connective.
SoleLogics.DISJUNCTION — Constantconst DISJUNCTION = NamedConnective{:∨}()
+const ∨ = DISJUNCTION
+arity(::typeof(∨)) = 2Logical disjunction. It can be typed by \vee<tab>.
See also NamedConnective, Connective.
SoleLogics.IMPLICATION — Constantconst IMPLICATION = NamedConnective{:→}()
+const → = IMPLICATION
+arity(::typeof(→)) = 2Logical implication. It can be typed by \to<tab>.
See also NamedConnective, Connective.
Boolean logic Connectives are regrouped in a single collection.
SoleLogics.BASE_CONNECTIVES — Constantconst BASE_CONNECTIVES = [¬, ∧, ∨, →]Basic logical operators.
See also NEGATION, CONJUNCTION, DISJUNCTION, IMPLICATION, Connective.
SoleLogics.BooleanTruth — Typestruct BooleanTruth <: Truth
+ flag::Bool
+endStructure for representing the Boolean truth values ⊤ and ⊥. It wraps a flag which takes value true for ⊤ (TOP), and false for ⊥ (BOT)
See also BooleanAlgebra.
SoleLogics.BooleanAlgebra — Typestruct BooleanAlgebra <: AbstractAlgebra{Bool} endA Boolean algebra, defined on the values TOP (representing truth) and BOT (for bottom, representing falsehood). For this algebra, the basic operators negation, conjunction and disjunction (stylized as ¬, ∧, ∨) can be defined as the complement, minimum and maximum, of the integer cast of true and false, respectively.
See also Truth.
SoleLogics.BaseLogic — Typestruct BaseLogic{G<:AbstractGrammar,A<:AbstractAlgebra} <: AbstractLogic{G,A}
+ grammar::G
+ algebra::A
+endA basic logic based on a grammar and an algebra, where both the grammar and the algebra are instantiated.
See also grammar, algebra, AbstractGrammar, AbstractAlgebra, AbstractLogic.
A method is provided to simply access a propositional logic.
SoleLogics.propositionallogic — Methodpropositionallogic(;
+ alphabet = AlphabetOfAny{String}(),
+ operators = NamedConnective[¬, ∧, ∨, →],
+ grammar = CompleteFlatGrammar(AlphabetOfAny{String}(), NamedConnective[¬, ∧, ∨, →]),
+ algebra = BooleanAlgebra()
+)Instantiate a propositional logic given a grammar and an algebra. Alternatively, an alphabet and a set of operators can be specified instead of the grammar.
Examples
julia> (¬) isa operatorstype(propositionallogic())
+true
+
+julia> (¬) isa operatorstype(propositionallogic(; operators = [∨]))
+false
+
+julia> propositionallogic(; alphabet = ["p", "q"]);
+
+julia> propositionallogic(; alphabet = ExplicitAlphabet([Atom("p"), Atom("q")]));
+See also modallogic, AbstractAlphabet, AbstractAlgebra, AlphabetOfAny, [CompleteFlatGrammar], BooleanAlgebra, BASE_PROPOSITIONAL_CONNECTIVES.
Interpretations
Interpretations are nothing but dictionaries working with Truth values, or other types that can be ultimately converted to Truth.
SoleLogics.AbstractAssignment — Typeabstract type AbstractAssignment <: AbstractInterpretation endAbstract type for assigments, that is, interpretations of propositional logic, encoding mappings from AbstractAtoms to Truth values.
Interface
Base.haskey(i::AbstractAssignment, ::AbstractAtom)::Boolinlinedisplay(i::AbstractAssignment)::Stringinterpret(a::AbstractAtom, i::AbstractAssignment, args...; kwargs...)::SyntaxLeaf
See also AbstractAssignment, AbstractAtom, AbstractInterpretation.
Base.haskey — MethodBase.haskey(i::AbstractAssignment, ::AbstractAtom)::BoolReturn whether an AbstractAssignment has a truth value for a given Atom. If any object is passed, it is wrapped in an Atom and then checked.
Examples
julia> haskey(TruthDict(["a" => true, "b" => false, "c" => true]), Atom("a"))
+true
+
+julia> haskey(TruthDict(1:4, false), Atom(3))
+trueSee also AbstractAssignment, AbstractInterpretation, AbstractAtom, TruthDict, Atom.
SoleLogics.TruthDict — Typestruct TruthDict{D<:AbstractDict{A where A<:Atom,T where T<:Truth}} <: AbstractAssignment
+ truth::D
+endA logical interpretation instantiated as a dictionary, explicitly assigning truth values to a finite set of atoms.
Examples
julia> TruthDict(1:4)
+TruthDict with values:
+┌────────┬────────┬────────┬────────┐
+│ 4 │ 2 │ 3 │ 1 │
+│ Int64 │ Int64 │ Int64 │ Int64 │
+├────────┼────────┼────────┼────────┤
+│ ⊤ │ ⊤ │ ⊤ │ ⊤ │
+└────────┴────────┴────────┴────────┘
+
+
+julia> t1 = TruthDict(1:4, false); t1[5] = true; t1
+TruthDict with values:
+┌───────┬───────┬───────┬───────┬───────┐
+│ 5 │ 4 │ 2 │ 3 │ 1 │
+│ Int64 │ Int64 │ Int64 │ Int64 │ Int64 │
+├───────┼───────┼───────┼───────┼───────┤
+│ ⊤ │ ⊥ │ ⊥ │ ⊥ │ ⊥ │
+└───────┴───────┴───────┴───────┴───────┘
+
+julia> t2 = TruthDict(["a" => true, "b" => false, "c" => true])
+TruthDict with values:
+┌────────┬────────┬────────┐
+│ c │ b │ a │
+│ String │ String │ String │
+├────────┼────────┼────────┤
+│ ⊤ │ ⊥ │ ⊤ │
+└────────┴────────┴────────┘
+
+julia> check(parseformula("a ∨ b"), t2)
+true
+If prompted for the value of an unknown atom, this throws an error. If boolean, integer, or float values are specified, they are converted to Truth values. If the structure is initialized as empty, BooleanTruth values are assumed.
See also AbstractAssignment, AbstractInterpretation, DefaultedTruthDict, BooleanTruth.
SoleLogics.DefaultedTruthDict — Typestruct DefaultedTruthDict{
+ D<:AbstractDict{A where A<:Atom,T where T<:Truth},
+ T<:Truth
+} <: AbstractAssignment
+ truth::D
+ default_truth::T
+endA truth table instantiated as a dictionary, plus a default value. This structure assigns truth values to a set of atoms and, when prompted for the value of an atom that is not in the dictionary, it returns default_truth.
Implementation
If you use interpret function and you pass a DefaultedTruthDict as AbstractAssignment and the Atom is not present in the dictionary, then the default dictionary value will be returned and not the Atom itself.
Here is an example of this.
julia> interpret(Atom(5), DefaultedTruthDict(string.(1:4), false))
+⊥Examples
julia> t1 = DefaultedTruthDict(string.(1:4), false); t1["5"] = false; t1
+DefaultedTruthDict with default truth `⊥` and values:
+┌────────┬────────┬────────┬────────┬────────┐
+│ 4 │ 1 │ 5 │ 2 │ 3 │
+│ String │ String │ String │ String │ String │
+├────────┼────────┼────────┼────────┼────────┤
+│ ⊤ │ ⊤ │ ⊥ │ ⊤ │ ⊤ │
+└────────┴────────┴────────┴────────┴────────┘
+
+julia> check(parseformula("1 ∨ 2"), t1)
+true
+
+julia> check(parseformula("1 ∧ 5"), t1)
+false
+See also AbstractAssignment, AbstractInterpretation, interpret, Atom, TruthDict, DefaultedTruthDict.
To associate interpretations with their assignment, we can simply build a truth table.
SoleLogics.TruthTable — Typestruct TruthTable{A,T<:Truth}Dictionary which associates an AbstractAssignments to the truth value of the assignment itself on a SyntaxStructure.
See also AbstractAssignment, SyntaxStructure, Truth.
AbstractInterpretationSet
+
+LogicalInstance{S<:AbstractInterpretationSet}
+
+check(φ::Formula, s::AbstractInterpretationSet, i_instance::Integer, args...; kwargs...)
+check(φ::Formula, s::AbstractInterpretationSet, args...; kwargs...)
+
+InterpretationVector{M<:AbstractInterpretation}
