Demo of the AtpClient Smart Cells

Mix.install([
  {:kino_atp_client, path: Path.expand("..", __DIR__)}
])

SystemOnTPTP

# Generated by SystemOnTPTP Smart Cell
problem = "thf(test, conjecture, $true => $true)."
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

$$X + 5 = 10$$

$$X \cdot Y = 15$$

$$Z + Y = 3$$

# Generated by SystemOnTPTP Smart Cell
problem = "%------------------------------------------------------------------------------\n% Church numerals over base type $i, existential arithmetic problem.\n% A Church numeral has type (i>i)>i>i.\n%------------------------------------------------------------------------------\n\nthf(nat_type,type,    nat: $tType ).\n% nat abbreviates ($i > $i) > $i > $i\n\n% Zero and successor\nthf(zero_decl,type,   zero: ( $i > $i ) > $i > $i ).\nthf(zero_def,definition,\n    zero = ( ^ [F: $i > $i, X: $i] : X ) ).\n\nthf(succ_decl,type,   succ: ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ).\nthf(succ_def,definition,\n    succ = ( ^ [N: ( $i > $i ) > $i > $i, F: $i > $i, X: $i] : ( F @ ( N @ F @ X ) ) ) ).\n\n% Addition:  m + n = lambda f x. m f (n f x)\nthf(plus_decl,type,   plus:\n    ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ).\nthf(plus_def,definition,\n    plus = ( ^ [M: ( $i > $i ) > $i > $i, N: ( $i > $i ) > $i > $i, F: $i > $i, X: $i] :\n               ( M @ F @ ( N @ F @ X ) ) ) ).\n\n% Multiplication:  m * n = lambda f. m (n f)\nthf(mult_decl,type,   mult:\n    ( ( $i > $i ) > $i > $i ) > ( ( $i > $i ) > $i > $i ) > ( $i > $i ) > $i > $i ).\nthf(mult_def,definition,\n    mult = ( ^ [M: ( $i > $i ) > $i > $i, N: ( $i > $i ) > $i > $i, F: $i > $i] :\n               ( M @ ( N @ F ) ) ) ).\n\n% Numeral constants needed\nthf(five_decl,type,   five: ( $i > $i ) > $i > $i ).\nthf(five_def,definition,\n    five = ( ^ [F: $i > $i, X: $i] : ( F @ ( F @ ( F @ ( F @ ( F @ X ) ) ) ) ) ) ).\n\nthf(ten_decl,type,    ten: ( $i > $i ) > $i > $i ).\nthf(ten_def,definition,\n    ten = ( ^ [F: $i > $i, X: $i] :\n              ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ X ) ) ) ) ) ) ) ) ) ) ) ).\n\nthf(fifteen_decl,type, fifteen: ( $i > $i ) > $i > $i ).\nthf(fifteen_def,definition,\n    fifteen = ( ^ [F: $i > $i, X: $i] :\n              ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @ ( F @\n              ( F @ ( F @ ( F @ ( F @ ( F @ X ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).\n\nthf(three_decl,type,  three: ( $i > $i ) > $i > $i ).\nthf(three_def,definition,\n    three = ( ^ [F: $i > $i, X: $i] : ( F @ ( F @ ( F @ X ) ) ) ) ).\n\n%------------------------------------------------------------------------------\n% Goal: exists X, Y, Z (Church numerals) such that\n%   X + 5  = 10\n%   X * Y  = 15\n%   Z + Y  = 3\n%------------------------------------------------------------------------------\nthf(conjecture,conjecture,\n    ? [X: ( $i > $i ) > $i > $i, Y: ( $i > $i ) > $i > $i, Z: ( $i > $i ) > $i > $i] :\n      ( ( ( plus @ X @ five ) = ten )\n      & ( ( mult @ X @ Y ) = fifteen )\n      & ( ( plus @ Z @ Y ) = three ) ) ).\n%------------------------------------------------------------------------------"
system_name = "E---3.3.0"
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