Package edu.udel.cis.vsl.sarl.prove.IF

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 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

      ValidityResult valid(BooleanExpression predicate)

      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

      ValidityResult unsat(BooleanExpression predicate) throws TheoremProverException

      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