# TPTP/THF Syntax and Pretty-Printing
## Intro
This notebook showcases the bundled [TPTP/THF-style notation](https://page.mi.fu-berlin.de/cbenzmueller/papers/C25.pdf) 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).
<!-- livebook:{"break_markdown":true} -->
When using the published package, replace the dependency with `{:isabelle_elixir, "~> 0.3"}`.
```elixir
Mix.install([
{:isabelle_elixir, path: Path.expand("..", __DIR__)}
])
```
## Start Isabelle
```elixir
#System.put_env("ISABELLE_TOOL", "path/to/isabelle/executable") # optionally, if needed
IsabelleClient.Server.executable()
```
```elixir
{:ok, server} =
IsabelleClient.start_server(
server_name: "livebook_tptp_#{System.unique_integer([:positive])}"
)
{:ok, client} = IsabelleClient.connect(server)
```
## Start the Session
```elixir
tptp_import = "TPTP"
%{
import: tptp_import,
source: IsabelleClient.TPTP.source_path()
}
```
```elixir
{: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).
```elixir
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.
```elixir
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.
```elixir
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 `@`.
```elixir
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.
```elixir
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.
```elixir
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`.
```elixir
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`.
```elixir
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.
```elixir
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`](https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=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.
```elixir
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.
```elixir
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.
```elixir
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
```elixir
{:ok, client, stop_task} = IsabelleClient.stop_session(client, 120_000)
%{
remaining_sessions: client.sessions,
messages: IsabelleClient.messages(stop_task)
}
```
```elixir
IsabelleClient.shutdown_server(client)
```