Package Documentation

Grammar

class tptp_lark_parser.grammar.Clause(literals: ~typing.Tuple[~tptp_lark_parser.grammar.Literal, ...], label: str = <factory>, role: str = 'lemma', inference_parents: ~typing.Tuple[str, ...] | None = None, inference_rule: str | None = None, processed: bool | None = None, birth_step: int | None = None)

Clause is a disjunction of literals.

Parameters:

literals – a list of literals, forming the clause
label – comes from the problem file or starts with inferred_ if inferred during the episode
role – formula role: axiom, hypothesis, …
inference_parents – a list of labels from which the clause was inferred. For clauses from the problem statement, this list is empty
inference_rule – the rule according to which the clause was got from the inference_parents
processed – boolean value splitting clauses into unprocessed and processed ones; in the beginning, everything is not processed
birth_step – a number of the step when the clause appeared in the unprocessed set; clauses from the problem have birth_step zero

class tptp_lark_parser.grammar.Function(index: int, arguments: Tuple[Variable | Function, ...]): A functional symbol might be applied to a list of arguments.

class tptp_lark_parser.grammar.Literal(negated: bool, atom: Predicate): Literal is an atom which can be negated or not.

class tptp_lark_parser.grammar.Predicate(index: int, arguments: Tuple[Variable | Function, ...]): A predicate symbol might be applied to a list of arguments.

class tptp_lark_parser.grammar.Variable(index: int): A variable is characterised only by its name.

CNF Parser

class tptp_lark_parser.cnf_parser.CNFParser(tokens_filename: str | None = None, extendable: bool = False)

A parser for <cnf_formula> from Lark parser tree.

Methods are not typed since nobody calls them directly.

>>> import sys
>>> import os
>>> if sys.version_info.major == 3 and sys.version_info.minor >= 9:
...     from importlib.resources import files
... else:
...     from importlib_resources import files
>>> from lark import Lark
>>> lark_parser = Lark(
...     files("tptp_lark_parser")
...     .joinpath(os.path.join("resources", "TPTP.lark"))
...     .read_text(),
...     start="tptp_file"
... )
>>> lark_parsed_tree = lark_parser.parse('''
...    cnf(test, axiom, f(X, g(Y), h(Z, c1)) = f(X, Y, c2)
...    | ~ better(f(X), g(Y)) | $false | this_is_a_test_case,
...    inference(resolution, [], [this, that, third])).
... ''')
>>> cnf_parser = CNFParser()
>>> cnf_parser.token_map["functions"]
{'f': 0}
>>> cnf_parser.transform(lark_parsed_tree)
Traceback (most recent call last):
...
lark.exceptions.VisitError: Error trying to process rule "fof_plain_term":

unknown symbol: g
>>> cnf_parser.extendable = True
>>> clause = cnf_parser.transform(lark_parsed_tree)
>>> print(cnf_parser.pretty_print(clause))
cnf(test, axiom, f(X,g(Y),h(Z,c1)) = f(X,Y,c2) | ~better(f(X), g(Y)) | $false() | this_is_a_test_case(), inference(resolution, [], [this, that, third])).
>>> cnf_parser.token_map
{'functions': {'f': 0, 'g': 1, 'c1': 2, 'h': 3, 'c2': 4, 'better': 5, 'this_is_a_test_case': 6}, 'predicates': {'$false': 0, '=': 1, '!=': 2, 'better': 3, 'this_is_a_test_case': 4}, 'variables': {'X0': 0, 'X1': 1, ..., 'X999': 999, 'X': 1000, 'Y': 1001, 'Z': 1002}}

static annotations(children: List[Any])

Annotation (we care only about inference info from it).

Parameters:: children – parsed tree node’s children

static cnf_annotated(children: List[Any])

Annotated CNF formula (clause).

<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula> <annotations>).

Parameters:: children – parsed tree node’s children

static disjunction(children: List[Any])

Clause structure.

Parameters:: children – parsed tree node’s children

static fof_arguments(children: List[Any])

List of arguments, organised in pairs.

<fof_arguments> ::= <fof_term> | <fof_term>,<fof_arguments>

Parameters:: children – parsed tree node’s children

fof_defined_infix_formula(children: List[Any])

Translate predicates in the infix form to the prefix.

<fof_defined_infix_formula> ::= <fof_term> <defined_infix_pred> <fof_term>

Parameters:: children – parsed tree node’s children

fof_defined_plain_formula(children: List[Any])

Predicate with or without arguments.

<fof_defined_plain_formula> :== <defined_proposition> | <defined_predicate>(<fof_arguments>)

Parameters:: children – parsed tree node’s children

fof_defined_term(children: List[Any])

Another way to describe a functional symbol.

<fof_defined_term> ::= <defined_term> | <fof_defined_atomic_term>

Parameters:: children – parsed tree node’s children

fof_infix_unary(children: List[Any])

Translate predicates in the infix form to the prefix.

<fof_infix_unary> ::= <fof_term> <infix_inequality> <fof_term>

Parameters:: children – parsed tree node’s children

fof_plain_atomic_formula(children: List[Any])

Another way for writing predicates.

<fof_plain_atomic_formula> :== <proposition> | <predicate>(<fof_arguments>)

Parameters:: children – parsed tree node’s children

fof_plain_term(children: List[Any])

Functional symbol with or without (a constant) arguments.

<fof_plain_term> ::= <constant> | <functor>(<fof_arguments>) :param children: parsed tree node’s children

static inference_record(children: List[Any])

Inference record (parents and rule).

<inference_record> :== inference(<inference_rule>,<useful_info>, <inference_parents>)

Parameters:: children – parsed tree node’s children

static literal(children: List[Any])

Literal is a possible negated predicate.

Parameters:: children – parsed tree node’s children

static parent_info(children: List[Any])

Inference parents.

<parent_info> :== <source><parent_details>

Parameters:: children – parsed tree node’s children

static parent_list(children: List[Any])

Inference parents list.

<parent_list> :== <parent_info> | <parent_info>,<parent_list>

Parameters:: children – parsed tree node’s children

pretty_print(clause: Clause) → str

Print a logical formula back to TPTP language.

Parameters:: clause – a logical clause to print
Returns:: a TPTP string

variable(children: List[Any])

Variable (supposed to be universally quantified).

Parameters:: children – parsed tree node’s children

TPTP Parser

class tptp_lark_parser.tptp_parser.TPTPParser(tptp_folder: str = '.', extendable: bool = False, tokens_filename: str | None = '/home/docs/checkouts/readthedocs.org/user_builds/tptp-lark-parser/checkouts/latest/tptp_lark_parser/resources/tptp_tokens.json')

TPTP parser.

>>> tptp_folder = (
...     files("tptp_lark_parser")
...     .joinpath(os.path.join("resources", "TPTP-mock"))
... )
>>> tokens_filename = (
...     files("tptp_lark_parser")
...     .joinpath(os.path.join("resources", "tptp_tokens.json"))
... )
>>> from tptp_lark_parser.grammar import (Literal, Predicate, Variable,
...     Function, EQUALITY_SYMBOL_ID)
>>> tptp_parser = TPTPParser(tptp_folder, True, tokens_filename)
>>> clause = Clause(label="this_is_a_test_case", literals=(Literal(True, Predicate(EQUALITY_SYMBOL_ID, (Function(1, (Variable(1), )), Variable(2)))), Literal(False, Predicate(EQUALITY_SYMBOL_ID, (Function(2, ()), Function(3, ())))), Literal(False, Predicate(3, (Variable(1),)))), inference_rule="resolution", inference_parents=("one", "two"))
>>> (
...     tptp_parser.parse(tptp_parser.cnf_parser.pretty_print(clause))[0]
...     == clause
... )
True
>>> empty_clause = Clause(literals=())
>>> (tptp_parser.parse(
...     tptp_parser.cnf_parser.pretty_print(empty_clause))[0] ==
...     empty_clause)
True
>>> tptp_text = (
...     files("tptp_lark_parser")
...     .joinpath(os.path.join(
...         "resources", "TPTP-mock", "Problems", "TST", "TST001-1.p"
...     ))
...     .read_text()
... )
>>> parsed_clauses = tptp_parser.parse(tptp_text)
>>> print(
...     "\n".join(map(tptp_parser.cnf_parser.pretty_print, parsed_clauses))
... )
cnf(this_is_a_test_case_1, hypothesis, this_is_a_test_case(test_constant), inference(resolution, [], [one, two])).
cnf(this_is_a_test_case_2, hypothesis, ~this_is_a_test_case(test_constant)).
cnf(test_axiom, axiom, test_constant = test_constant_2).
cnf(test_axiom_2, axiom, ~test_constant = 0).

parse(tptp_text: str) → Tuple[Clause, ...]

Recursively parse a string containing a TPTP problem.

Parameters:: tptp_text – a name of a problem (or axioms) file
Returns:: a list of clauses (including those of the axioms)