| Interface | Description |
|---|---|
| PrenexingStrategy |
A prenexing strategy.
|
| Class | Description |
|---|---|
| ExistsDownForAllUp |
∃↓∀↑ (prioritizing existential quantifiers)
|
| ExistsUpForAllDown |
∃↑∀↓ (prioritizing existential quantifiers)
|
| ForAllDownExistsDown |
∀↓∃↓
|
| ForAllDownExistsUp |
∀↓∃↑ (prioritizing universal quantifiers)
|
| ForAllUpExistsDown |
∀↑∃↓ (prioritizing universal quantifiers)
|
| ForAllUpExistsUp |
∀↑∃↑
|
| ShiftingStrategy |
Abstract class for strategies based on quantifier shifting.
|
| SimpleUpDownStrategy |
Abstract class for strategies based on simple variable reordering.
|