# ModelSearchProver

### Related Docs: object ModelSearchProver | package proof

#### class ModelSearchProver extends AnyRef

A prover that tries to construct a countermodel of a ground formula. This prover works in depth-first mode, in contrast to the `ExhaustiveProver`.

Linear Supertypes
AnyRef, Any
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ModelSearchProver
2. AnyRef
3. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### 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 apply(inputDisjuncts: Seq[Conjunction], order: TermOrder, withFullModel: Boolean = true): Either[Conjunction, Certificate]

`inputDisjuncts` are the formulae (connected disjunctively) to be disproven.

`inputDisjuncts` are the formulae (connected disjunctively) to be disproven. The result of the method is either countermodel of `inputDisjuncts` (the case `Left`), or a proof of validity (`Right`). In case proof construction is disabled, the validity result will be `Left(FALSE)`.

5. #### def apply(inputFor: Formula, order: TermOrder): Conjunction

`inputFor` is the formula to be disproven.

`inputFor` is the formula to be disproven. The result of the method is a countermodel of `inputFor`, or `FALSE` if it was not possible to find one (this implies that `inputFor` is valid).

6. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
7. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
8. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
9. #### def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
10. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
11. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
12. #### def hashCode(): Int

Definition Classes
AnyRef → Any
13. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
14. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
15. #### final def notify(): Unit

Definition Classes
AnyRef
16. #### final def notifyAll(): Unit

Definition Classes
AnyRef
17. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
18. #### def toString(): String

Definition Classes
AnyRef → Any
19. #### final def wait(): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )