Software

Current Projects

Previous Projects

  • Classic SPASS Theorem Prover
  • COMPIT - COMParison of Indexing Techniques for automated reasoning
  • OPBDP - linear 0-1 (pseudo-boolean) optimization
  • SATURATE - an experimental theorem prover for first-order logic, primarily based on saturation
  • SCAN - elimination of second-order quantifiers.