Applications and libraries/Theorem provers
< Applications and libraries
Jump to navigation
Jump to search
Revision as of 19:31, 25 March 2006 by EndreyMark (talk | contribs) (The description of Agda mentioned dependent types, so I made a link to Dependent types wikipage.)
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 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 generates Haskell code * from a type declaration, using a decision procedure from intuitionistic propositional calculus.
- Paradox ”processes first-order logic problems and tries to find finite-domain models for them”.
- Dumatel “is a prover based on many-sorted term rewriting (TRW) and equational reasoning”