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.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 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
import ShotDs.Hol.Sigils
# Generated by SystemOnTPTP Smart Cell
problem = "%------------------------------------------------------------------------------\n% Case-split steamroller — one notch harder than the dessert puzzle.\n% bird < fox < wolf, plant 'corn'. The fox's diet is undetermined: the proof\n% must split on it, and BOTH branches reach the goal via different witnesses.\n% First-order content, THF syntax.\n%------------------------------------------------------------------------------\n\n% --- Signature ---------------------------------------------------------------\nthf(thing_decl,   type, thing   : $tType ).\nthf(animal_decl,  type, animal  : thing > $o ).\nthf(plant_decl,   type, plant   : thing > $o ).\nthf(eats_decl,    type, eats    : thing > thing > $o ).\nthf(smaller_decl, type, smaller : thing > thing > $o ).\nthf(bird_decl,    type, bird    : thing ).\nthf(fox_decl,     type, fox     : thing ).\nthf(wolf_decl,    type, wolf    : thing ).\nthf(corn_decl,    type, corn    : thing ).\n\n% --- Facts -------------------------------------------------------------------\nthf(bird_animal, axiom, animal @ bird ).\nthf(fox_animal,  axiom, animal @ fox ).\nthf(wolf_animal, axiom, animal @ wolf ).\nthf(corn_plant,  axiom, plant  @ corn ).\n\nthf(bird_eats_corn,   axiom, eats @ bird @ corn ).      % bird is a known plant-eater\nthf(bird_smaller_fox, axiom, smaller @ bird @ fox ).\nthf(fox_smaller_wolf, axiom, smaller @ fox  @ wolf ).\nthf(wolf_spurns_corn, axiom, ~ ( eats @ wolf @ corn ) ). % forces the wolf\n\n% --- The diet law ------------------------------------------------------------\n% Every animal eats either every plant, or every smaller plant-eating animal.\nthf(diet, axiom,\n    ! [X : thing]\n    : ( ( animal @ X )\n     => ( ( ! [Y : thing] : ( ( plant @ Y ) => ( eats @ X @ Y ) ) )\n        | ( ! [Y : thing]\n            : ( ( ( animal @ Y )\n                & ( smaller @ Y @ X )\n                & ( ? [Z : thing] : ( ( plant @ Z ) & ( eats @ Y @ Z ) ) ) )\n             => ( eats @ X @ Y ) ) ) ) ) ).\n\n% --- Conjecture --------------------------------------------------------------\n% Some animal eats a plant-eating animal.\nthf(goal, conjecture,\n    ? [X : thing]\n    : ( ( animal @ X )\n      & ? [Y : thing]\n        : ( ( animal @ Y )\n          & ( eats @ X @ Y )\n          & ? [Z : thing] : ( ( plant @ Z ) & ( eats @ Y @ Z ) ) ) ) ).\n%------------------------------------------------------------------------------\n"
system_name = "Zipperpin---2.1"
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

problem = ~p"""
%------------------------------------------------------------------------------
% Case-split steamroller — one notch harder than the dessert puzzle.
% bird < fox < wolf, plant 'corn'. The fox's diet is undetermined: the proof
% must split on it, and BOTH branches reach the goal via different witnesses.
% First-order content, THF syntax.
%------------------------------------------------------------------------------

% --- Signature ---------------------------------------------------------------
thf(thing_decl,   type, thing   : $tType ).
thf(animal_decl,  type, animal  : thing > $o ).
thf(plant_decl,   type, plant   : thing > $o ).
thf(eats_decl,    type, eats    : thing > thing > $o ).
thf(smaller_decl, type, smaller : thing > thing > $o ).
thf(bird_decl,    type, bird    : thing ).
thf(fox_decl,     type, fox     : thing ).
thf(wolf_decl,    type, wolf    : thing ).
thf(corn_decl,    type, corn    : thing ).

% --- Facts -------------------------------------------------------------------
thf(bird_animal, axiom, animal @ bird ).
thf(fox_animal,  axiom, animal @ fox ).
thf(wolf_animal, axiom, animal @ wolf ).
thf(corn_plant,  axiom, plant  @ corn ).

thf(bird_eats_corn,   axiom, eats @ bird @ corn ).      % bird is a known plant-eater
thf(bird_smaller_fox, axiom, smaller @ bird @ fox ).
thf(fox_smaller_wolf, axiom, smaller @ fox  @ wolf ).
thf(wolf_spurns_corn, axiom, ~ ( eats @ wolf @ corn ) ). % forces the wolf

% --- The diet law ------------------------------------------------------------
% Every animal eats either every plant, or every smaller plant-eating animal.
thf(diet, axiom,
    ! [X : thing]
    : ( ( animal @ X )
     => ( ( ! [Y : thing] : ( ( plant @ Y ) => ( eats @ X @ Y ) ) )
        | ( ! [Y : thing]
            : ( ( ( animal @ Y )
                & ( smaller @ Y @ X )
                & ( ? [Z : thing] : ( ( plant @ Z ) & ( eats @ Y @ Z ) ) ) )
             => ( eats @ X @ Y ) ) ) ) ) ).

% --- Conjecture --------------------------------------------------------------
% Some animal eats a plant-eating animal.
thf(goal, conjecture,
    ? [X : thing]
    : ( ( animal @ X )
      & ? [Y : thing]
        : ( ( animal @ Y )
          & ( eats @ X @ Y )
          & ? [Z : thing] : ( ( plant @ Z ) & ( eats @ Y @ Z ) ) ) ) ).
%------------------------------------------------------------------------------

"""
res = prove problem, timeout: 100, instance_based_gamma: false
format_result res
render res
problem = ~p"""
%------------------------------------------------------------------------------
% Mini-Steamroller — vereinfachte Schubert-Steamroller (vgl. PUZ031), THF
% Drei Kreaturen:  snail  <  bird  <  wolf   plus eine Pflanze 'corn'.
%------------------------------------------------------------------------------

% --- Signatur ----------------------------------------------------------------
thf(thing_decl,   type, thing   : $tType ).
thf(animal_decl,  type, animal  : thing > $o ).
thf(plant_decl,   type, plant   : thing > $o ).
thf(eats_decl,    type, eats    : thing > thing > $o ).
thf(smaller_decl, type, smaller : thing > thing > $o ).   % "viel kleiner als"
thf(snail_decl,   type, snail   : thing ).
thf(bird_decl,    type, bird    : thing ).
thf(wolf_decl,    type, wolf    : thing ).
thf(corn_decl,    type, corn    : thing ).

% --- Höherstufige Abkürzungen ------------------------------------------------
% eats_all X S  <=>  X frisst jedes Element der Menge S.
thf(eats_all_decl, type, eats_all : thing > ( thing > $o ) > $o ).
thf(eats_all_def, definition,
    ( eats_all
    = ( ^ [X : thing, S : thing > $o]
        : ! [Y : thing] : ( ( S @ Y ) => ( eats @ X @ Y ) ) ) ) ).

% plant_eater Y  <=>  Y frisst irgendeine Pflanze.
thf(plant_eater_decl, type, plant_eater : thing > $o ).
thf(plant_eater_def, definition,
    ( plant_eater
    = ( ^ [Y : thing] : ? [Z : thing] : ( ( plant @ Z ) & ( eats @ Y @ Z ) ) ) ) ).

% --- Fakten ------------------------------------------------------------------
thf(snail_animal, axiom, animal @ snail ).
thf(bird_animal,  axiom, animal @ bird ).
thf(wolf_animal,  axiom, animal @ wolf ).
thf(corn_plant,   axiom, plant  @ corn ).

thf(snail_smaller_bird, axiom, smaller @ snail @ bird ).
thf(bird_smaller_wolf,  axiom, smaller @ bird  @ wolf ).

thf(snail_eats_a_plant, axiom, plant_eater @ snail ).
thf(bird_spares_snail,  axiom, ~ ( eats @ bird @ snail ) ).
thf(wolf_spurns_corn,   axiom, ~ ( eats @ wolf @ corn  ) ).

% --- Das Fressgesetz ---------------------------------------------------------
% Jedes Tier frisst entweder alle Pflanzen, oder alle kleineren Pflanzenfresser.
thf(diet, axiom,
    ! [X : thing]
    : ( ( animal @ X )
     => ( ( eats_all @ X @ plant )
        | ( eats_all @ X
            @ ( ^ [Y : thing]
                : ( ( animal @ Y )
                  & ( smaller @ Y @ X )
                  & ( plant_eater @ Y ) ) ) ) ) ) ).

% --- Behauptung --------------------------------------------------------------
% Es gibt ein Tier, das ein pflanzenfressendes Tier frisst.
% thf(goal, conjecture,
%    ? [X : thing]
%    : ( ( animal @ X )
%      & ? [Y : thing] : ( ( animal @ Y )
%                        & ( eats @ X @ Y )
%                        & ( plant_eater @ Y ) ) ) ).

thf(goal, conjecture,
  plant_eater @ bird
).
%------------------------------------------------------------------------------
"""
res = prove problem, timeout: 100
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