Generate tasks for the given formulas and add them to the goal
The constants that can be considered free (resp., that have to be considered non-free) in this proof tree.
The fully simplified closing constraint
All constants that occur in formulas in this goal
Constants that can be eliminated in this goal because they are universal, and they do not occur in any tasks or compound formulas (but they might occur in the facts)
Return whether t
is a constant that is eliminated in this goal
Return whether t
is a constant that is eliminated in this goal
Eliminate all prioritised tasks for which the given predicate is false.
true
if the sets of free constants have reached a fixed point
Create the tasks to store and handle an arbitrary given formula.
Create the tasks to store and handle an arbitrary given formula. This method is part of the goal because different tasks might be created depending on the settings
Function to be called after split rules, to generate new inference collections for the subgoals.
Function to be called after split rules, to generate new inference collections for the subgoals. All compound formulae introduced by the split rule (formulae that are not literals) have to be given as arguments.
true
if there are chances that the
closingConstraint
of this tree changes by applying rules
to any goal
true
if it is possible to apply rules to any goal in this
tree
the vocabulary available at a certain node in the proof