Wolfram/Parser | Paclet Repository

Wolfram`Parser`

TPTPExport

TPTPExport [derivation]
	renders an SZS-output derivation Association back to SZS-framed TPTP text — the inverse of TPTPImport [source,"SZS"] .

Details and Options

▪

derivation is an

Association

carrying a

"Derivation"

— a list of step records — and optional

"Status"

"Problem"

, and

"OutputForm"

framing keys. Each step is

Association

[{"Head","Name","Role","Formula","Rule","Status","Parents",…}]

, the record

TPTPImport

returns for each clause in

"SZS"

mode.

▪

The result is a

String

of SZS-framed TPTP text, one clause per line, ending in a newline.

▪

The

%SZSstatus…

line is emitted when

"Status"

is a string; the

%SZSoutputstart…

%SZSoutputend…

markers when

"OutputForm"

is a string.

"Problem"

supplies the trailing problem name and defaults to

unknown

▪

Each step renders as

head(name,role,formula,source).

▪

An inference step re-renders structurally from its

"Rule"

"Status"

, and

"Parents"

fields as

inference(rule,[status(...)],[parents])

; a missing status leaves an empty

[]

▪

Any other source — a

file(...)

axiom, an

introduced(...)

clause — is reproduced verbatim from the step's retained

"RawSource"

. A step with neither an inference rule nor a

"RawSource"

renders with no source annotation.

▪

Formula bodies re-render through the inverse of the

action map:

≠

≤>

<~>

$true

$false

; a String-headed compound

"f"[a,b]

f(a,b)

and a nullary

"c"[]

. A compound subformula of a connective is parenthesized.

▪

A clause body the SZS reader kept as raw source text (one it does not lift to a Wolfram formula) is emitted unchanged.

▪

Round-trip: for a derivation obtained from

TPTPImport

[TPTPExport[derivation],"SZS"]

reproduces it.

Examples

(12)

Basic Examples

(2)

Import a small SZS refutation, then render it back — the framing, the clauses, and the inference records all return:

In[1]:=

szsText="% SZS status Unsatisfiable for GRP001% SZS output start Refutation for GRP001cnf(left_id, axiom, mult(e, X) = X, file('GRP001.p', left_id)).cnf(goal, plain, mult(a, b) = c, inference(superposition, [status(thm)], [left_id])).cnf(bot, plain, $false, inference(cr, [status(thm)], [goal])).% SZS output end Refutation for GRP001";szs=

TPTPImport

[szsText,"SZS"];

TPTPExport

[szs]

Out[1]=

% SZS status Unsatisfiable for GRP001% SZS output start Refutation for GRP001cnf(left_id, axiom, mult(e, X) = X, file('GRP001.p', left_id)).cnf(goal, plain, mult(a, b) = c, inference(superposition, [status(thm)], [left_id])).cnf(bot, plain, $false, inference(cr, [status(thm)], [goal])).% SZS output end Refutation for GRP001