Loge: TPTP smoke test

root = Path.expand("..", __DIR__)

Mix.install([
  {:loge, path: Path.join(root, "loge"), override: true},
  {:loge_tptp, path: Path.join(root, "loge_tptp")},
  {:kino_loge, path: Path.join(root, "kino_loge")}
])

Settings

Nothing to set for SystemOnTPTP. To try another engine, fill in its fields and press Verify; a password field takes the name of a Livebook secret, not the password.

:ok

Definitions

A Logic Engine cell with no engine, bound to set_theory. Later cells include it by name.

set_theory =
  Loge.source(
    :tptp,
    "fof(subset, axiom, ![A, B]: (subset(A, B) <=> ![X]: (member(X, A) => member(X, B)))).\nfof(equal_set, axiom, ![A, B]: (equal_set(A, B) <=> (subset(A, B) & subset(B, A)))).\nfof(intersection, axiom, ![X, A, B]: (member(X, intersection(A, B)) <=> (member(X, A) & member(X, B)))).\nfof(union, axiom, ![X, A, B]: (member(X, union(A, B)) <=> (member(X, A) | member(X, B))))."
  )

Including a cell

Expected: Theorem. Edit the definitions above and this cell turns stale.

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('set_theory').\n\nfof(intersection_commutes, conjecture,\n    ![A, B]: equal_set(intersection(A, B), intersection(B, A))).",
  system: "E",
  time_limit_sec: 10,
  includes: %{"set_theory" => set_theory}
)

A selection includes only the named formulae. Expected: Theorem.

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('set_theory', [subset, union]).\n\nfof(union_upper_bound, conjecture, ![A, B]: subset(A, union(A, B))).",
  system: "E",
  time_limit_sec: 10,
  includes: %{"set_theory" => set_theory}
)

Including the TPTP library

A name that is not a cell is fetched from tptp.org (cached under ~/.cache/tptp). Expected: Theorem.

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('Axioms/SET006+0.ax').\n\nfof(power_set_of_subset, conjecture,\n    ![A, B]: (subset(A, B) => subset(power_set(A), power_set(B)))).",
  system: "E",
  time_limit_sec: 10
)

A false conjecture

Expected: CounterSatisfiable (or GaveUp/Timeout, depending on the system).

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('set_theory').\n\nfof(union_is_intersection, conjecture,\n    ![A, B]: equal_set(union(A, B), intersection(A, B))).",
  system: "Vampire",
  time_limit_sec: 10,
  includes: %{"set_theory" => set_theory}
)

Diagnostics

The list under the editor should show: no_such_cell cannot be resolved (line 2), subset names two statements (line 4, the first one is inside set_theory), the unfinished last statement (line 5), and, on the include of set_theory, that it has no conjecture. Evaluating fails with undefined variable "no_such_cell": an include that names a variable is a reference to it.

Loge.run!(
  Loge.Tptp.Engines.SystemOnTptp,
  "include('set_theory').\ninclude('no_such_cell').\n\nfof(subset, axiom, $true).\nfof(unfinished, conjecture, ![A]: subset(A, A)",
  system: "E",
  time_limit_sec: 10,
  includes: %{"set_theory" => set_theory, "no_such_cell" => no_such_cell}
)