SoleLogics.jl – Computational logic in Julia

<!-- --> <!-- -->

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.

Usage

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

Parsing and manipulating Formulas

```julia julia> φ1 = parseformula("¬p∧q∧(¬s∧¬z)");

julia> φ1 isa SyntaxTree true

julia> syntaxstring(φ1) "¬p ∧ q ∧ ¬s ∧ ¬z"

julia> φ2 = ⊥ ∨ Atom("t") → φ1;

julia> φ2 isa SyntaxTree true

julia> syntaxstring(φ2) "(⊥ ∨ t) → (¬p ∧ q ∧ ¬s ∧ ¬z)" ```

Generating random formulas

```julia julia> using Random

julia> height = 2

julia> alphabet = Atom.(["p", "q"])

Propositional case

julia> SoleLogics.BASEPROPOSITIONALCONNECTIVES 6-element Vector{SoleLogics.Connective}: ¬ ∧ ∨ →

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

Modal case

julia> SoleLogics.BASEMODALCONNECTIVES 8-element Vector{SoleLogics.Connective}: ¬ ∧ ∨ → ◊ □

julia> randformula(Random.MersenneTwister(14), height, alphabet, SoleLogics.BASEMODALCONNECTIVES) SyntaxBranch: ¬□p ```

Model checking

Propositional logic

```julia

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

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

julia> check(phi, I) true

```

Modal logic K (Saul Kripke, see an introduction here)

```julia julia> using Graphs

Instantiate a Kripke frame with 5 worlds and 5 edges

julia> worlds = SoleLogics.World.(1:5);

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

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

Enumerate the world that are accessible from the first world

julia> accessibles(fr, first(worlds)) 2-element Vector{SoleLogics.World{Int64}}: SoleLogics.World{Int64}(2) SoleLogics.World{Int64}(3)

julia> p,q = Atom.(["p", "q"])

# Assign each world a propositional interpretation julia> 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]), ])

Instantiate a Kripke structure by combining a Kripke frame and the propositional interpretations over each world

julia> K = KripkeStructure(fr, valuation)

Generate a modal formula

julia> modphi = parseformula("◊(p ∧ q)")

Check the just generated formula on each world of the Kripke structure

julia> [w => check(modphi, K, w) for w in worlds] 5-element Vector{Pair{SoleLogics.World{Int64}, Bool}}: SoleLogics.World{Int64}(1) => 1 SoleLogics.World{Int64}(2) => 0 SoleLogics.World{Int64}(3) => 0 SoleLogics.World{Int64}(4) => 0 SoleLogics.World{Int64}(5) => 0 ```

Temporal modal logics

```julia

A temporal frame of 10 (equidistant) points

julia> fr = SoleLogics.FullDimensionalFrame((10,), SoleLogics.Point{1,Int});

Linear Temporal Logic (LTL) successor relation

julia> accessibles(fr, SoleLogics.Point(3), SoleLogics.SuccessorRel) |> collect 1-element Vector{SoleLogics.Point{1, Int64}}: ❮4❯

Linear Temporal Logic (LTL) greater than relation

julia> accessibles(fr, SoleLogics.Point(3), SoleLogics.GreaterRel) |> collect 7-element Vector{SoleLogics.Point{1, Int64}}: ❮4❯ ❮5❯ ❮6❯ ❮7❯ ❮8❯ ❮9❯ ❮10❯

```

```julia

An interval temporal frame on 10 (equidistant) points

julia> fr = SoleLogics.FullDimensionalFrame(10, Interval{Int});

Interval Algebra (IA) relation L (later, see Halpern & Shoham, 1991)

julia> 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)

Region Connection Calculus relation DC (disconnected, see Cohn et al., 1997)

julia> 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