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
    @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. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  24. 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
  25. 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

  26. def getCertificate: Certificate

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

    Permalink
    Definition Classes
    AnyRef → Any
  28. def getInferenceCollector: BranchInferenceCollector

    Permalink
  29. def hashCode(): Int

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

    Permalink
    Definition Classes
    Any
  31. lazy val mayAlias: AliasChecker

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

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

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

    Permalink
    Definition Classes
    AnyRef
  35. def order: TermOrder

    Permalink
    Definition Classes
    ProofTree
  36. lazy val reduceWithFacts: ReduceWithConjunction

    Permalink
  37. lazy val reducerSettings: Value

    Permalink
  38. val settings: GoalSettings

    Permalink
  39. def startNewInferenceCollection: BranchInferenceCollection

    Permalink
  40. 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.

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
  47. val tasks: TaskManager

    Permalink
  48. def toString(): String

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

    Permalink
  50. 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
  51. final def wait(): Unit

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

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

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

Inherited from ProofTree

Inherited from AnyRef

Inherited from Any

Ungrouped