Wolfram/Parser | Paclet Repository

Wolfram`Parser`

TPTPImport

TPTPImport [ File [path]]
	parses a TPTP (Thousands of Problems for Theorem Provers) problem file into an Association of its axioms and conjecture.

TPTPImport [source]
	parses TPTP source given directly as a string.

TPTPImport [source,"SZS"]
	reads an SZS-output derivation instead, returning its status and proof steps.

Details and Options

▪

The default result partitions the problem into

"Axioms"

— the formulas of the

axiom

and

hypothesis

clauses — and

"Conjecture"

, the goal of a

conjecture

clause, or a

negated_conjecture

flipped through

Not

so the returned goal is positive, or

None

when there is none.

▪

Function and predicate symbols return as String-headed compounds:

"multiply"[x,y]

"p"[x]

, a constant as

"c"[]

. A parsed symbol therefore cannot collide with a Wolfram Language binding, and an equational atom stays symbolic instead of eagerly evaluating.

▪

Variables return as

Pattern

[name,

Blank

[]]

, rendering as

▪

Quantifiers

and

lift to

ForAll

and

Exists

; the Boolean connectives to

, and

; the equational atoms

and

≠

Equal

and

Unequal

▪

The clause heads

cnf

fof

, and

thf

lift to Wolfram Language formulas;

tff

and

tcf

clauses are recognized and partitioned but their formula bodies may come back as the raw parse tree; a

tpi

clause is skipped.

▪

THF connectives (

≤>

, …) are parsed through

ParseOperatorTable

, which stays linear where an ordered-choice cascade over the shared operand would backtrack exponentially.

▪

The top-level universal quantifier of a clause is dropped — a clause is read under its implicit universal closure — while inner quantifiers are kept.

▪

$true

and

$false

map to

True

and

False

; other

-defined atoms keep their token (

$sum

$distinct

▪

include('path')

directives resolve recursively against the directory of the including file, then the

$TPTP

and

$TPTP/Problems

environment roots. A selector

include('path',[a,b])

admits only the named clauses.

▪

"SZS"

mode the

"Derivation"

value is a list of step records

Association

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

; this mode is the inverse of

TPTPExport

▪

The parser is built once per kernel session by

EBNFParse

from the published TPTPWorld

SyntaxBNF

grammar plus an action map; the grammar is fetched on the first call.

Examples

(23)

Basic Examples

(4)

Import a small first-order (

fof

) formula; the propositional axiom

p=>q

lifts to

Implies

In[1]:=

TPTPImport

["fof(a, axiom, p => q)."]

Out[1]=

$Failed

_________________________________________________________________________________________________________________

Predicate and function symbols return as String-headed compounds and variables as

; the implicit top-level universal quantifier is dropped:

In[1]:=

TPTPImport

["fof(comm, axiom, ! [X, Y] : mult(X, Y) = mult(Y, X))."]

Out[1]=

$Failed

_________________________________________________________________________________________________________________

A clause-normal-form (

cnf

) axiom lifts the same way:

In[1]:=

TPTPImport

["cnf(a, axiom, and(X, Y) = and(Y, X))."]

Out[1]=

$Failed

_________________________________________________________________________________________________________________

conjecture

clause lands in the

"Conjecture"

slot instead of

"Axioms"

In[1]:=

TPTPImport

["fof(goal, conjecture, ! [X] : p(X))."]

Out[1]=

$Failed

Scope

(11)



Properties & Relations

(5)



Possible Issues

(2)



Neat Examples

(1)



SeeAlso

▪

▪

▪

▪

RelatedGuides

▪

WolframParser