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. Protected

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
  4. def addTasksFor(fors: Iterable[Conjunction]): (Goal, Seq[CertFormula])

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

  5. val age: Int
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def bindingContext: BindingContext
    Definition Classes
    ProofTree
  8. val branchInferences: BranchInferenceCollection
  9. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  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
    Goal → ProofTree
  11. lazy val closingConstraint: Conjunction

    The fully simplified closing constraint

    The fully simplified closing constraint

    Definition Classes
    Goal → ProofTree
  12. val compoundFormulas: CompoundFormulas
  13. def constantFreedom: ConstantFreedom
    Definition Classes
    ProofTree
  14. lazy val constants: Set[ConstantTerm]

    All constants that occur in formulas in this goal

  15. val definedSyms: Substitution
  16. val eliminatedConstants: Set[ConstantTerm]
  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

  19. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  21. val facts: Conjunction
  22. def filterTasks(p: (PrioritisedTask) => Boolean): Goal

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

  23. 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
    Goal → ProofTree
  24. def formulaTasks(formula: Conjunction): Seq[FormulaTask]

    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

  25. def getCertificate: Certificate
  26. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  27. def getInferenceCollector: BranchInferenceCollector
  28. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  29. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  30. lazy val mayAlias: AliasChecker
  31. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  32. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  33. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  34. def order: TermOrder
    Definition Classes
    ProofTree
  35. lazy val reduceWithFacts: ReduceWithConjunction
  36. lazy val reducerSettings: Value
  37. val settings: GoalSettings
  38. def startNewInferenceCollection: BranchInferenceCollection
  39. 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.

  40. def startNewInferenceCollectionCert(initialFors: => Iterable[CertFormula]): BranchInferenceCollection
  41. def step(ptf: ProofTreeFactory): ProofTree
  42. 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
    Goal → ProofTree
  43. 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
    Goal → ProofTree
  44. val subtrees: Seq[ProofTree]
    Definition Classes
    Goal → ProofTree
  45. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  46. val tasks: TaskManager
  47. def toString(): String
    Definition Classes
    Goal → AnyRef → Any
  48. def updateConstantFreedom(cf: ConstantFreedom): Goal
  49. 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
    Goal → ProofTree
  50. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  51. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  52. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from ProofTree

Inherited from AnyRef

Inherited from Any

Ungrouped