<div align="center"><a href="https://github.com/aclai-lab/Sole.jl"><img src="logo_transparent.png" alt="" title="This package is part of Sole.jl" width="200"></a></div>

SoleLogics.jl – Computational logic in Julia

<!-- [](https://github.com/invenia/BlueStyle) -->

In a nutshell

SoleLogics.jl provides a fresh codebase for computational logic, featuring easy manipulation of:

• Propositional and (multi)modal logics (atoms, logical constants, alphabets, grammars, crisp/fuzzy algebras);
• Logical formulas (parsing, random generation, minimization);
• Logical interpretations (e.g., propositional valuations, Kripke structures);
• Algorithms for finite model checking, that is, checking that a formula is satisfied by an interpretation.

<!-- However, it can be used for other purposes by computational logicians. -->

Usage

using Pkg; Pkg.add("SoleLogics")
using SoleLogics

Parsing and manipulating Formulas

julia> φ1 = parseformula("¬p∧q∨(s∨z)")
SyntaxBranch: (¬p ∧ q) ∨ s ∨ z

julia> syntaxstring(φ1; parenthesize_commutatives = true)
"(¬p ∧ q) ∨ (s ∨ z)"

julia> filter(ψ -> height(ψ) == 1, subformulas(φ1))
2-element Vector{SyntaxTree}:
 SyntaxBranch: ¬p
 SyntaxBranch: s ∨ z

julia> filter(ψ -> natoms(ψ) == 1, subformulas(φ1))
5-element Vector{SyntaxTree}:
 Atom{String}: p
 Atom{String}: q
 Atom{String}: s
 Atom{String}: z
 SyntaxBranch: ¬p

julia> φ2 = ⊥ ∨ Atom("t") → φ1
SyntaxBranch: ⊥ ∨ t → (¬p ∧ q) ∨ s ∨ z

Generating random formulas

julia> using Random

julia> height = 2;

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

julia> # A propositional formula
       SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES
4-element Vector{NamedConnective}:
 ¬
 ∧
 ∨
 →

julia> randformula(Random.MersenneTwister(507), height, alphabet, SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES)
SyntaxBranch: p → q ∧ q

julia> # A modal formula
       SoleLogics.BASE_MODAL_CONNECTIVES
6-element Vector{NamedConnective}:
 ¬
 ∧
 ∨
 →
 ◊
 □

julia> randformula(Random.MersenneTwister(4267), height, alphabet, SoleLogics.BASE_MODAL_CONNECTIVES)
SyntaxBranch: ◊□p

Model checking

Propositional logic

julia> φ1 = parseformula("¬(p ∧ q)")
SyntaxBranch: ¬(p ∧ q)

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

julia> check(φ1, I)
⊤

julia> φ2 = parseformula("¬(p ∧ q) ∧ (r ∨ q)")
SyntaxBranch: ¬(p ∧ q)

julia> interpret(φ2, I)
Atom{String}: r

Modal logic K

See an introduction to modal logic K here.

julia> using Graphs

julia> # Instantiate a Kripke frame with 5 worlds and 5 edges
       worlds = World.(1:5);

julia> edges = Edge.([(1,2), (1,3), (2,4), (3,4), (3,5)]);

julia> fr = SimpleModalFrame(worlds, Graphs.SimpleDiGraph(edges))
SimpleModalFrame{World{Int64}, SimpleDiGraph{Int64}} with 5 worlds:
- worlds: [1, 2, 3, 4, 5]
- accessibles:
        1 -> [2, 3]
        2 -> [4]
        3 -> [4, 5]
        4 -> []
        5 -> []

julia> # Enumerate the world that are accessible from the first world
       accessibles(fr, first(worlds))
2-element Vector{World{Int64}}:
 World{Int64}(2)
 World{Int64}(3)

julia> @atoms p q

julia> # Assign each world a propositional interpretation
       valuation = Dict([
	        worlds[1] => TruthDict([p => true, q => false]),
	        worlds[2] => TruthDict([p => true, q => true]),
	        worlds[3] => TruthDict([p => true, q => false]),
	        worlds[4] => TruthDict([p => false, q => false]),
	        worlds[5] => TruthDict([p => false, q => true]),
	     ]);

julia> # Instantiate a Kripke structure by combining a Kripke frame and the propositional interpretations over each world
       K = KripkeStructure(fr, valuation);

julia> # Generate a modal formula
       φ = parseformula("◊(p ∧ q)");

julia> # Check the just generated formula on each world of the Kripke structure
       [w => check(φ, K, w) for w in worlds]
5-element Vector{Pair{World{Int64}, Bool}}:
 World{Int64}(1) => 1
 World{Int64}(2) => 0
 World{Int64}(3) => 0
 World{Int64}(4) => 0
 World{Int64}(5) => 0

Temporal modal logics

julia> # A frame consisting of 10 (evenly spaced) points
       fr = FullDimensionalFrame((10,), Point{1, Int64});

julia> # Linear Temporal Logic (LTL) `successor` relation
       accessibles(fr, Point(3), SoleLogics.SuccessorRel) |> collect
1-element Vector{Point{1, Int64}}:
 ❮4❯

julia> # Linear Temporal Logic (LTL) `greater than` relation
       accessibles(fr, Point(3), SoleLogics.GreaterRel) |> collect
7-element Vector{Point{1, Int64}}:
 ❮4❯
 ❮5❯
 ❮6❯
 ❮7❯
 ❮8❯
 ❮9❯
 ❮10❯

julia> # An interval frame consisting of all intervals over 10 (evenly spaced) points
       fr = FullDimensionalFrame((10, ), Interval{Int64});

julia> # Interval Algebra (IA) relation `L` (later, see [Halpern & Shoham, 1991](https://dl.acm.org/doi/abs/10.1145/115234.115351))
       accessibles(fr, Interval(3, 5), IA_L) |> collect
15-element Vector{Interval{Int64}}:
 Interval{Int64}(6, 7)
 Interval{Int64}(6, 8)
 Interval{Int64}(7, 8)
 Interval{Int64}(6, 9)
 Interval{Int64}(7, 9)
 Interval{Int64}(8, 9)
 Interval{Int64}(6, 10)
 Interval{Int64}(7, 10)
 Interval{Int64}(8, 10)
 Interval{Int64}(9, 10)
 Interval{Int64}(6, 11)
 Interval{Int64}(7, 11)
 Interval{Int64}(8, 11)
 Interval{Int64}(9, 11)
 Interval{Int64}(10, 11)

julia> # Region Connection Calculus relation `DC` (disconnected, see [Cohn et al., 1997](https://link.springer.com/article/10.1023/A:1009712514511))
       accessibles(fr, Interval(3, 5), Topo_DC) |> collect
 16-element Vector{Interval{Int64}}:
 Interval{Int64}(6, 7)
 Interval{Int64}(6, 8)
 Interval{Int64}(7, 8)
 Interval{Int64}(6, 9)
 Interval{Int64}(7, 9)
 Interval{Int64}(8, 9)
 Interval{Int64}(6, 10)
 Interval{Int64}(7, 10)
 Interval{Int64}(8, 10)
 Interval{Int64}(9, 10)
 Interval{Int64}(6, 11)
 Interval{Int64}(7, 11)
 Interval{Int64}(8, 11)
 Interval{Int64}(9, 11)
 Interval{Int64}(10, 11)
 Interval{Int64}(1, 2)

About

SoleLogics.jl lays the logical foundations for Sole.jl, an open-source framework for symbolic machine learning, originally designed for machine learning based on modal logics (see Eduard I. Stan's PhD thesis 'Foundations of Modal Symbolic Learning' here).

The package is developed by the ACLAI Lab @ University of Ferrara.

Thanks to Jakob Peters (author of PAndQ.jl) for the interesting discussions and ideas.

Want to contribute?

We have some TODOs

More on Sole

• SoleData.jl
• SoleFeatures.jl
• SoleModels.jl
• SolePostHoc.jl

Similar Julia Packages for Computational Logic

• PAndQ.jl
• Julog.jl
• LogicCircuits.jl
• FirstOrderLogic.jl