IncProver

abstract def assert(fors: Iterable[Conjunction], newOrder: TermOrder): IncProver

abstract def assert(f: Conjunction, newOrder: TermOrder): IncProver

abstract def checkValidity(constructModel: Boolean): Either[Conjunction, Certificate]

abstract def checkValidityDir(searchDirector: (Conjunction, Boolean) ⇒ SearchDirection, lemmaBase: LemmaBase): Either[Conjunction, Certificate]

abstract def checkValidityDir(searchDirector: (Conjunction, Boolean) ⇒ SearchDirection): Either[Conjunction, Certificate]

abstract def conclude(fors: Iterable[Conjunction], newOrder: TermOrder): IncProver

abstract def conclude(f: Conjunction, newOrder: TermOrder): IncProver

abstract def filterTasks(p: (PrioritisedTask) ⇒ Boolean): IncProver

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

abstract def isObviouslyUnprovable: Boolean

Apply a simple criterion to check whether the formulas so far are not valid (there are still countermodels)

abstract def isObviouslyValid: Boolean

Apply a simple criterion to check whether the formulas so far are valid

abstract def order: TermOrder

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

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

def toString(): String

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit