Goal

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def addTasksFor(fors: Iterable[Conjunction]): (Goal, Seq[CertFormula])

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

val age: Int

final def asInstanceOf[T0]: T0

def bindingContext: BindingContext

val branchInferences: BranchInferenceCollection

def clone(): AnyRef

lazy val closingConstantFreedom: ConstantFreedom

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

lazy val closingConstraint: Conjunction

The fully simplified closing constraint

val compoundFormulas: CompoundFormulas

def constantFreedom: ConstantFreedom

lazy val constants: Set[ConstantTerm]

All constants that occur in formulas in this goal

val definedSyms: Substitution

val eliminatedConstants: Set[ConstantTerm]

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)

def eliminates(t: Term): Boolean

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

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

val facts: Conjunction

def filterTasks(p: (PrioritisedTask) ⇒ Boolean): Goal

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

lazy val fixedConstantFreedom: Boolean

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

def formulaTasks(formula: Conjunction): Seq[FormulaTask]

Create the tasks to store and handle an arbitrary given formula.

def getCertificate: Certificate

final def getClass(): Class[_]

def getInferenceCollector: BranchInferenceCollector

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

lazy val mayAlias: AliasChecker

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def order: TermOrder

lazy val reduceWithFacts: ReduceWithConjunction

lazy val reducerSettings: Value

val settings: GoalSettings

def startNewInferenceCollection: BranchInferenceCollection

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

Function to be called after split rules, to generate new inference collections for the subgoals.

def startNewInferenceCollectionCert(initialFors: ⇒ Iterable[CertFormula]): BranchInferenceCollection

def step(ptf: ProofTreeFactory): ProofTree

val stepMeaningful: Boolean

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

val stepPossible: Boolean

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

val subtrees: Seq[ProofTree]

final def synchronized[T0](arg0: ⇒ T0): T0

val tasks: TaskManager

def toString(): String

def updateConstantFreedom(cf: ConstantFreedom): Goal

val vocabulary: Vocabulary

the vocabulary available at a certain node in the proof

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit