Applications and libraries/Theorem provers
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
Theorem provers
- Agda
- Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with Dependent types. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.
- Djinn
- Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus.
- Paradox
- Paradox processes first-order logic problems and tries to find finite-domain models for them.
- Dumatel
- Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning
- Camila
- Camila is a system for software development using formal methods. Other materials on formal methods can be found also on Analysis and design page.