# Interface TheoremProver

All Known Implementing Classes:
`MultiProver`, `RobustCVCTheoremProver`, `RobustWhy3ProvePlatform`, `RobustZ3TheoremProver`

public interface TheoremProver
Provides an abstract interface for an automated theorem prover operating under a fixed context (i.e., a boolean expression assumed to hold).
• ## Method Summary

Modifier and Type
Method
Description
`PreUniverse`
`universe()`
Get the symbolic universe associated with the theorem prover.
`ValidityResult`
`unsat(BooleanExpression predicate)`
Attempts to determine whether the statement p(x) && q(x) is unsatisfiable.
`ValidityResult`
`valid(BooleanExpression predicate)`
Attempts to determine whether the statement p(x)=>q(x) is valid, i.e., is a tautology.
`ValidityResult`
`validOrModel(BooleanExpression predicate)`
Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample).
• ## Method Details

• ### universe

PreUniverse universe()
Get the symbolic universe associated with the theorem prover. This is the object used to create and manipulate symbolic expressions.
Returns:
the symbolic universe associated to this theorem prover
• ### valid

Attempts to determine whether the statement p(x)=>q(x) is valid, i.e., is a tautology. Here, p is the "context", q is the "predicate", and x stands for the set of all symbolic constants which occur in p or q.

A result of type YES implies forall x.(p(x)=>q(x)). A result of NO implies nsat(p)||exists x.(p(x)&&!q(x)). Nothing can be concluded from a result of MAYBE.

nsat(p) means p is not satisfiable, i.e., forall x.!p(x), or equivalently !exists x.p(x). Note that if p is not satisfiable then any of the three possible results could be returned.

Note that if the context is unsatisfiable then any of the three types could be returned.

Consider the case where the context p is "true". If valid(q) returns YES then forall x.q(x) (i.e., q is a tautology); if it returns NO then exists x.!q(x) (i.e., q is not a tautology). If valid(!q) returns YES then q is not satisfiable; if it returns NO then q is satisfiable.

Note that in the case NO is returned, there is no guarantee this method will attempt to find a model (and return an instance of `ModelResult`). If a model is required in the NO case, use method `validOrModel(edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression)` instead.

Parameters:
`predicate` - the boolean expression q(x)
Returns:
a ValidityResult whose type must satisfy the constraints described above
Throws:
`TheoremProverException` - if something goes wrong with the automated theorem prover during this call
• ### unsat

Attempts to determine whether the statement p(x) && q(x) is unsatisfiable. Here, p is the "context", q is the "predicate", and x stands for the set of all symbolic constants which occur in p or q.

A result of type YES implies `forall x. !(p(x) && q(x))`. A result of NO implies `exists x. p(x)&&q(x)`. Nothing can be concluded from a result of MAYBE.

Parameters:
`predicate` - the boolean expression q(x)
Returns:
a `ValidityResult` whose type must satisfy the constraints described above
Throws:
`TheoremProverException` - if something goes wrong with the automated theorem prover during this call
• ### validOrModel

ValidityResult validOrModel(BooleanExpression predicate)
Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample). The specification is exactly the same as for `valid(edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression)`, except that a `ModelResult` is returned in the NO case. This provides a method to get the model. Note that the model may be null if there was some problem in obtaining or constructing the model. If the model is non-null, it will be a map in which the key set consists of all the symbolic constants of non-function type that occur in the context or predicate. The value associated to a key will be a concrete symbolic expression.
Returns:
a validity result as specified above
Throws:
`TheoremProverException` - if something goes wrong with the automated theorem prover during this call