Debug of Tableaux

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

Setup

defmodule Util do
  def render res do
    case res do
      {:thm, proof} -> do_render proof
      {:csa, _model, proof} -> do_render proof
      {:timeout, partial_proof} -> do_render partial_proof
      other -> other
    end
  end

  defp do_render proof do
    frame = Kino.Frame.new
    Kino.render(frame)
    diagram = proof |> ShotTx.Proof.to_mermaid |> Kino.Mermaid.new
    Kino.Frame.render frame, diagram
  end
end

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

default_to_debug = true

form =
  Kino.Control.form(
    [
      name: Kino.Input.checkbox("Print debug logs", default: default_to_debug)
    ],
    report_changes: true
  )

set_logger_debug = fn
  true  -> Logger.configure(level: :debug)
  false -> Logger.configure(level: :error)
end

Kino.listen(form, fn event -> set_logger_debug.(event.data.name) end)

set_logger_debug.(default_to_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()

Simplification

import ShotDs.Hol.Sigils
import ShotDs.Util.Formatter
import ShotTx.Util.PropSimplify

simplify(~f"P & ~P") |> format!

simplify(~f"P | $true") |> format!

Tableaux Proving

import ShotDs.Hol.Sigils
import ShotTx.Prover

$\exists X. X$

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

render res

$a \land b \supset a$

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

render res

$a \supset a \lor b$

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

render res

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()
format_result res

render res

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

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

IO.puts ShotTx.Proof.to_text elem res, 1

render res

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
format_result res

render res

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
format_result res

render res

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

render res

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

render res

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

render res

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

render res

TPTP Problems

import ShotTx.Prover

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

render res