Debug of Tableaux

Mix.install([
  {:shot_tx, path: Path.join(__DIR__, "..")},
  {:kino, "~> 0.19.0"}
])

Setup

import ShotDs.Hol.Definitions
import ShotTx.Generation
import ShotDs.Util.Formatter
alias ShotDs.Data.Type

form =
  Kino.Control.form(
    [
      name: Kino.Input.checkbox("Debug", default: true)
    ],
    report_changes: true
  )

Kino.listen(form, fn event ->
  if event.data.name == true do
    Logger.configure(level: :debug)
  else
    Logger.configure(level: :warning)
  end
end)

Logger.configure(level: :debug)
form

Generation Algorithm (Type o)

gen_o(type_o())
|> Enum.with_index(1)
|> Enum.map(fn {t, idx} -> "(#{idx}) #{format!(t, true)}" end)
|> Enum.join("\n") |> IO.puts()

gen_o(type_oo())
|> Enum.with_index(1)
|> Enum.map(fn {t, idx} -> "(#{idx}) #{format!(t, true)}" end)
|> Enum.join("\n") |> IO.puts()

gen_o(type_ooo())
|> Enum.with_index(1)
|> Enum.map(fn {t, idx} -> "(#{idx}) #{format!(t, true)}" end)
|> Enum.join("\n") |> IO.puts()

gen_o(Type.new(:o, [type_oo()]))
|> Enum.with_index(1)
|> Enum.map(fn {t, idx} -> "(#{idx}) #{format!(t, true)}" end)
|> Enum.join("\n") |> IO.puts()

gen_o(Type.new(:o, [:o, :o, :o]))
|> Enum.with_index(1)
|> Enum.map(fn {t, idx} -> "(#{idx}) #{format!(t, true)}" end)
|> Enum.join("\n") |> IO.puts()

Tableaux Proving

import ShotDs.Hol.Sigils
import ShotTx.Prover

res = ~f"?[X: $o]: X" |> prove

frame = Kino.Frame.new()
Kino.render(frame)

res
|> then(fn {:thm, proof} -> proof end)
|> ShotTx.Proof.to_rich_mermaid()
|> then(& Kino.Frame.render(frame, Kino.Mermaid.new(&1)))

res = ~f"a & b => a" |> prove

frame = Kino.Frame.new()
Kino.render(frame)

res
|> then(fn {:thm, proof} -> proof end)
|> ShotTx.Proof.to_rich_mermaid()
|> then(& Kino.Frame.render(frame, Kino.Mermaid.new(&1)))

~f"a => (a | b)" |> prove

~f"~?[F : $i>$i>$o]: ![Y: $i>$o]: ?[X: $i]: F @ X = Y" |> prove

~f"p @ (a & b) => p @ (b & a)" |> prove

~f"![X : $o, Y : $o]: p @ X & p @ Y => p @ (X & Y)" |> prove

~f"""
(
  (p @ ^[X : $o]: X) &
  (p @ ^[X : $o]: ~X) &
  (p @ ^[X : $o]: $false) &
  (p @ ^[X : $o]: $true)
)
=>
![Y : $o>$o]: p @ Y
"""
|> prove

~f"""
(
  (p @ ^[X : $o]: X) &
  (p @ ^[X : $o]: ~X) &
  (p @ ^[X : $o]: $false) &
  (p @ ^[X : $o]: $true)
)
=>
?[Y : $o>$o]: ~ p @ Y
"""
|> prove

~f"p @ a & p @ b => p @ (a & b)" |> prove

~f"p @ a & q @ a => ?[X : $i>$o]: X @ a & X @ b" |> prove

TPTP Problems

alias ShotDs.Tptp
import ShotTx.Prover

{:ok, problem} = Tptp.parse_tptp_file("SET008^5")
res = prove(problem)

frame = Kino.Frame.new()
Kino.render(frame)

res
|> then(fn {:thm, proof} -> proof end)
|> ShotTx.Proof.to_rich_mermaid()
|> then(& Kino.Frame.render(frame, Kino.Mermaid.new(&1)))