Powered by AppSignal & Oban Pro
Notesclub
Sign in with GitHub
created by hec & contributors
terms privacy

Debug of Tableaux

examples/debug.livemd

avatar
Johannes Schuster
avatar
avatar
Share to X
Share to Bluesky
More notebooks

Debug of Tableaux

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

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
res = ~f"![P:$i>$o, Q:$i>$o]: ((?[X:$i]: P @ X & Q @ X) => (?[X:$i]: P @ X) & (?[X:$i]: Q @ X))"
|> prove
format_result res
render res

$\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

Section

import ShotTx.Prover
import ShotDs.Hol.Sigils
input = ~p"""
%------------------------------------------------------------------------------
% File     : PUZ001^1 : TPTP v9.2.1.
% Domain   : Puzzles
% Problem  : Dreadbury Mansion
% Version  : Especial. Theorem formulation : Reduced > Complete.
% English  : Who killed Aunt Agatha.
% Status   : Theorem
%------------------------------------------------------------------------------
%----Types
thf(person_type,type,
    person: $tType ).

%----Constants
thf(agatha_decl,type,
    agatha: person ).

thf(butler_decl,type,
    butler: person ).

thf(charles_decl,type,
    charles: person ).

%----Predicates
thf(lives_decl,type,
    lives: person > $o ).

thf(killed_decl,type,
    killed: person > person > $o ).

thf(hates_decl,type,
    hates: person > person > $o ).

thf(richer_decl,type,
    richer: person > person > $o ).

%----Problem axioms
thf(pel55_1,axiom,
    ? [X: person] :
      ( ( lives @ X )
      & ( killed @ X @ agatha ) ) ).

thf(pel55_2_1,axiom,
    lives @ agatha ).

thf(pel55_2_2,axiom,
    lives @ butler ).

thf(pel55_2_3,axiom,
    lives @ charles ).

thf(pel55_3,axiom,
    ! [X: person] :
      ( ( lives @ X )
     => ( ( X = agatha )
        | ( X = butler )
        | ( X = charles ) ) ) ).

thf(pel55_4,axiom,
    ! [X: person,Y: person] :
      ( ( killed @ X @ Y )
     => ( hates @ X @ Y ) ) ).

thf(pel55_5,axiom,
    ! [X: person,Y: person] :
      ( ( killed @ X @ Y )
     => ~ ( richer @ X @ Y ) ) ).

thf(pel55_6,axiom,
    ! [X: person] :
      ( ( hates @ agatha @ X )
     => ~ ( hates @ charles @ X ) ) ).

thf(pel55_7,axiom,
    ! [X: person] :
      ( ( X != butler )
     => ( hates @ agatha @ X ) ) ).

thf(pel55_8,axiom,
    ! [X: person] :
      ( ~ ( richer @ X @ agatha )
     => ( hates @ butler @ X ) ) ).

thf(pel55_9,axiom,
    ! [X: person] :
      ( ( hates @ agatha @ X )
     => ( hates @ butler @ X ) ) ).

thf(pel55_10,axiom,
    ! [X: person] :
    ? [Y: person] :
      ~ ( hates @ X @ Y ) ).

thf(pel55_11,axiom,
    agatha != butler ).

thf(pel55,conjecture,
    killed @ agatha @ agatha ).

%------------------------------------------------------------------------------
"""

{res, stats} = prove input, stats: true, timeout: 100
# format_result res
stats
render res
# Generated by SystemOnTPTP Smart Cell
problem = "%------------------------------------------------------------------------------\n% File     : PUZ001^1 : TPTP v9.2.1.\n% Domain   : Puzzles\n% Problem  : Dreadbury Mansion\n% Version  : Especial. Theorem formulation : Reduced > Complete.\n% English  : Who killed Aunt Agatha.\n% Status   : Theorem\n%------------------------------------------------------------------------------\n%----Types\nthf(person_type,type,\n    person: $tType ).\n\n%----Constants\nthf(agatha_decl,type,\n    agatha: person ).\n\nthf(butler_decl,type,\n    butler: person ).\n\nthf(charles_decl,type,\n    charles: person ).\n\n%----Predicates\nthf(lives_decl,type,\n    lives: person > $o ).\n\nthf(killed_decl,type,\n    killed: person > person > $o ).\n\nthf(hates_decl,type,\n    hates: person > person > $o ).\n\nthf(richer_decl,type,\n    richer: person > person > $o ).\n\n%----Problem axioms\nthf(pel55_1,axiom,\n    ? [X: person] :\n      ( ( lives @ X )\n      & ( killed @ X @ agatha ) ) ).\n\nthf(pel55_2_1,axiom,\n    lives @ agatha ).\n\nthf(pel55_2_2,axiom,\n    lives @ butler ).\n\nthf(pel55_2_3,axiom,\n    lives @ charles ).\n\nthf(pel55_3,axiom,\n    ! [X: person] :\n      ( ( lives @ X )\n     => ( ( X = agatha )\n        | ( X = butler )\n        | ( X = charles ) ) ) ).\n\nthf(pel55_4,axiom,\n    ! [X: person,Y: person] :\n      ( ( killed @ X @ Y )\n     => ( hates @ X @ Y ) ) ).\n\nthf(pel55_5,axiom,\n    ! [X: person,Y: person] :\n      ( ( killed @ X @ Y )\n     => ~ ( richer @ X @ Y ) ) ).\n\nthf(pel55_6,axiom,\n    ! [X: person] :\n      ( ( hates @ agatha @ X )\n     => ~ ( hates @ charles @ X ) ) ).\n\nthf(pel55_7,axiom,\n    ! [X: person] :\n      ( ( X != butler )\n     => ( hates @ agatha @ X ) ) ).\n\nthf(pel55_8,axiom,\n    ! [X: person] :\n      ( ~ ( richer @ X @ agatha )\n     => ( hates @ butler @ X ) ) ).\n\nthf(pel55_9,axiom,\n    ! [X: person] :\n      ( ( hates @ agatha @ X )\n     => ( hates @ butler @ X ) ) ).\n\nthf(pel55_10,axiom,\n    ! [X: person] :\n    ? [Y: person] :\n      ~ ( hates @ X @ Y ) ).\n\nthf(pel55_11,axiom,\n    agatha != butler ).\n\nthf(pel55,conjecture,\n    killed @ agatha @ agatha ).\n\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

Other notebooks:

Back