TPTP/THF Syntax and Pretty-Printing

Intro

This notebook showcases the bundled TPTP/THF-style notation for higher-order logic. Livebook sends ordinary Isabelle theory text through check_text; the support theory provides syntax bundles for parsing and printing THF-like formulas.

Behind the scenes:

• priv/isabelle/tptp/TPTP.thy defines the THF notation bundles and the explicit application operator @
• IsabelleClient.TPTP.load/1 copies that theory into an existing Isabelle session and checks it there

This is not a full TPTP frontend. It is a lightweight bridge for writing Isabelle theories with THF-style syntax, inspecting THF-style pretty output, and converting a small subset of annotated THF formulae.

In particular, we deviate from the THF “standard” in allowing untyped terms, ML-style schematic type variables (as in 'a > 'b) instead of type quantifiers (which are not supported), and the infix application operator @ can be omitted (optionally).

When using the published package, replace the dependency with {:isabelle_elixir, "~> 0.3"}.

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

Start Isabelle

#System.put_env("ISABELLE_TOOL", "path/to/isabelle/executable") # optionally, if needed
IsabelleClient.Server.executable()

{:ok, server} =
  IsabelleClient.start_server(
    server_name: "livebook_tptp_#{System.unique_integer([:positive])}"
  )

{:ok, client} = IsabelleClient.connect(server)

Start the Session

tptp_import = "TPTP"

%{
  import: tptp_import,
  source: IsabelleClient.TPTP.source_path()
}

{:ok, client, start_task} =
  IsabelleClient.start_session(
    client,
    [session: "HOL", verbose: true],
    120_000
  )

{:ok, tptp_task} = IsabelleClient.TPTP.load(client, 120_000)

%{
  session_id: IsabelleClient.active_session(client).id,
  start_messages: IsabelleClient.messages(start_task),
  tptp_messages: IsabelleClient.messages(tptp_task)
}

Checking Examples

IsabelleClient.TPTP.check/5 checks a small Isabelle theory body and returns only the relevant Isabelle messages. The from:, to:, and show_thf_app: options keep the examples focused on the problem text: the function activates the corresponding Isabelle notation before the body and deactivates it afterwards.

From TPTP to Isabelle

IsabelleClient.TPTP.check/5 takes a client, import name, theory name, and theory body, then invokes IsabelleClient.check_text/5 under the hood. Additionally, the option from: true wraps the body in unbundle from_TPTP ... unbundle no from_TPTP, in order to activate the TPTP -> Isabelle translation (and deactivate it afterwards). The option show_thf_app: false deactivates the explicit infix application notation @ (which is mostly useful for the Isabelle -> TPTP direction).

IsabelleClient.TPTP.check(client, tptp_import, "TPTPSyllogism", ~S"""
typedecl entity
consts human :: "entity > $o"
consts mortal :: "entity > $o"
consts socrates :: entity

lemma mortal_socrates:
  "(! [x::entity] : (human @ x) => (mortal @ x))
    => (human @ socrates)
    => (mortal @ socrates)"
  unfolding thf_app_def
  by blast
""", from: true, show_thf_app: false)
|> IO.puts()

Characteristic functions give a compact encoding of sets. This example defines union with THF notation and proves commutativity.

IsabelleClient.TPTP.check(client, tptp_import, "TPTPSetUnion", ~S"""
typedecl elem
type_synonym eset = "elem > $o"

definition union :: "eset > eset > eset" where
  "union = (^ [A::eset, B::eset, x::elem] : (A @ x) | (B @ x))"

lemma union_comm:
  "! [A::eset, B::eset, x::elem] :
      ((union @ A @ B @ x) <=> (union @ B @ A @ x))"
  unfolding union_def thf_app_def
  by blast
""", from: true, show_thf_app: false)
|> IO.puts()

To TPTP from Isabelle

unbundle to_TPTP changes output notation. show_thf_app controls whether ordinary function application is printed with explicit @. This cell toggles show_thf_app inside the body for comparing both translation styles.

IsabelleClient.TPTP.check(client, tptp_import, "TPTPPrettyPrint", ~S"""
declare [[show_types = true, show_abbrevs = true]]

typedecl elem

declare [[show_thf_app = true]]
term "\<lambda>(A::elem \<Rightarrow> bool) x. A x"

declare [[show_thf_app = false]]
term "\<lambda>(A::elem \<Rightarrow> bool) x. A x"
""", to: true)
|> IO.puts()

Round Trip: TPTP - Isabelle

Both translations can be active at once: Isabelle parses THF-style input and prints the resulting term back in THF style. Note that below we are getting type inference for A and B for free. Here from: true enables parsing, to: true enables THF-style printing, and show_thf_app: true asks the printer to expose application as @.

IsabelleClient.TPTP.check(client, tptp_import, "TPTPRoundTrip", ~S"""
declare [[show_types = true, show_abbrevs = true]]

term "! [A, B] :
        (? [x::$i] : (A @ x) & ~(B @ x))
        => ~(! [x::$i] : (A @ x) => (B @ x))"
""", from: true, to: true, show_thf_app: true)
|> IO.puts()

Annotated THF Formulae

IsabelleClient.TPTP.isabellize_theory/1 accepts a small THF/TPTP fragment and turns supported annotated formulae of the form thf(name, role, formula, metadata). into Isabelle theory commands. It preserves THF formulas as text; use it together with from: true so the from_TPTP bundle parses those formulas.

Supported annotated formulae are intentionally minimal:

• thf(name, type, (T: $tType)). becomes typedecl T
• thf(name, type, (c: T)). becomes consts c :: "T"
• thf(name, type, (alias: old = new)). becomes type_synonym alias = "new"
• thf(name, axiom, formula, file(...), [simp]). becomes axiomatization where name[simp]: "formula"
• thf(name, theorem/conjecture, formula). becomes lemma name: "formula"
• include('path/file.ext'). becomes imports "path/file"

Metadata is allowed to be any comma-separated list of TPTP terms after the formula, including nested commas such as file('x.p', name) or inference(rule, [], [a,b]). The converter does not interpret or filter metadata values. If a metadata argument is already a bracketed Isabelle attribute list, its contents are copied verbatim to the generated declaration; metadata outside that bracket-list shape, such as file(...), is ignored. TPTP comments are preserved as Isabelle comments: % ... and /* ... */ become (* ... *).

Include directives are intentionally simple-minded: the first path argument is unquoted, its final extension is removed, and any optional selection list is ignored. The resulting imports line belongs in an Isabelle theory header, so the following example is printed rather than passed to check_text as a theory body fragment.

include_demo = ~S"""
include('Axioms/SET001.ax').
include('Problems/PUZ001+0.p', [agatha, butler]).
"""

IO.puts(IsabelleClient.TPTP.isabellize_theory(include_demo))

Converted lemmas are proof obligations. Add a proof after them, or close them with oops when you only want to parse and inspect the generated Isabelle text.

annotated_tptp = ~S"""
% Type constants, type aliases, and term constants.
thf(type_entity,type,(entity: $tType), file('example.p', type_entity)).
thf(type_predicate,type,(predicate: entity > $o = entity > $o), introduced(local)).
thf(type_human,type,(human: entity > $o), [description('predicate')]).
thf(type_socrates,type,(socrates: entity), [description('constant')]).

% The bracketed metadata list is passed through as Isabelle attributes.
thf(ax_human_self,axiom,
  (! [X: entity] : (human @ X) => (human @ X)),
  file('example.p', ax_human_self),
  [simp]).

thf(conj_some_human,conjecture,
  (? [X: entity] : (human @ X)),
  inference(copy, [], [ax_human_self]),
  []).
"""

isabelle_fragment = IsabelleClient.TPTP.isabellize_theory(annotated_tptp)
IO.puts(isabelle_fragment)

The generated conjecture is a lemma, so this parse-only example closes it with oops.

IsabelleClient.TPTP.check(
  client,
  tptp_import,
  "TPTPAnnotatedFormulae",
  isabelle_fragment <> "\noops",
  from: true,
  show_thf_app: false
)
|> IO.puts()

For converted theorem formulae, append the proof that should discharge the generated lemma.

annotated_theorem = ~S"""
thf(type_person,type,(person: $tType)).
thf(type_good,type,(good: person > $o)).
thf(type_alice,type,(alice: person)).

thf(ax_good_self,axiom,
  ((good @ alice) => (good @ alice)),
  file('example.p', ax_good_self),
  [simp]).

thf(thm_good_self,theorem,
  ((good @ alice) => (good @ alice)),
  inference(copy, [], [ax_good_self]),
  [intro]).
"""

proved_fragment =
  IsabelleClient.TPTP.isabellize_theory(annotated_theorem) <> "\nby simp"

IsabelleClient.TPTP.check(
  client,
  tptp_import,
  "TPTPAnnotatedTheorem",
  proved_fragment,
  from: true,
  show_thf_app: false
)
|> IO.puts()

The metadata pass-through is shape-based, not name-based. This example is only printed, because arbitrary attribute names must still be meaningful to Isabelle if you later check the generated text.

metadata_shape_demo = ~S"""
thf(ax_attrs,axiom,
  ($true),
  file('ignored.p', ax_attrs),
  [foo, bar(baz, qux), simp]).
"""

IO.puts(IsabelleClient.TPTP.isabellize_theory(metadata_shape_demo))

Who Killed Agatha?

The classic TPTP problem PUZ001+1.p is a first-order puzzle: someone in Dreadbury Mansion killed Agatha, and the axioms imply that Agatha killed herself.

The original problem is FOF. Here we write the same formulas in the bundled THF-style notation: $i for individuals, $o for propositions, !/? for quantifiers, and @ for explicit application.

agatha_problem = ~S"""
consts agatha :: "$i"
consts butler :: "$i"
consts charles :: "$i"
consts lives :: "$i > $o"
consts killed :: "$i > $i > $o"
consts hates :: "$i > $i > $o"
consts richer :: "$i > $i > $o"

lemma agatha_killed_herself:
  assumes "? [X :: $i] : (lives @ X) & (killed @ X @ agatha)"
    and "lives @ agatha"
    and "lives @ butler"
    and "lives @ charles"
    and "! [X :: $i] : (lives @ X) => ((X = agatha) | (X = butler) | (X = charles))"
    and "! [X :: $i, Y :: $i] : (killed @ X @ Y) => (hates @ X @ Y)"
    and "! [X :: $i, Y :: $i] : (killed @ X @ Y) => ~(richer @ X @ Y)"
    and "! [X :: $i] : (hates @ agatha @ X) => ~(hates @ charles @ X)"
    and "! [X :: $i] : (X != butler) => (hates @ agatha @ X)"
    and "! [X :: $i] : ~(richer @ X @ agatha) => (hates @ butler @ X)"
    and "! [X :: $i] : (hates @ agatha @ X) => (hates @ butler @ X)"
    and "! [X :: $i] : (? [Y :: $i] : ~(hates @ X @ Y))"
    and "agatha != butler"
  shows "killed @ agatha @ agatha"
  using assms unfolding thf_app_def
  __PROOF__
"""

Ask Isabelle which basic proof method works. The longer timeout is only for try0, which runs a small portfolio of methods.

IsabelleClient.TPTP.check(
  client,
  tptp_import,
  "AgathaTry0",
  String.replace(agatha_problem, "__PROOF__", "try0 oops"),
  from: true,
  show_thf_app: false,
  timeout: 120_000
)
|> IO.puts()

try0 suggests metis, so the theorem checks directly.

IsabelleClient.TPTP.check(
  client,
  tptp_import,
  "AgathaMetis",
  String.replace(agatha_problem, "__PROOF__", "by metis"),
  from: true,
  show_thf_app: false,
  timeout: 120_000
)
|> IO.puts()

Stop and Shutdown

{:ok, client, stop_task} = IsabelleClient.stop_session(client, 120_000)

%{
  remaining_sessions: client.sessions,
  messages: IsabelleClient.messages(stop_task)
}

IsabelleClient.shutdown_server(client)