An SMT solver. A high-performance theorem prover being developed at Microsoft Research.
DES (Datalog Educational System). A deductive database system with Datalog, SQL, and Relational Algebra query languages.
LaTeX. A document preparation system.