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

$\exists X. X$

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

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

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

$a \land b \supset a$

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

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

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

$a \supset a \lor b$

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

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

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

Cantor: $\nexists F. \forall Y. \exists X. F X = Y$

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

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

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

Extensionality: $p (a \land b) \supset p (b \land a)$

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

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

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

Extensionality: $\forall X Y. p~X \land p~Y \supset p (X \land Y)$

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

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

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

Finite domain of type $o\to o$

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

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

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

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

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

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

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

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

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

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

res =
  ~f"p @ a & q @ a => ?[X : $i>$o]: X @ a & X @ b & X != (^[Y: $i]: $true)"
  |> prove

TPTP Problems

alias ShotDs.Tptp
import ShotTx.Prover

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

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

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