Jump to letter: [
ABCDEFGHIJKLMNOPQRSTUVWXYZ
]
cvc3 - CVC3 - Automated validity checker
- Description:
CVC3 is an automated validity checker for a many-sorted (i.e., typed)
first-order logic with built-in theories, including some support for
quantifiers, partial functions, and predicate subtypes. The current built-in
theories are the theories of:
* equality over free (aka uninterpreted) function and predicate symbols
* real and integer linear arithmetic (with some support for non-linear
arithmetic)
* bit vectors
* arrays
* tuples
* records
* user-defined inductive datatypes
Packages
