Getting started

In this introductory section you will learn about the main building blocks of SoleLogics. Their definition, usage examples and how to customize them to your own needs.

In short, you can consider this package as divided into two halves.:

the syntactical half, which defines structures to represent logical constructs such as assertions, logical constants, alphabets, grammars, crisp and fuzzy algebras, formulas etc. A consistent part of SoleLogics is devoted to randomly generate such structures, as well as parse and minimize formulas;
the semantic half, which defines rules to apply when interpreting a logical formulas. The "semantic heart" of SoleLogics is its finite model checking algorithm, whose purpose is to efficiently check whether a formula is satisfied by an interpretation or not.

Please, feel free to use the following tree structures to orient yourself in the reading of this section. More pieces will be added to this type-hierarchy tree in the following sections.

Type hierarchy

Syntactical
- Connective (e.g., ∧, ∨, ¬, →)
- Formula
  - SyntaxStructure
    - SyntaxTree (e.g., ¬p ∧ q → s)
      - SyntaxLeaf
        Atom (e.g., p, q)
        Truth (e.g., ⊤, ⊥)
      - SyntaxBranch (e.g., p ∧ q)
AbstractInterpretation (e.g., p is ⊤, equivalent to p is true in boolean logic)

Also, two union types are defined:

Operator, that is, Union{Connective,Truth},
SyntaxToken, that is, Union{Atom,Connective}.

Syntax Basics

SoleLogics.Syntactical — Type

abstract type Syntactical end

Master abstract type for all syntactical objects (e.g., formulas, connectives).

Interface

syntaxstring(s::Syntactical; kwargs...)::String

See also Formula, Connective.

source

To print out a generic Syntactical element, we must define how it is converted into a string. To do this, we can implement a custom syntaxstring.

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)
"∧(∧(∧(∧(p, q), r), s), t)"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), remove_redundant_parentheses=false)
"((((p) ∧ (q)) ∧ (r)) ∧ (s)) ∧ (t)"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), remove_redundant_parentheses=true, parenthesize_atoms=true)
"(p) ∧ (q) ∧ (r) ∧ (s) ∧ (t)"

julia> syntaxstring(parseformula("◊((p∧s)→q)"))
"◊((p ∧ s) → q)"

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

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 the kwargs... part!) 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 SyntaxTrees, 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 (',').

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, NEGATION and IMPLICATION (stylized as ∧, ∨, ¬ and →).

Interface

arity(::Connective)::Int
iscommutative(::Connective)::Bool
precedence(::Connective)::Int
associativity(::Connective)::Symbol
collatetruth(::Connective, ::NTuple{N,Truth})::Truth
simplify(::Connective, ::NTuple{N,SyntaxTree})::SyntaxTree
dual(s::Connective)::Connective
hasdual(s::Connective)::Bool
See also Syntactical

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

The semantics of a propositional connective can be specified via collatetruth (see example below); in principle, the definition can rely on the partial order between truth values (specified via precedes).

Here is an example of a custom implementation of the xor (⊻) Boolean operator.

import SoleLogics: arity, iscommutative, collatetruth
const ⊻ = SoleLogics.NamedConnective{:⊻}()
SoleLogics.arity(::typeof(⊻)) = 2
SoleLogics.iscommutative(::typeof(⊻)) = true
SoleLogics.collatetruth(::typeof(⊻), (t1, t2)::NTuple{N,T where T<:BooleanTruth}) where {N} = (count(istop, (t1, t2)) == 1)

Note that collatetruth must be defined at least for some truth value types T via methods accepting an NTuple{arity,T} as a second argument.

To make the operator work with incomplete interpretations (e.g., when the Truth value for an atom is not known), simplification rules for NTuple{arity,T where T<:Formula}s should be provided via methods for simplify. For example, these rules suffice for simplifying xors between TOP/BOT`s, and other formulas:

import SoleLogics: simplify
simplify(::typeof(⊻), (t1, t2)::Tuple{BooleanTruth,BooleanTruth}) = istop(t1) == istop(t2) ? BOT : TOP
simplify(::typeof(⊻), (t1, t2)::Tuple{BooleanTruth,Formula}) = istop(t1) ? ¬t2 : t2
simplify(::typeof(⊻), (t1, t2)::Tuple{Formula,BooleanTruth}) = istop(t2) ? ¬t1 : t1

Beware of dispatch ambiguities!

source

If the definition above overwhelms you, don't worry: it will be clearer later. For now we are simply interested in understanding that Connectives are simply symbols used to concatenate other logical constructs with each other.

Later, we will see some interesting example about how to equip these symbols with semantics, that is, what rules should be applied when interpreting connectives in a generic Formula. We will also understand how to define our own custom connectives.

SoleLogics.arity — Method

arity(φ::SyntaxTree)::Integer
arity(tok::Connective)::Integer

Return the arity of a Connective or a SyntaxTree. The arity is an integer representing the number of allowed children for a node in a tree. Connectives with arity equal to 0, 1 or 2 are called nullary, unary and binary, respectively. SyntaxLeafs (Atoms and Truth values) are always nullary.

source

The vast majority of data structures involved in encoding a logical formula, are children of the Formula abstract type. When such data structures purely represents tree-shaped data structures (or single nodes in them), then they are also children of the SyntaxStructure abstract type.

SoleLogics.Formula — Type

abstract type Formula <: Syntactical end

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

Interface

tree(φ::Formula)::SyntaxTree
composeformulas(c::Connective, φs::NTuple{N,F})::F where {N,F<:Formula}
See also Syntactical

Utility functions (requiring a walk of the tree)

Base.in(tok::SyntaxToken, φ::Formula)::Bool
height(φ::Formula)::Int
tokens(φ::Formula)::AbstractVector{<:SyntaxToken}
atoms(φ::Formula)::AbstractVector{<:AbstractAtom}
truths(φ::Formula)::AbstractVector{<:Truth}
leaves(φ::Formula)::AbstractVector{<:SyntaxLeaf}
connectives(φ::Formula)::AbstractVector{<:Connective}
operators(φ::Formula)::AbstractVector{<:Operator}
ntokens(φ::Formula)::Int
natoms(φ::Formula)::Int
ntruths(φ::Formula)::Int
nleaves(φ::Formula)::Int
nconnectives(φ::Formula)::Int
noperators(φ::Formula)::Int

source

The following methods define Formula interface.

SoleLogics.tree — Method

tree(φ::Formula)::SyntaxTree

Return the SyntaxTree representation of a formula; note that this is equivalent to Base.convert(SyntaxTree, φ).

Semantics Basics

SoleLogics.AbstractInterpretation — Type

abstract type AbstractInterpretation end

Abstract type for representing a logical interpretation. In the case of propositional logic, is essentially a map atom → truth value.

Properties expressed via logical formulas can be checked on logical interpretations.

Interface

valuetype(i::AbstractInterpretation)
truthtype(i::AbstractInterpretation)
interpret(φ::Formula, i::AbstractInterpretation, args...; kwargs...)::Formula

Utility functions

check(φ::Formula, i::AbstractInterpretation, args...; kwargs...)::Bool

source

SoleLogics.interpret — Method

interpret(
    φ::Formula,
    i::AbstractInterpretation,
    args...;
    kwargs...
)::Formula

Return the truth value for a formula on a logical interpretation (or model).

Examples

julia> @atoms p q
2-element Vector{Atom{String}}:
 p
 q

julia> td = TruthDict([p => true, q => false])
TruthDict with values:
┌────────┬────────┐
│      q │      p │
│ String │ String │
├────────┼────────┤
│      ⊥ │      ⊤ │
└────────┴────────┘

julia> interpret(CONJUNCTION(p,q), td)
⊥

source

SoleLogics.check — Method

check(
    φ::Formula,
    i::AbstractInterpretation,
    args...;
    kwargs...
)::Bool

Check a formula on a logical interpretation (or model), returning true if the truth value for the formula istop. This process is referred to as (finite) model checking, and there are many algorithms for it, typically depending on the complexity of the logic.

Examples

julia> @atoms String p q
2-element Vector{Atom{String}}:
 Atom{String}("p")
 Atom{String}("q")

julia> td = TruthDict([p => TOP, q => BOT])
TruthDict with values:
┌────────┬────────┐
│      q │      p │
│ String │ String │
├────────┼────────┤
│      ⊥ │      ⊤ │
└────────┴────────┘

julia> check(CONJUNCTION(p,q), td)
false

source