ATP Development with Elixir

Mix.install([
  {:shot_tx, github: "jcschuster/ShotTx"},
  {:kino_shot_ds, "~> 0.1"},
  {:kino_atp_client, "~> 0.1.4"}
])

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 Util
import ShotDs.Hol.Sigils
import ShotDs.Parser
import ShotDs.Util.Formatter
import ShotTx.Prover

default_to_debug = false

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

Custom DSLs: Parsing Input via Sigils

# TPTP encoding for ∀ x, y. ∃ p. (p x) ⊃ (p y)
~f"![X: $i, Y: $i]: ?[P: $i>$o]: P @ X => P @ Y"
|> format! |> IO.puts

# Parsing TPTP problems
~p"""
thf(p_type, type, p: $i>$o).
thf(c_type, type, c: $i).
thf(ax1, axiom, p @ c).
thf(conj, conjecture,
  ?[X: $i]: P @ X
).
""" |> format! |> IO.puts

Custom Smart Cells

formula = "?[X : $i, Y : $i]: ( (f @ X) = f @ Y )"
context = ShotDs.Parser.parse_context!("f: $i>$i")

formula =
  case ShotDs.Parser.parse(formula, ctx: context) do
    {:ok, term_id} -> term_id
    {:error, reason} -> raise "Error: #{inspect(reason)}"
  end

:ok

IO.puts format! parsed_formula_or_problem

problem =
  "thf(f_type, type, f: $i>$i).\r\nthf(test, conjecture,\r\n    ?[X : $i, Y : $i]: ( (f @ X) = f @ Y )\r\n)."

problem =
  case ShotDs.Tptp.parse_tptp_string(problem) do
    {:ok, parsed} -> parsed
    {:error, reason} -> raise "Error: #{inspect(reason)}"
  end

:ok

IO.puts format! parsed_formula_or_problem

Proof Tree Rendering with Kino and Mermaid

res = prove ~f"![P, Q]: P & Q => Q & P", simplification: :none
IO.puts format_result res

render res

res = prove ~f"![P: $i>$o]: P @ a | P @ b => P @ b", simplification: :none
IO.puts format_result res

render res

Truth Grounding: ATPClient with SmartCell

AtpClient.SystemOnTptp.list_provers |> Enum.join("\n") |> IO.puts

problem = """
thf(test, conjecture,
    ![P: $o, Q: $o]: ((P & Q) => (Q & P))
).
"""

AtpClient.SystemOnTptp.query_system(problem, "Zipperpin---2.1")

# Generated by SystemOnTPTP Smart Cell
problem = "thf(test, conjecture,\r\n    ![P: $o, Q: $o]: ((P & Q) => (Q & P))\r\n)."
system_name = "Leo-III---1.7.20"
time_limit = 5

case AtpClient.SystemOnTptp.query_system(problem, system_name, time_limit_sec: time_limit, raw: true) do
  {:ok, result} ->
    IO.puts(result)
    result

  {:error, reason} ->
    raise "Error: #{inspect(reason)}"
end