Class/Object

ap.proof.goal

Goal

Related Docs: object Goal | package goal

Permalink

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  4. def addTasksFor(fors: Iterable[Conjunction]): (Goal, Seq[CertFormula])

    Permalink

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

  5. val age: Int

    Permalink
  6. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  7. def bindingContext: BindingContext

    Permalink
    Definition Classes
    ProofTree
  8. val branchInferences: BranchInferenceCollection

    Permalink
  9. def clone(): AnyRef

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

    Permalink

    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

    Permalink

    The fully simplified closing constraint

    The fully simplified closing constraint

    Definition Classes
    GoalProofTree
  12. val compoundFormulas: CompoundFormulas

    Permalink
  13. def constantFreedom: ConstantFreedom

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

    Permalink

    All constants that occur in formulas in this goal

  15. val definedSyms: Substitution

    Permalink
  16. val eliminatedConstants: Set[ConstantTerm]

    Permalink
  17. lazy val eliminatedIsolatedConstants: Set[ConstantTerm]

    Permalink

    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

    Permalink

    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

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

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

    Permalink
  22. def filterTasks(p: (PrioritisedTask) ⇒ Boolean): Goal

    Permalink

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

  23. lazy val fixedConstantFreedom: Boolean

    Permalink

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

    Permalink

    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

    Permalink
  26. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  27. def getInferenceCollector: BranchInferenceCollector

    Permalink
  28. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  29. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  30. lazy val mayAlias: AliasChecker

    Permalink
  31. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  32. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  33. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  34. def order: TermOrder

    Permalink
    Definition Classes
    ProofTree
  35. lazy val reduceWithFacts: ReduceWithConjunction

    Permalink
  36. lazy val reducerSettings: Value

    Permalink
  37. val settings: GoalSettings

    Permalink
  38. def startNewInferenceCollection: BranchInferenceCollection

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

    Permalink

    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

    Permalink
  41. def step(ptf: ProofTreeFactory): ProofTree

    Permalink
  42. val stepMeaningful: Boolean

    Permalink

    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
  43. val stepPossible: Boolean

    Permalink

    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
  44. val subtrees: Seq[ProofTree]

    Permalink
    Definition Classes
    GoalProofTree
  45. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  46. val tasks: TaskManager

    Permalink
  47. def toString(): String

    Permalink
    Definition Classes
    Goal → AnyRef → Any
  48. def updateConstantFreedom(cf: ConstantFreedom): Goal

    Permalink
  49. val vocabulary: Vocabulary

    Permalink

    the vocabulary available at a certain node in the proof

    the vocabulary available at a certain node in the proof

    Definition Classes
    GoalProofTree
  50. final def wait(arg0: Long, arg1: Int): Unit

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  52. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from ProofTree

Inherited from AnyRef

Inherited from Any

Ungrouped