Merge branch 'main' into dev

Author: PasoStudio73

.cirrus.yml

@@ -1,5 +1,5 @@
 freebsd_instance:
-  image_family: freebsd-14-1
+  image_family: freebsd-14-2
 task:
   name: FreeBSD
   artifacts_cache:

Project.toml

@@ -1,7 +1,7 @@
 name = "SoleLogics"
 uuid = "b002da8f-3cb3-4d91-bbe3-2953433912b5"
-authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Edoardo PONSANESI", "Alberto PAPARELLA", "Eduard I. STAN"]
-version = "0.12.0"
+authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Alberto PAPARELLA", "Edoardo PONSANESI", "Eduard I. STAN"]
+version = "0.13.0"
 
 [deps]
 AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"

benchmarks/alphacheck.jl

@@ -115,6 +115,8 @@ include("types/modal-logic.jl")
 
 include("utils/modal-logic.jl")
 
+include("utils/multi-modal-logic.jl")
+
 export WorldFilter
 export FunctionalWorldFilter, FilteredRelation
 export IntervalLengthFilter

src/SoleLogics.jl

@@ -2,13 +2,16 @@ module ManyValuedLogics
 
 using ..SoleLogics
 
+export FiniteTruth
+
+include("finitetruth.jl")
+
 export BinaryOperation
 
 include("operations.jl")
 
 include("axioms.jl")
 
-export FiniteTruth
 export Monoid, CommutativeMonoid
 export FiniteLattice, FiniteBoundedLattice, FiniteResiduatedLattice
 export FiniteFLewAlgebra, FiniteHeytingAlgebra
@@ -26,8 +29,6 @@ include("many-valued-formulas.jl")
 
 include("algebras/algebras.jl")
 
-include("finite-index-algebras.jl")
-
 export alphacheck
 
 include("check.jl")

src/many-valued-logics/ManyValuedLogics.jl

@@ -1,17 +1,22 @@
-d2 = Vector{BooleanTruth}([⊥, ⊤])
+# Domain ⊤, ⊥
+t, b = FiniteTruth.([1:2]...)
 
-jt2 = Dict{Tuple{BooleanTruth, BooleanTruth}, BooleanTruth}(
-    (⊥, ⊥) => ⊥, (⊥, ⊤) => ⊤,
-    (⊤, ⊥) => ⊤, (⊤, ⊤) => ⊤
-)
+# α ∨ β = max{α, β}
+jointruthtable = [
+#   ⊤  ⊥
+    t, t,   # ⊤
+    t, b    # ⊥
+]
 
-mt2 = Dict{Tuple{BooleanTruth, BooleanTruth}, BooleanTruth}(
-    (⊥, ⊥) => ⊥, (⊥, ⊤) => ⊥,
-    (⊤, ⊥) => ⊥, (⊤, ⊤) => ⊤
-)
+# α ∧ β = min{α, β}
+meettruthtable = [
+#   ⊤  ⊥
+    t, b,   # ⊤
+    b, b    # ⊥
+]
 
-j2 = BinaryOperation(d2, jt2)
+join = BinaryOperation{2}(jointruthtable)
+meet = BinaryOperation{2}(meettruthtable)
+# In booleanalgebra, the t-norm ⋅ is ∧
 
-m2 = BinaryOperation(d2, mt2)
-
-booleanalgebra = FiniteFLewAlgebra(j2, m2, m2, ⊥, ⊤)
+booleanalgebra = FiniteFLewAlgebra{2}(join, meet, meet, b, t)

src/many-valued-logics/algebras/booleanalgebra.jl

@@ -1,22 +1,24 @@
-α = FiniteTruth("α")
+# Domain ⊤, ⊥, α
+t, b, α = FiniteTruth.([1:3]...)
 
-d3 = Vector{FiniteTruth}([⊥, α, ⊤])
+# α ∨ β = max{α, β}
+jointruthtable = [
+#   ⊤  ⊥  α
+    t, t, t,    # ⊤
+    t, b, α,    # ⊥
+    t, α, α     # α
+]
 
-# a ∨ b = max{a, b}
-jointable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => α, (⊥, ⊤) => ⊤,
-    (α, ⊥) => α, (α, α) => α, (α, ⊤) => ⊤,
-    (⊤, ⊥) => ⊤, (⊤, α) => ⊤, (⊤, ⊤) => ⊤
-)
+# α ∧ β = min{α, β}
+meettruthtable = [
+#   ⊤  ⊥  α
+    t, b, α,    # ⊤
+    b, b, b,    # ⊥
+    α, b, α     # α
+]
 
-# a ∧ b = min{a, b}
-meettable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => ⊥, (⊥, ⊤) => ⊥,
-    (α, ⊥) => ⊥, (α, α) => α, (α, ⊤) => α,
-    (⊤, ⊥) => ⊥, (⊤, α) => α, (⊤, ⊤) => ⊤
-)
+join = BinaryOperation{3}(jointruthtable)
+meet = BinaryOperation{3}(meettruthtable)
+# In G3, the t-norm ⋅ is ∧
 
-join = BinaryOperation(d3, jointable)
-meet = BinaryOperation(d3, meettable)
-
-G3 = FiniteFLewAlgebra(join, meet, meet, ⊥, ⊤)
+G3 = FiniteFLewAlgebra{3}(join, meet, meet, b, t)

src/many-valued-logics/algebras/g3.jl

@@ -1,25 +1,26 @@
-α = FiniteTruth("α")
-β = FiniteTruth("β")
+# Domain ⊤, ⊥, α, β
+t, b, α, β = FiniteTruth.([1:4]...)
 
-d4 = Vector{FiniteTruth}([⊥, α, β, ⊤])
+# α ∨ β = max{α, β}
+jointruthtable = [
+#   ⊤  ⊥  α  β
+    t, t, t, t, # ⊤
+    t, b, α, β, # ⊥
+    t, α, α, β, # α
+    t, β, β, β  # β
+]
 
-# a ∨ b = max{a, b}
-jointable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => α, (⊥, β) => β, (⊥, ⊤) => ⊤,
-    (α, ⊥) => α, (α, α) => α, (α, β) => β, (α, ⊤) => ⊤,
-    (β, ⊥) => β, (β, α) => β, (β, β) => β, (β, ⊤) => ⊤,
-    (⊤, ⊥) => ⊤, (⊤, α) => ⊤, (⊤, β) => ⊤, (⊤, ⊤) => ⊤
-)
+# α ∧ β = min{α, β}
+meettruthtable = [
+#   ⊤  ⊥  α  β
+    t, b, α, β, # ⊤
+    b, b, b, b, # ⊥
+    α, b, α, α, # α
+    β, b, α, β  # β
+]
 
-# a ∧ b = min{a, b}
-meettable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => ⊥, (⊥, β) => ⊥, (⊥, ⊤) => ⊥,
-    (α, ⊥) => ⊥, (α, α) => α, (α, β) => α, (α, ⊤) => α,
-    (β, ⊥) => ⊥, (β, α) => α, (β, β) => β, (β, ⊤) => β,
-    (⊤, ⊥) => ⊥, (⊤, α) => α, (⊤, β) => β, (⊤, ⊤) => ⊤
-)
+join = BinaryOperation{4}(jointruthtable)
+meet = BinaryOperation{4}(meettruthtable)
+# In G4, the t-norm ⋅ is ∧
 
-join = BinaryOperation(d4, jointable)
-meet = BinaryOperation(d4, meettable)
-
-G4 = FiniteFLewAlgebra(join, meet, meet, ⊥, ⊤)
+G4 = FiniteFLewAlgebra{4}(join, meet, meet, b, t)

src/many-valued-logics/algebras/g4.jl

@@ -1,28 +1,28 @@
-α = FiniteTruth("α")
-β = FiniteTruth("β")
-γ = FiniteTruth("γ")
+# Domain ⊤, ⊥, α, β, γ
+t, b, α, β, γ = FiniteTruth.([1:5]...)
 
-d5 = Vector{FiniteTruth}([⊥, α, β, γ, ⊤])
+# α ∨ β = max{α, β}
+jointruthtable = [
+#   ⊤  ⊥  α  β  γ
+    t, t, t, t, t,  # ⊤
+    t, b, α, β, γ,  # ⊥
+    t, α, α, β, γ,  # α
+    t, β, β, β, γ,  # β
+    t, γ, γ, γ, γ   # γ
+]
 
-# a ∨ b = max{a, b}
-jointable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => α, (⊥, β) => β, (⊥, γ) => γ, (⊥, ⊤) => ⊤,
-    (α, ⊥) => α, (α, α) => α, (α, β) => β, (α, γ) => γ, (α, ⊤) => ⊤,
-    (β, ⊥) => β, (β, α) => β, (β, β) => β, (β, γ) => γ, (β, ⊤) => ⊤,
-    (γ, ⊥) => γ, (γ, α) => γ, (γ, β) => γ, (γ, γ) => γ, (γ, ⊤) => ⊤,
-    (⊤, ⊥) => ⊤, (⊤, α) => ⊤, (⊤, β) => ⊤, (⊤, γ) => ⊤, (⊤, ⊤) => ⊤
-)
+# α ∧ β = min{α, β}
+meettruthtable = [
+#   ⊤  ⊥  α  β
+    t, b, α, β, γ,  # ⊤
+    b, b, b, b, b,  # ⊥
+    α, b, α, α, α,  # α
+    β, b, α, β, β,  # β
+    γ, b, α, β, γ   # γ  
+]
 
-# a ∧ b = min{a, b}
-meettable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => ⊥, (⊥, β) => ⊥, (⊥, γ) => ⊥, (⊥, ⊤) => ⊥,
-    (α, ⊥) => ⊥, (α, α) => α, (α, β) => α, (α, γ) => α, (α, ⊤) => α,
-    (β, ⊥) => ⊥, (β, α) => α, (β, β) => β, (β, γ) => β, (β, ⊤) => β,
-    (γ, ⊥) => ⊥, (γ, α) => α, (γ, β) => β, (γ, γ) => γ, (γ, ⊤) => γ,
-    (⊤, ⊥) => ⊥, (⊤, α) => α, (⊤, β) => β, (⊤, γ) => γ, (⊤, ⊤) => ⊤
-)
+join = BinaryOperation{5}(jointruthtable)
+meet = BinaryOperation{5}(meettruthtable)
+# In G5, the t-norm ⋅ is ∧
 
-join = BinaryOperation(d5, jointable)
-meet = BinaryOperation(d5, meettable)
-
-G5 = FiniteFLewAlgebra(join, meet, meet, ⊥, ⊤)
+G5 = FiniteFLewAlgebra{5}(join, meet, meet, b, t)

src/many-valued-logics/algebras/g5.jl

@@ -1,23 +1,26 @@
-α = FiniteTruth("α")
-β = FiniteTruth("β")
+# Domain ⊤, ⊥, α, β
+t, b, α, β = FiniteTruth.([1:4]...)
 
-d4 = Vector{FiniteTruth}([⊥, α, β, ⊤])
+# α ∨ β = max{α, β}
+jointruthtable = [
+#   ⊤  ⊥  α  β
+    t, t, t, t, # ⊤
+    t, b, α, β, # ⊥
+    t, α, α, t, # α
+    t, β, t, β  # β
+]
 
-djointable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => α, (⊥, β) => β, (⊥, ⊤) => ⊤,
-    (α, ⊥) => α, (α, α) => α, (α, β) => ⊤, (α, ⊤) => ⊤,
-    (β, ⊥) => β, (β, α) => ⊤, (β, β) => β, (β, ⊤) => ⊤,
-    (⊤, ⊥) => ⊤, (⊤, α) => ⊤, (⊤, β) => ⊤, (⊤, ⊤) => ⊤
-)
+# α ∧ β = min{α, β}
+meettruthtable = [
+#   ⊤  ⊥  α  β
+    t, b, α, β, # ⊤
+    b, b, b, b, # ⊥
+    α, b, α, b, # α
+    β, b, b, β  # β
+]
 
-dmeettable = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}(
-    (⊥, ⊥) => ⊥, (⊥, α) => ⊥, (⊥, β) => ⊥, (⊥, ⊤) => ⊥,
-    (α, ⊥) => ⊥, (α, α) => α, (α, β) => ⊥, (α, ⊤) => α,
-    (β, ⊥) => ⊥, (β, α) => ⊥, (β, β) => β, (β, ⊤) => β,
-    (⊤, ⊥) => ⊥, (⊤, α) => α, (⊤, β) => β, (⊤, ⊤) => ⊤
-)
+join = BinaryOperation{4}(jointruthtable)
+meet = BinaryOperation{4}(meettruthtable)
+# In H4, the t-norm ⋅ is ∧
 
-djoin = BinaryOperation(d4, djointable)
-dmeet = BinaryOperation(d4, dmeettable)
-
-H4 = FiniteFLewAlgebra(djoin, dmeet, dmeet, ⊥, ⊤)
+H4 = FiniteFLewAlgebra{4}(join, meet, meet, b, t)