44 * New proof method "smt" for a combination of first-order logic |
44 * New proof method "smt" for a combination of first-order logic |
45 with equality, linear and nonlinear (natural/integer/real) |
45 with equality, linear and nonlinear (natural/integer/real) |
46 arithmetic, and fixed-size bitvectors; there is also basic |
46 arithmetic, and fixed-size bitvectors; there is also basic |
47 support for higher-order features (esp. lambda abstractions). |
47 support for higher-order features (esp. lambda abstractions). |
48 It is an incomplete decision procedure based on external SMT |
48 It is an incomplete decision procedure based on external SMT |
49 solvers using the oracle mechanism. |
49 solvers using the oracle mechanism; for the SMT solver Z3, |
|
50 this method is proof-producing. Certificates are provided to |
|
51 avoid calling the external solvers solely for re-checking proofs. |
50 |
52 |
51 * Reorganization of number theory: |
53 * Reorganization of number theory: |
52 * former session NumberTheory now named Old_Number_Theory |
54 * former session NumberTheory now named Old_Number_Theory |
53 * new session Number_Theory by Jeremy Avigad; if possible, prefer this. |
55 * new session Number_Theory by Jeremy Avigad; if possible, prefer this. |
54 * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; |
56 * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; |