API Documentation#

Saturation Prover#

class yapsap.yapsa_prover.YapsaProver(problem: str)#

Saturation algorithm defined in a Reinforcement Learning friendly way.

>>> import sys
>>> if sys.version_info.major == 3 and sys.version_info.minor >= 9:
...     from importlib.resources import files
... else:
...     from importlib_resources import files
>>> tptp_folder = files("yapsap").joinpath(
...     os.path.join("resources", "TPTP-mock")
... )
>>> problem = os.path.join(tptp_folder, "Problems", "TST", "TST001-1.p")
>>> from random import choice
>>> class RandomProver(YapsaProver):
...     def proof_attempt(self) -> None:
...         while not self.proof_found:
...             self._step(choice(list(self.state.keys())))
...
>>> prover = RandomProver(problem)
>>> len(prover.state)
4

>>> from random import seed
>>> seed(0)
>>> prover.proof_attempt()
>>> print(len(prover.state))
161

__init__(problem: str)#

Initialise spaces et al.

Parameters:: problem – a list of the names of TPTP problem files

proof_attempt() → None#: Try finding a proof.

property proof_found: bool#: Return whether there is an empty clause in the state.

Factoring#

yapsap.factoring.all_possible_factors(given_clause: Clause) → Tuple[Clause, ...]#

One of the four basic building blocks of the Given Clause algorithm.

>>> from tptp_lark_parser.tptp_parser import TPTPParser
>>> parser = TPTPParser()
>>> clause = parser.parse("cnf(one, axiom, p(c) | p(X) | q).")[0]
>>> tuple(map(
...     parser.cnf_parser.pretty_print,
...     all_possible_factors(clause)
... ))
('cnf(x..., lemma, q() | p(c), inference(factoring, [], [one])).',)

Parameters:: given_clause – a new clause which should be combined with all the processed ones
Returns:: results of all possible factors with each one from clauses and the given_clause

yapsap.factoring.factoring(given_clause: Clause, literal_one: Literal, literal_two: Literal) → Clause#

Apply positive factoring rule.

\[{\frac{C\vee A_1\vee A_2}{\sigma\left(C\vee L_1\right)}}\]

where

\(C\) and is a clause
\(A_1\) and \(A_2\) are atomic formulae (positive literals)
\(\sigma\) is a most general unifier of \(A_1\) and \(A_2\)

>>> from tptp_lark_parser.grammar import Predicate, Variable, Function
>>> from pprint import pprint
>>> pprint(factoring(
...     gram.Clause((gram.Literal(True, Predicate(8, (Variable(0),))),)),
...     gram.Literal(False, Predicate(9, (Variable(0),))),
...     gram.Literal(False, Predicate(9, (Function(0, ()),)))
... ).literals, width=75)
(Literal(negated=True,
         atom=Predicate(index=8,
                        arguments=(Function(index=0, arguments=()),))),
 Literal(negated=False,
         atom=Predicate(index=9,
                        arguments=(Function(index=0, arguments=()),))))
>>> factoring(
...     gram.Clause(()), gram.Literal(False, Predicate(8, ())),
...     gram.Literal(True, Predicate(7, ()))
... )
Traceback (most recent call last):
 ...
ValueError: factoring is not possible for Literal(negated=False, atom=P...

Parameters:

given_clause – \(C\)
literal_one – \(A_1\)
literal_two – \(A_2\)

Returns:

a new clause — the factoring result

Raises:

ValueError – if literal_one or literal_two is negated

Paramodulation#

yapsap.paramodulation.all_paramodulants_from_clause(clause_one: Clause, literal_one: Literal, clause_two: Clause, literal_two: Literal) → Tuple[Clause, ...]#

Apply paramodulation with varying r_position argument.

Also varies for equality symmetry

Parameters:

clause_one – \(C_1\)
literal_one – \(s\approx t\)
clause_two – \(C_2\)
literal_two – \(L\left[r\right]\)

Returns:

a list of paramodulants for all possible values of r_position

Raises:

ValueError – if literal_one is not an equality

yapsap.paramodulation.all_paramodulants_from_list(clauses: Tuple[Clause, ...], given_clause: Clause) → Tuple[Clause, ...]#

One of the four basic building block of the Given Clause algorithm.

>>> from tptp_lark_parser.grammar import Literal, Function, Predicate
>>> all_paramodulants_from_list(
...     (Clause(
...         (Literal(
...             False,
...             Predicate(EQUALITY_SYMBOL_ID, (Function(1, ()),))),
...         ),
...         "one"
...     ),),
...     Clause((Literal(True, Predicate(3, ())),), "two")
... )
Traceback (most recent call last):
 ...
ValueError: expected equality, but got Literal(negated=False, ...)
>>> from tptp_lark_parser.tptp_parser import TPTPParser
>>> parser = TPTPParser()
>>> one = parser.parse("cnf(one, axiom, a=b | X=X).")[0]
>>> two = parser.parse("cnf(two, axiom, b=c).")[0]
>>> res = all_paramodulants_from_list((one,), two)
>>> print(len(res))
6

Parameters:

clauses – a list of (processed) clauses
given_clause – a new clause which should be combined with all the processed ones

Returns:

results of all possible paramodulants with each one from clauses and the given_clause

yapsap.paramodulation.paramodulation(clause_one: Clause, literal_one: Tuple[Variable | Function, Variable | Function], clause_two: Clause, literal_two: Literal, r_position: int) → Clause#

Apply the binary paramodulation rule.

\[{\frac{C_1\vee s\approx t,C_2\vee L\left[r\right]}{\sigma\left(L\left[t\right]\vee C_1\vee C_2\right)}}\]

where

\(C_1\) and \(C_2\) are clauses with no common variables
\(L\left[r\right]\) is a literal with a sub-term \(r\)
only one instance of \(r\) in \(L\left[r\right]\) is considered,
even if there are many of them
\(s\) and \(t\) are terms, \(\approx\) is a syntactic
equality symbol
\(\sigma\) is a most general unifier of \(s\) and \(r\)

>>> from tptp_lark_parser.grammar import Predicate, Variable, Function
>>> res = paramodulation(
...     Clause((Literal(False, Predicate(8, (Variable(0),))),)),
...     (Variable(0), Function(7, ())),
...     Clause((Literal(False, Predicate(9, (Variable(0),))),)),
...     Literal(True, Predicate(10, (Function(0, ()),))),
...     1
... ).literals
>>> from pprint import pprint
>>> pprint(list(sorted(map(str, res))), width=75)
['Literal(negated=False, atom=Predicate(index=8, '
 'arguments=(Function(index=0, arguments=()),)))',
 'Literal(negated=False, atom=Predicate(index=9, '
 'arguments=(Function(index=0, arguments=()),)))',
 'Literal(negated=True, atom=Predicate(index=10, '
 'arguments=(Function(index=7, arguments=()),)))']

Parameters:

clause_one – \(C_1\)
literal_one – \(s\approx t\)
clause_two – \(C_2\)
literal_two – \(L\left[r\right]\)
r_position – index of \(r\) in the tree of sub-terms of \(L\left[r\right]\)

Returns:

a new clause — the paramodulation result

Reflexivity Resolution#

yapsap.reflexivity_resolution.all_possible_reflexivity_resolvents(given_clause: Clause) → Tuple[Clause, ...]#

One of the four basic building blocks of the Given Clause algorithm.

>>> from tptp_lark_parser.tptp_parser import TPTPParser
>>> parser = TPTPParser()
>>> clause = parser.parse("cnf(test, axiom, p(X) | ~ X=a | b != a).")[0]
>>> from pprint import pprint
>>> pprint(tuple(map(
...     parser.cnf_parser.pretty_print,
...     all_possible_reflexivity_resolvents(clause)
... )), width=75)
('cnf(x..., lemma, p(a) | ~b = a, '
 'inference(reflexivity_resolution, [], [test])).',)

Parameters:: given_clause – a new clause which should be combined with all the processed ones
Returns:: results of all possible reflexivity resolvents with each one from clauses and the given_clause

yapsap.reflexivity_resolution.reflexivity_resolution(given_clause: Clause, a_literal: Tuple[Variable | Function, Variable | Function]) → Clause#

Apply reflexivity resolution rule.

\[\frac{C\vee s\not\approx t}{\sigma\left(C\right)}\]

where

\(C\) and is a clause
\(s\) and \(t\) are terms, \(\not\approx\) is a negation of equality
\(\sigma\) is a most general unifier of \(s\) and \(t\)

>>> from pprint import pprint
>>> from tptp_lark_parser.grammar import Predicate, Variable, Function
>>> pprint(reflexivity_resolution(grammar.Clause((grammar.Literal(True,
...     Predicate(7, (Variable(0),))),)), (Variable(0), Function(0, ()))
...     ).literals, width=75)
(Literal(negated=True,
         atom=Predicate(index=7,
                        arguments=(Function(index=0, arguments=()),))),)

Parameters:

given_clause – \(C\)
a_literal – \(s\not\approx t\)

Returns:

a new clause — the reflexivity resolution result

Resolution#

yapsap.resolution.all_possible_resolvents(clauses: Tuple[Clause, ...], given_clause: Clause) → Tuple[Clause, ...]#

One of the four basic building blocks of the Given Clause algorithm.

>>> from tptp_lark_parser.tptp_parser import TPTPParser
>>> parser = TPTPParser()
>>> one = parser.parse("cnf(one, axiom, q(X) | p(X)).")[0]
>>> two = parser.parse("cnf(two, axiom, ~p(c)).")[0]
>>> tuple(map(
...      parser.cnf_parser.pretty_print,
...      all_possible_resolvents((one,), two)
... ))
('cnf(x..., lemma, q(c), inference(resolution, [], [one, two])).',)

Parameters:

clauses – a list of (processed) clauses
given_clause – a new clause which should be combined with all the processed ones

Returns:

results of all possible resolvents with each one from clauses and the given_clause

yapsap.resolution.resolution(clause_one: Clause, literal_one: Literal, clause_two: Clause, literal_two: Literal) → Clause#

Do inference according to the standard first-order resolution rule.

\[{\frac{C_1\vee L_1,C_2\vee L_2}{\sigma\left(C_1\vee C_2\right)}}\]

where

\(C_1\) and \(C_2\) are clauses with no common variables
\(L_1\) and \(L_2\) are literals (one negated and one not)
\(\sigma\) is a most general unifier of atoms from \(L_1\) and
\(L_2\)

>>> from tptp_lark_parser.grammar import Predicate, Variable, Function
>>> from pprint import pprint
>>> pprint(resolution(
...     Clause((Literal(False, Predicate(4, (Variable(0),))),)),
...     Literal(False, Predicate(3, (Variable(0),))),
...     Clause((Literal(False, Predicate(5, (Variable(0),))),)),
...     Literal(True, Predicate(3, (Function(1, ()),)))
... ).literals, width=75)
(Literal(negated=False,
         atom=Predicate(index=4,
                        arguments=(Function(index=1, arguments=()),))),
 Literal(negated=False,
         atom=Predicate(index=5,
                        arguments=(Function(index=1, arguments=()),))))
>>> resolution(
...     Clause(()), Literal(False, Predicate(8, ())),
...     Clause(()), Literal(False, Predicate(7, ()))
... )
Traceback (most recent call last):
 ...
ValueError: resolution is not possible for Literal(negated=False, atom=...

Parameters:

clause_one – \(C_1\)
literal_one – \(L_1\)
clause_two – \(C_2\)
literal_two – \(L_2\)

Returns:

a new clause — the resolution result

Raises:

ValueError – if both literal_one and literal_two are negated or non-negated

Substitution#

class yapsap.substitution.Substitution(variable: Variable, term: Variable | Function)#

A mapping from Variable to Term.

>>> substitution = Substitution(
...     grammar.Variable(0), grammar.Function(2, ())
... )
>>> from pprint import pprint
>>> pprint(substitution(
...     grammar.Clause((
...         grammar.Literal(
...             False,
...             grammar.Predicate(
...                 3,
...                 (grammar.Function(1, (grammar.Variable(0),)),))
...             ),
...     ), label="test")
... ).literals[0].atom, width=75)
Predicate(index=3,
          arguments=(Function(index=1,
                              arguments=(Function(index=2,
                                                  arguments=()),)),))
>>> substitution(grammar.Variable(0))
Function(index=2, arguments=())

Apply a substitution to a given target clause.

Parameters:: target – a clause to which to apply the substitution

__init__(variable: Variable, term: Variable | Function) → None#

substitute_in_clause(clause: Clause) → Clause#

Apply the substitution to something which is known to be a Clause.

Parameters:: clause – a clause to apply substitution to
Returns:: the result of the substitution

Unification#

exception yapsap.unification.NonUnifiableError#: Exception raised when terms are not unifiable.

yapsap.unification.most_general_unifier(propositions: Tuple[Predicate | Variable | Function, ...], substitutions: Tuple[Substitution, ...] | None = None) → Tuple[Substitution, ...]#

Follow the Robinson’s 1965 unification algorithm.

>>> most_general_unifier((Variable(0), Variable(0)))
()
>>> most_general_unifier((Variable(0), Function(7, (Variable(0),))))
Traceback (most recent call last):
 ...
yapsap.unification.NonUnifiableError: (Variable(index=...
>>> from pprint import pprint
>>> pprint(most_general_unifier((
...     Predicate(
...         8, (Variable(0), Variable(1), Function(0, (Variable(2),)))
...     ),
...     Predicate(8,
...         (
...            Variable(4),
...            Function(7, (Variable(5), Variable(5))),
...            Variable(5)
...         )
...     )
... )), width=75)
(Substitution(variable=Variable(index=0), term=Variable(index=4)),
 Substitution(variable=Variable(index=1),
              term=Function(index=7,
                            arguments=(Variable(index=5),
                                       Variable(index=5)))),
 Substitution(variable=Variable(index=5),
              term=Function(index=0, arguments=(Variable(index=2),))))

Parameters:

propositions – a set of propositions to unify
substitutions – this function is recursive and uses this param to accumulate its output

Returns:

a map from variables to functions or other variables (aka substitution)

Logic Operations Utility Functions#

exception yapsap.utils.NoSubtermFound#: Sometimes a sub-term index is larger than term length.

exception yapsap.utils.TermSelfReplace#: An exception raised when trying to replace a sub-term with itself.

yapsap.utils.clause_length(clause: dict) → int#

Find the length of arguments of each predicate.

Negation adds one to each literal.

Parameters:: clause – a clause in JSON representation
Returns:: structural length of a clause

>>> from tptp_lark_parser.grammar import Literal
>>> import orjson
>>> clause_length(orjson.loads(orjson.dumps(
...     Clause((Literal(True, Predicate("p", (Function("f", ()),))),))
... )))
3

yapsap.utils.get_variable_list(clause: Clause | Predicate | Variable | Function) → Tuple[Variable, ...]#

Find all variables present in a clause.

>>> from tptp_lark_parser.grammar import Literal
>>> get_variable_list(Clause((Literal(False,
...     Predicate(0, (Function(0, (Variable(0), Variable(0))),))
... ),)))
(Variable(index=0), Variable(index=0))

Parameters:: clause – a clause
Returns:: a list (with repetitions) of variables from there clause

yapsap.utils.is_subproposition(one: Predicate | Variable | Function, two: Predicate | Variable | Function) → bool#

Check whether proposition one is part of a proposition two.

Parameters:

one – presumably shorter proposition which is probably a part
two – presumably longer proposition which is probably the whole

Returns:

whether one is a part of two

yapsap.utils.is_tautology(clause: Clause) → bool#

Check whether there are two literals (negated and not) with the same atom.

>>> from tptp_lark_parser.grammar import Literal
>>> is_tautology(Clause((Literal(False, Predicate(7, ())),)))
False
>>> is_tautology(Clause(
...     (Literal(False, Predicate(7, ())), Literal(True, Predicate(7, ())))
... ))
True
>>> is_tautology(Clause(
...     (Literal(False, Predicate(1, (Variable(0), Variable(0)))),)
... ))
True

Parameters:: clause – a clause to check
Returns:: whether the clause is a primitive tautology or not

yapsap.utils.proposition_length(proposition: Predicate | Variable | Function) → int#

Find the number of functional, predicate and variable symbols.

Parameters:: proposition – a function, a predicate or a variable
Returns:: structural length of a proposition

>>> proposition_length(Predicate(7, (Function(0, (Variable(0),)),)))
3

yapsap.utils.reindex_variables(clauses: Dict[str, Clause]) → Dict[str, Clause]#

Rename variables so that each clause has its unique set of variables.

>>> from tptp_lark_parser.grammar import Literal
>>> clause = Clause((Literal(False,
...     Predicate(0, (Variable(2), Variable(1), Variable(0)))
... ),))
>>> sorted(map(
...     attrgetter("index"),
...     reindex_variables(
...         {"this_is_a_test_case": clause}
...     )["this_is_a_test_case"].literals[0].atom.arguments
... ))
[0, 1, 2]
>>> clause = Clause((Literal(False,
...     Predicate(0, (Variable(5), Variable(10), Variable(5)))
... ),))
>>> sorted(map(
...     attrgetter("index"),
...     reindex_variables(
...         {"this_is_a_test_case": clause}
...     )["this_is_a_test_case"].literals[0].atom.arguments
... ))
[0, 1, 1]

Parameters:: clauses – a map of clause labels to clauses
Returns:: the list of clauses with renamed variables

Replace a sub-term with a given index (depth-first search) by a new term.

>>> atom = Predicate(7, (
...     Function(0, (Variable(0),)), Function(1, (Variable(2),))
... ))
>>> replace_subterm_by_index(atom, 0, Variable(3))
Traceback (most recent call last):
 ...
yapsap.utils.NoSubtermFound: 5
>>> from pprint import pprint
>>> pprint(
...     replace_subterm_by_index(atom, 4, Function(2, (Variable(3),))),
...     width=75
... )
Predicate(index=7,
          arguments=(Function(index=0, arguments=(Variable(index=0),)),
          Function(index=1,
                   arguments=(Function(index=2,
                                       arguments=(Variable(index=3),)),))))
>>> replace_subterm_by_index(Predicate(7, (Variable(0),)), 1, Variable(0))
Traceback (most recent call last):
 ...
yapsap.utils.TermSelfReplace

Parameters:

atom – a predicate or a term
index – an index of a sub-term to replace, must be greater than 0
term – replacement term for a given index

Returns:

Raises:

NoSubtermFound – if sub-term with a given index doesn’t exist

yapsap.utils.subterm_by_index(atom: Predicate | Variable | Function, index: int) → Variable | Function#

Extract a sub-term using depth-first search.

>>> atom = Predicate(7, (
...     Function(0, (Variable(0),)), Function(1, (Variable(1),))
... ))
>>> subterm_by_index(atom, 0)
Traceback (most recent call last):
 ...
ValueError: sub-term with index 0 exists only for terms, but got: ...
>>> subterm_by_index(atom, 1) == atom.arguments[0]
True
>>> subterm_by_index(atom, 2) == atom.arguments[0].arguments[0]
True
>>> subterm_by_index(atom, 4) == atom.arguments[1].arguments[0]
True

Parameters:

atom – a predicate or a term
index – an index of a desired sub-term

Returns:

a sub-term

Raises:

ValueError – when trying to get a term with index 0 of a predicate
NoSubtermFound – if sub-term with a given index doesn’t exist