# QuantifierElimProver

### Related Doc: package proof

#### object QuantifierElimProver

Prover to eliminate quantifiers in a PA formula. The prover is losely based on the idea in the paper "A Quantifier Elimination Algorithm for Linear Real Arithmetic" by David Monniaux, although it does not explicitly compute solutions of the matrix of a quantified formula like in the paper. Instead, the constraint extracted from an exhaustive subtree is injected as a lemma into other subtrees and used to close such subtrees earlier.

It is assumed that it is never necessary to adjust the constant freedom of a proof tree in this setting, because all constants that shield formulas also have to be eliminated constants and, thus, never occur in constraints anyway. This makes it possible to construct proof trees in a purely depth-first way (just like in the `ModelSearchProver`)

TODO: at the moment, this prover does not support theories like bit-vectors or multiplication

Linear Supertypes
AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. QuantifierElimProver
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )