unicode_fol_kit.parse_prover9

unicode_fol_kit.parse_prover9(text)

Parse a single Prover9-syntax formula into a toolkit Node.

A trailing period (Prover9 terminates each formula with .) is accepted and ignored.

Parameters:

text (str) – a Prover9 formula, e.g. "(all X (man(X) -> mortal(X)))".

Returns:

The formula as a toolkit Node.

Raises:

Prover9ParsingError – if text is not a well-formed Prover9 formula.

Return type:

Node