Day1-symbolic-knowledge.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "354b97bf",
   "metadata": {},
   "source": [
    "# Symbolic knowledge manipulation with SoleLogics.jl"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c216d7ad",
   "metadata": {},
   "source": [
    "## Propositional Logic"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4e8dd1a4",
   "metadata": {},
   "source": [
    "### Formulas & Interpretations"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "b627caf4",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\u001b[32m\u001b[1m  Activating\u001b[22m\u001b[39m project at `~/Desktop/modal-symbolic-learning-course`\n",
      "\u001b[32m\u001b[1m    Updating\u001b[22m\u001b[39m registry at `~/.julia/registries/General`\n",
      "\u001b[32m\u001b[1m    Updating\u001b[22m\u001b[39m git-repo `https://github.com/JuliaRegistries/General.git`\n",
      "\u001b[32m\u001b[1m  No Changes\u001b[22m\u001b[39m to `~/Desktop/modal-symbolic-learning-course/Project.toml`\n",
      "\u001b[32m\u001b[1m  No Changes\u001b[22m\u001b[39m to `~/Desktop/modal-symbolic-learning-course/Manifest.toml`\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001b[32m\u001b[1mStatus\u001b[22m\u001b[39m `~/Desktop/modal-symbolic-learning-course/Project.toml`\n",
      "  \u001b[90m[a93c6f00] \u001b[39mDataFrames v1.6.1\n",
      "  \u001b[90m[7806a523] \u001b[39mDecisionTree v0.12.4\n",
      "  \u001b[90m[7073ff75] \u001b[39mIJulia v1.24.2\n",
      "  \u001b[90m[033835bb] \u001b[39mJLD2 v0.4.38\n",
      "\u001b[33m⌅\u001b[39m \u001b[90m[add582a8] \u001b[39mMLJ v0.19.5\n",
      "  \u001b[90m[c6f25543] \u001b[39mMLJDecisionTreeInterface v0.4.0\n",
      "  \u001b[90m[e54bda2e] \u001b[39mModalDecisionTrees v0.3.3\n",
      "  \u001b[90m[91a5bcdd] \u001b[39mPlots v1.39.0\n",
      "  \u001b[90m[7b3b3b3f] \u001b[39mSole v0.3.1\n",
      "  \u001b[90m[b002da8f] \u001b[39mSoleLogics v0.6.12\n",
      "  \u001b[90m[4249d9c7] \u001b[39mSoleModels v0.5.3\n",
      "  \u001b[90m[2913bbd2] \u001b[39mStatsBase v0.34.2\n",
      "  \u001b[90m[9a3f8284] \u001b[39mRandom\n",
      "\u001b[36m\u001b[1mInfo\u001b[22m\u001b[39m Packages marked with \u001b[33m⌅\u001b[39m have new versions available but compatibility constraints restrict them from upgrading. To see why use `status --outdated`\n"
     ]
    }
   ],
   "source": [
    "using Pkg\n",
    "Pkg.activate(\".\")\n",
    "Pkg.instantiate()\n",
    "Pkg.update()\n",
    "Pkg.status()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "id": "c4ad7184",
   "metadata": {},
   "outputs": [],
   "source": [
    "using SoleLogics"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "id": "c54cfd90",
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Atom{String}: it's alive!"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "p = Atom(\"it's alive!\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "id": "f3d1a4ed",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Atom{String}: it's mortal!"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "q = Atom(\"it's mortal!\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "id": "8df839b8",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:∧}}: it's alive! ∧ (it's alive! ∧ it's mortal! ∨ it's alive! ∧ it's mortal!)"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "φ = p ∧ q"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "df54799c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "φ isa Formula && p isa Formula"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "id": "0da9fd85",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "∧\n",
      "(Atom{String}: it's alive!, SyntaxBranch{NamedConnective{:∨}}: it's alive! ∧ it's mortal! ∨ it's alive! ∧ it's mortal!)\n"
     ]
    }
   ],
   "source": [
    "# φ is the root node of a syntax tree.\n",
    "# Print the syntax token at the root node\n",
    "println(token(φ))\n",
    "# Print the children of the root node\n",
    "println(children(φ))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "060f5efc",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "negateformula (generic function with 1 method)"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Create a method for negating any formula\n",
    "function negateformula(f::Formula)\n",
    "    return ¬f\n",
    "end"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "id": "530f79fc",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:¬}}: ¬(it's alive! ∧ (it's alive! ∧ it's mortal! ∨ it's alive! ∧ it's mortal!))"
      ]
     },
     "execution_count": 57,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "negateformula(φ)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "358814d4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:¬}}: ¬it's alive!"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "negateformula(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "c91481b7",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\"it's alive! ∧ it's mortal!\""
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Obtain the string representation of a Formula\n",
    "syntaxstring(φ)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "id": "36c1ab4d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:∧}}: it's alive! ∧ it's mortal!"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# I can also parse Formula's from standard string representations\n",
    "φ = parseformula(\"it's alive! ∧ it's mortal!\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "ae67b123",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "my_own_string_representation (generic function with 3 methods)"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "function my_own_string_representation(f::SyntaxBranch{NamedConnective{:¬}})\n",
    "    return \"It is not the case that $(my_own_string_representation(first(children(f))))\"\n",
    "end\n",
    "function my_own_string_representation(f::SyntaxBranch{NamedConnective{:∧}})\n",
    "    subformula1, subformula2 = children(f)\n",
    "    return \"both $(my_own_string_representation(subformula1)) and $(my_own_string_representation(subformula2))\"\n",
    "end\n",
    "function my_own_string_representation(f::SyntaxTree)\n",
    "    return syntaxstring(f)\n",
    "end"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "65f06c8e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\"It is not the case that both it's alive! and it's mortal!\""
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "my_own_string_representation(¬φ)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "b54406ea",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TruthDict with values:\n",
       "┌──────────────┬─────────────┐\n",
       "│\u001b[1m it's mortal! \u001b[0m│\u001b[1m it's alive! \u001b[0m│\n",
       "│\u001b[90m       String \u001b[0m│\u001b[90m      String \u001b[0m│\n",
       "├──────────────┼─────────────┤\n",
       "│            ⊥ │           ⊤ │\n",
       "└──────────────┴─────────────┘\n"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "soul = TruthDict([p => true, q => false])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "1a700c75",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TruthDict with values:\n",
       "┌──────────────┬─────────────┐\n",
       "│\u001b[1m it's mortal! \u001b[0m│\u001b[1m it's alive! \u001b[0m│\n",
       "│\u001b[90m       String \u001b[0m│\u001b[90m      String \u001b[0m│\n",
       "├──────────────┼─────────────┤\n",
       "│            ⊤ │           ⊤ │\n",
       "└──────────────┴─────────────┘\n"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "body = TruthDict([p => true, q => true])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "ca7fd25e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "check(p, soul) # soul is alive"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "6563d348",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "false"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "check(φ, soul) # But not both alive and mortal"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "5183edd2",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "check(φ, body) # body is both alive and mortal!"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "63dd28ac",
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(⊥, ⊤)"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# These objects can actually be used as dictionaries from Formula to Truth values\n",
    "# For example, we both assign ⊤ (top) to the atom \"alive\"\n",
    "soul[q], body[q]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "id": "31a8781e",
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "⊤"
      ]
     },
     "execution_count": 64,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "body[q]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "id": "1c40c64b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Top"
      ]
     },
     "execution_count": 67,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "7ae99b5d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# What is ⊤?\n",
    "⊤ isa Truth      &&     ⊤ isa Formula"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "09294823",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(⊤, ⊥, ∧, ∨, →)"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# By the way, if you find these Unicode characters uncomfortable to work with, they have aliases:\n",
    "(TOP, BOT, CONJUNCTION, DISJUNCTION, IMPLICATION)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "id": "d9c52872",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "⊥"
      ]
     },
     "execution_count": 73,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Actually, indexing (with [⋅]) can be used to check generic Formula's\n",
    "soul[φ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "id": "ec744724",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "⊥"
      ]
     },
     "execution_count": 70,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# This is syntactic sugar for the *interpretation* algorithm, which is actually more general than check!\n",
    "interpret(φ, soul)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "id": "9a69ccb3",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Atom{String}: ?Unknown property?"
      ]
     },
     "execution_count": 75,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# In fact, it also works under incomplete information.\n",
    "body[φ ∧ Atom(\"?Unknown property?\")]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "9c58e360",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "⊤"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Notice how in this example, with an *unknown atom*, it uses the *known* information to simplify the formula\n",
    "body[φ ∨ Atom(\"?Unknown property?\")]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "717be11c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# So ultimately, `check` is just a shortcut for making sure that `interpret` simplifies the formula to ⊤\n",
    "check(φ, soul) == istop(interpret(φ, soul))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "5b9f702d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:∨}}: ¬a ∨ a ∧ b ∨ a ∧ b ∧ (b → b)"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Let's generate random formulas\n",
    "treeheight = 3\n",
    "@atoms a b\n",
    "φ2 = randformula(treeheight, [a,b], SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "35c62634",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:¬}}: ¬(b ∧ a ∧ ¬b)"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Let's control reproducibility, though ;)\n",
    "using Random\n",
    "rng = Random.MersenneTwister(1)\n",
    "φ2 = randformula(rng, treeheight, [a,b], SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "b5f569c7",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SyntaxBranch{NamedConnective{:∨}}: ¬a ∨ b ∨ ¬b"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "normalize(φ2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d0e53736",
   "metadata": {},
   "source": [
    "#### Exercise 1:\n",
    "Check many, randomly-generated formulas on the alphabet ${p, q}$ on both `soul` and `body`.\n",
    "Do `soul` and `body` have the same probability of satisfying a generic formula? Can you estimate this probability?"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "17021f26",
   "metadata": {},
   "source": [
    "### Scalar interpretations"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3521b00b",
   "metadata": {},
   "source": [
    "Now, let's consider a propositional interpretation on scalar attributes $A_1, A_2, \\ldots$, and check formulas on an alphabet $\\mathcal{A} \\subseteq \\{A_i < v, v \\in \\mathbb{R}\\}$ on it.\n",
    "\n",
    "We start by defining the atoms of type $A_i < v.$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "f2a2c3f7",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\"A2 < 10\""
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import SoleLogics: syntaxstring\n",
    "\n",
    "struct ConditionOnAttribute\n",
    "    i_attribute::Integer\n",
    "    threshold::Real\n",
    "end\n",
    "\n",
    "function syntaxstring(c::ConditionOnAttribute; kwargs...)\n",
    "    \"A$(c.i_attribute) < $(c.threshold)\"\n",
    "end\n",
    "\n",
    "syntaxstring(ConditionOnAttribute(2, 10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "0350840a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "interpret (generic function with 12 methods)"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "using SoleLogics: AbstractAssignment # Abstract type for propositional Interpretations\n",
    "\n",
    "struct TabularInterpretation{T<:Real} <: AbstractAssignment\n",
    "    vals::Vector{T}\n",
    "end\n",
    "\n",
    "import SoleLogics: interpret\n",
    "\n",
    "function interpret(a::Atom{ConditionOnAttribute}, I::TabularInterpretation)\n",
    "    cond = value(a)\n",
    "    return (I.vals[cond.i_attribute] < cond.threshold ? ⊤ : ⊥)\n",
    "end"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "ec6a49ad",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TabularInterpretation{Float64}([0.23603334566204692, 0.34651701419196046, 0.3127069683360675, 0.00790928339056074])"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "rng = Random.MersenneTwister(1)\n",
    "n_variables = 4\n",
    "\n",
    "vals = rand(rng, n_variables)\n",
    "I = TabularInterpretation(vals)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "f5d49221",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "44-element Vector{String}:\n",
       " \"A1 < 0.0\"\n",
       " \"A1 < 0.1\"\n",
       " \"A1 < 0.2\"\n",
       " \"A1 < 0.3\"\n",
       " \"A1 < 0.4\"\n",
       " \"A1 < 0.5\"\n",
       " \"A1 < 0.6\"\n",
       " \"A1 < 0.7\"\n",
       " \"A1 < 0.8\"\n",
       " \"A1 < 0.9\"\n",
       " \"A1 < 1.0\"\n",
       " \"A2 < 0.0\"\n",
       " \"A2 < 0.1\"\n",
       " ⋮\n",
       " \"A3 < 1.0\"\n",
       " \"A4 < 0.0\"\n",
       " \"A4 < 0.1\"\n",
       " \"A4 < 0.2\"\n",
       " \"A4 < 0.3\"\n",
       " \"A4 < 0.4\"\n",
       " \"A4 < 0.5\"\n",
       " \"A4 < 0.6\"\n",
       " \"A4 < 0.7\"\n",
       " \"A4 < 0.8\"\n",
       " \"A4 < 0.9\"\n",
       " \"A4 < 1.0\""
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A = Atom.([ConditionOnAttribute(v, t) for v in 1:n_variables for t in 0:0.1:1.0])\n",
    "syntaxstring.(A)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "b33b3c32",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "44-element Vector{BooleanTruth}:\n",
       " ⊥\n",
       " ⊥\n",
       " ⊥\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊥\n",
       " ⊥\n",
       " ⋮\n",
       " ⊤\n",
       " ⊥\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤\n",
       " ⊤"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[interpret(cond, I) for cond in A]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "id": "28f7a862",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "10-element Vector{Pair{String}}:\n",
       "                 \"(¬A2 < 0.4 ∧ (A1 < 0.5 → A4 < 0.8)) → (A4 < 0.4 ∧ A4 < 0.9 ∧ A2 < 0.9 ∧ A1 < 0.2)\" => ⊤\n",
       "                     \"A4 < 0.1 ∨ A2 < 0.6 ∨ A4 < 0.8 ∨ A2 < 0.5 ∨ ¬A4 < 0.8 ∧ (A2 < 0.4 → A1 < 0.5)\" => ⊤\n",
       "                                                   \"¬(A3 < 0.6 ∧ A4 < 0.9) ∧ ¬(A2 < 0.3 → A1 < 1.0)\" => ⊥\n",
       "                                                \"¬¬A4 < 0.6 ∧ ((¬A1 < 0.0) → (A2 < 0.4 ∧ A2 < 0.3))\" => ⊥\n",
       "   \"((A4 < 0.4 → A4 < 1.0) ∨ A1 < 0.7 ∨ A2 < 0.7) → ((A3 < 0.3 → A4 < 0.3) ∧ (A2 < 0.2 ∨ A3 < 0.5))\" => ⊤\n",
       " \"((A4 < 0.0 → A2 < 0.3) → (A4 < 0.2 ∧ A3 < 0.9)) ∨ ((A1 < 0.8 → A1 < 0.4) → (A2 < 0.7 → A2 < 0.0))\" => ⊤\n",
       "                           \"¬A3 < 0.6 ∧ ¬A3 < 1.0 ∧ ((A3 < 0.5 → A3 < 0.5) → (A3 < 0.8 ∧ A4 < 0.3))\" => ⊥\n",
       "                                                                \"¬(A3 < 0.6 ∧ A1 < 0.1 ∧ ¬A1 < 0.7)\" => ⊤\n",
       "                                                   \"¬(A1 < 0.0 ∨ A3 < 0.5) ∧ ¬(A4 < 0.2 ∨ A1 < 0.8)\" => ⊥\n",
       "                                                                          \"¬(¬A1 < 0.5 ∨ ¬A3 < 0.8)\" => ⊤"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "rng = Random.MersenneTwister(32)\n",
    "\n",
    "[begin\n",
    "f = randformula(rng, 3, A, SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES)\n",
    "syntaxstring(f) => interpret(f, I)\n",
    "end for _ in 1:10]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7f0ae20a",
   "metadata": {},
   "source": [
    "#### Exercise 2\n",
    "Check many, randomly-generated formulas on many, randomly-generated tabular interpretations,\n",
    "and store the formulas that satisfy the highest number of instances!"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "41df4adb",
   "metadata": {},
   "source": [
    "## Modal Logic"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "id": "232ed72c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SoleLogics.ExplicitCrispUniModalFrame{SoleLogics.World{Int64}, SimpleDiGraph{Int64}} with\n",
       "- worlds = [\"1\", \"2\", \"3\", \"4\", \"5\"]\n",
       "- accessibles = \n",
       "\t1 -> [2, 3]\n",
       "\t2 -> [4]\n",
       "\t3 -> [4, 5]\n",
       "\t4 -> []\n",
       "\t5 -> []\n"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Instantiate a frame with 5 worlds and 5 edges\n",
    "using Graphs\n",
    "\n",
    "worlds = SoleLogics.World.(1:5)\n",
    "edges = Edge.([(1,2), (1,3), (2,4), (3,4), (3,5)])\n",
    "fr = SoleLogics.ExplicitCrispUniModalFrame(worlds, Graphs.SimpleDiGraph(edges))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "a50761c4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2-element Vector{SoleLogics.World{Int64}}:\n",
       " SoleLogics.World{Int64}(2)\n",
       " SoleLogics.World{Int64}(3)"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Pick the first world\n",
    "w1 = worlds[1]\n",
    "\n",
    "# Enumerate the world that are accessible from the first world\n",
    "accessibles(fr, w1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "dda40348",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "KripkeStructure{SoleLogics.ExplicitCrispUniModalFrame{SoleLogics.World{Int64}, SimpleDiGraph{Int64}}, Dict{SoleLogics.World{Int64}, TruthDict{Dict{Atom{String}, BooleanTruth}}}} with\n",
       "- frame = SoleLogics.ExplicitCrispUniModalFrame{SoleLogics.World{Int64}, SimpleDiGraph{Int64}} with\n",
       "- worlds = [\"1\", \"2\", \"3\", \"4\", \"5\"]\n",
       "- accessibles = \n",
       "\t1 -> [2, 3]\n",
       "\t2 -> [4]\n",
       "\t3 -> [4, 5]\n",
       "\t4 -> []\n",
       "\t5 -> []\n",
       "- valuations = \n",
       "\t1 -> TruthDict([it's mortal! => ⊥, it's alive! => ⊤])\n",
       "\t2 -> TruthDict([it's mortal! => ⊤, it's alive! => ⊤])\n",
       "\t3 -> TruthDict([it's mortal! => ⊥, it's alive! => ⊤])\n",
       "\t4 -> TruthDict([it's mortal! => ⊥, it's alive! => ⊥])\n",
       "\t5 -> TruthDict([it's mortal! => ⊤, it's alive! => ⊥])\n"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Assign each world a propositional interpretation\n",
    "valuation = Dict([\n",
    "        worlds[1] => TruthDict([p => TOP, q => BOT]),\n",
    "        worlds[2] => TruthDict([p => TOP, q => TOP]),\n",
    "        worlds[3] => TruthDict([p => TOP, q => BOT]),\n",
    "        worlds[4] => TruthDict([p => BOT, q => BOT]),\n",
    "        worlds[5] => TruthDict([p => BOT, q => TOP]),\n",
    "     ])\n",
    "\n",
    "# Instantiate a Kripke structure\n",
    "K = KripkeStructure(fr, valuation)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "3cad233c",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "□(it's alive! → it's mortal!) ∨ ¬(it's alive! → it's alive!)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "5-element Vector{Pair{SoleLogics.World{Int64}, Bool}}:\n",
       " SoleLogics.World{Int64}(1) => 0\n",
       " SoleLogics.World{Int64}(2) => 1\n",
       " SoleLogics.World{Int64}(3) => 1\n",
       " SoleLogics.World{Int64}(4) => 1\n",
       " SoleLogics.World{Int64}(5) => 1"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Generate a random modal formula\n",
    "φmodal = randformula(Random.MersenneTwister(14), 3, [p,q], SoleLogics.BASE_MODAL_CONNECTIVES)\n",
    "\n",
    "println(syntaxstring(φmodal))\n",
    "\n",
    "# Check the formula on each world of the Kripke structure\n",
    "[w => check(φmodal, K, w) for w in worlds]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "67913778",
   "metadata": {},
   "source": [
    "#### Exercise 3\n",
    "Check many, randomly-generated *modal* formulas on many, randomly-generated *modal* interpretations,\n",
    "and store the formulas that satisfy the highest number of instances!"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "72d1413a",
   "metadata": {},
   "source": [
    "#### Exercise 4\n",
    "Define a structure for representing a *modal* interpretation on scalar variables. You can see if your solution it works by running the cell below, which instantiates a random modal scalar interpretation.\n",
    "\n",
    "Note: Julia [currently](https://github.com/timholy/Revise.jl/issues/18) does not allow redefining structures at the global scope, so the code is wrapped in a module."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "14c0d1e6",
   "metadata": {},
   "outputs": [
    {
     "ename": "LoadError",
     "evalue": "UndefVarError: `ModalInterpretation` not defined",
     "output_type": "error",
     "traceback": [
      "UndefVarError: `ModalInterpretation` not defined",
      "",
      "Stacktrace:",
      " [1] top-level scope",
      "   @ In[41]:20"
     ]
    }
   ],
   "source": [
    "module exercise4\n",
    "\n",
    "export ModalInterpretation\n",
    "\n",
    "using Main: ConditionOnAttribute\n",
    "\n",
    "using SoleLogics\n",
    "\n",
    "using SoleLogics: AbstractFrame, World, AbstractKripkeStructure\n",
    "\n",
    "# TODO:\n",
    "# struct ModalInterpretation{FR<:AbstractFrame,T<:Real} <: AbstractKripkeStructure\n",
    "#     frame::FR\n",
    "#     vals::???\n",
    "# end\n",
    "\n",
    "import SoleLogics: interpret, frame\n",
    "\n",
    "# Retrieve the interpretation's frame\n",
    "frame(i::ModalInterpretation) = i.frame\n",
    "\n",
    "# TODO:\n",
    "# function interpret(a::Atom{ConditionOnAttribute}, I::ModalInterpretation, w::World)\n",
    "#     cond = value(a)\n",
    "#     v = ???\n",
    "#     return (v < cond.threshold ? TOP : BOT)\n",
    "# end\n",
    "\n",
    "\n",
    "end # end module"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "id": "50dd1e5a",
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "ename": "LoadError",
     "evalue": "UndefVarError: `ModalInterpretation` not defined",
     "output_type": "error",
     "traceback": [
      "UndefVarError: `ModalInterpretation` not defined",
      "",
      "Stacktrace:",
      " [1] top-level scope",
      "   @ In[42]:14"
     ]
    }
   ],
   "source": [
    "using .exercise4\n",
    "\n",
    "rng = Random.MersenneTwister(1)\n",
    "n_variables = 4\n",
    "n_worlds = 5\n",
    "n_edges = 7\n",
    "n_formulas = 10\n",
    "\n",
    "worlds = SoleLogics.World.(1:n_worlds)\n",
    "g = SimpleDiGraph(n_worlds, n_edges; rng)\n",
    "fr = SoleLogics.ExplicitCrispUniModalFrame(worlds, g)\n",
    "variable_values = [rand(n_variables) for w in worlds]\n",
    "\n",
    "Imodal = ModalInterpretation(fr, variable_values)\n",
    "\n",
    "for i_formula in 1:n_formulas\n",
    "    φmodal = randformula(Random.MersenneTwister(i_formula), 2, A, SoleLogics.BASE_MODAL_CONNECTIVES)\n",
    "\n",
    "    println(syntaxstring(φmodal) => [\"w$(SoleLogics.name(w))\" => check(φmodal, Imodal, w) for w in worlds])\n",
    "    println()\n",
    "end"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Julia 1.9.0",
   "language": "julia",
   "name": "julia-1.9"
  },
  "language_info": {
   "file_extension": ".jl",
   "mimetype": "application/julia",
   "name": "julia",
   "version": "1.9.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}