class Goal extends AnyRef
A Goal is a single-conclusion sequent - the basic node in a proof tree. A goal nodes knows its parent (except for the root goal) and children (the alternatives and their subgoals).
Each Goal stores a partial proof: a list of alternatives each of which stores a list of subgoals. Goals are disjunctive: a goal can be closed if all subgoals of one alternative can be closed.
The conclusion, the proof alternatives, and the proof term are stored statefully and are set by this class or other prover components.
The prover expands new goals greedily by applying invertible rules, and each goal stores those invertible rules that have not been applied yet.
- Source
- Goal.scala
- Alphabetic
- By Inheritance
- Goal
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
below(that: Goal): Boolean
true if that is an ancestor (reflexive, transitive) of this goal
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
def
conc: Term
the conclusion (may have been simplified since Goal creation)
- val context: Context
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
lazy val
fullContext: Context
the complete context/antecedent (i.e., including the parent's context) of this sequent
-
lazy val
fullVarAtoms: List[Atom]
the complete context of this goal seen as a list of atomic facts that rules can make use of
-
def
getAlternatives: List[Alternative]
the list of explored directions in the backward search space that can prove the goal
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getNextExpansion: Option[ApplicableTactic]
the invertible backward/forward tactics that have not been applied yet are stored here, but set and read by the Prover this method retrieves the next tactic to apply
-
final
def
getNextSearch(prover: Searcher): List[ApplicableTactic]
- Annotations
- @tailrec()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
isSolved: Boolean
checks if the goal can be closed by closing all subgoals of some alternative the result is cached so that the method can be called arbitrarily often without performance penalty
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
newFacts(implicit facts: Facts): Unit
recursively checks if the goal can be closed by using the axiom rule
recursively checks if the goal can be closed by using the axiom rule
should be called iff there are new facts available (result is cached by isSolved)
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
path: List[Goal]
the path from this goal up to the root of the proof tree
- def present(depth: Int)(implicit presentObj: (Obj) ⇒ String, current: Option[Goal], newAlt: Option[Alternative]): String
- def presentHtml(depth: Int, firstTime: Boolean = true)(implicit presentObj: (Obj) ⇒ String, current: Option[Goal], newAlt: Option[Alternative]): String
-
def
proof: Term
stores the proof, contains holes if the goal is not solved
-
def
setExpansionTactics(prover: Searcher, backw: List[BackwardInvertible], forw: List[ForwardInvertible]): Unit
initializes the invertible backward/forward tactics that can be applied
- def setSearchTactics(prover: Searcher, backw: List[BackwardSearch]): Unit
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- Goal → AnyRef → Any
-
lazy val
varAtoms: List[Atom]
the local context of this goal seen as a list of atomic facts that rules can make use of
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()