# Goal

### Related Docs: object Goal | package goal

#### class Goal extends ProofTree

Linear Supertypes
ProofTree, AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. Goal
2. ProofTree
3. AnyRef
4. Any
1. Hide All
2. Show All
Visibility
1. Public
2. All

### Value Members

1. #### final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
2. #### final def ##(): Int

Definition Classes
AnyRef → Any
3. #### final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any

Generate tasks for the given formulas and add them to the goal

6. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
7. #### def bindingContext: BindingContext

Definition Classes
ProofTree

9. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
10. #### lazy val closingConstantFreedom: ConstantFreedom

The constants that can be considered free (resp., that have to be considered non-free) in this proof tree.

The constants that can be considered free (resp., that have to be considered non-free) in this proof tree.

Definition Classes
GoalProofTree
11. #### lazy val closingConstraint: Conjunction

The fully simplified closing constraint

The fully simplified closing constraint

Definition Classes
GoalProofTree

13. #### def constantFreedom: ConstantFreedom

Definition Classes
ProofTree
14. #### lazy val constants: Set[ConstantTerm]

All constants that occur in formulas in this goal

17. #### lazy val eliminatedIsolatedConstants: Set[ConstantTerm]

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)

18. #### def eliminates(t: Term): Boolean

Return whether t is a constant that is eliminated in this goal

Return whether t is a constant that is eliminated in this goal

19. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
20. #### def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
21. #### val facts: Conjunction

Eliminate all prioritised tasks for which the given predicate is false.

23. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
24. #### lazy val fixedConstantFreedom: Boolean

true if the sets of free constants have reached a fixed point

true if the sets of free constants have reached a fixed point

Definition Classes
GoalProofTree

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

27. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any

29. #### def hashCode(): Int

Definition Classes
AnyRef → Any
30. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any

32. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
33. #### final def notify(): Unit

Definition Classes
AnyRef
34. #### final def notifyAll(): Unit

Definition Classes
AnyRef
35. #### def order: TermOrder

Definition Classes
ProofTree

40. #### def startNewInferenceCollection(initialFors: ⇒ Iterable[Conjunction]): BranchInferenceCollection

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.

43. #### val stepMeaningful: Boolean

true if there are chances that the closingConstraint of this tree changes by applying rules to any goal

true if there are chances that the closingConstraint of this tree changes by applying rules to any goal

Definition Classes
GoalProofTree
44. #### val stepPossible: Boolean

true if it is possible to apply rules to any goal in this tree

true if it is possible to apply rules to any goal in this tree

Definition Classes
GoalProofTree
45. #### val subtrees: Seq[ProofTree]

Definition Classes
GoalProofTree
46. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef

48. #### def toString(): String

Definition Classes
Goal → AnyRef → Any

50. #### val vocabulary: Vocabulary

the vocabulary available at a certain node in the proof

the vocabulary available at a certain node in the proof

Definition Classes
GoalProofTree
51. #### final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
52. #### final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
53. #### final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )