Tools on Rewriting

CeTA is a tool that certifies termination analysis (in terms of a termination proof) provided by a termination tool.
* N. Hirokawa, A. Middeldorp, S. Winkler, and C. Sternagel Infinite Runs in Abstract Completion Proc. of the 2nd International Conference on Formal Structures for Computation and Ded...

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
* Download for Windows (32bit) ... Some notable changes: * Improved Isabelle/jEdit Prover IDE: more support for formal text structure, more visual feedback. * The Isabelle/ML IDE can loa...