Research software
  • Redlog: Computing with Logic
    Redlog is an integral part of the interactive computer algebra system Reduce. It supplies reasoning capabilities for first-order formulas interpreted over specific theories, including Nonlinear Real Arithmetic, Presburger Arithmetic, and parametric QSAT.
  • Spass: an automated theorem prover for first-order logic with equality.
  • TLAPS: the TLA+ proof system
    The TLA+ Proof System (TLAPS) is a platform for computerized verification of TLA+ proofs using formal reasoning systems such as automated theorem provers, proof-assistants, SMT/SAT solvers, and decision procedures. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various backend verifiers. TLAPS is free software, distributed under a BSD-like license.
  • veriT: an open-source, proof-producing SMT (Satisfiability Modulo Theories) solver.