# Applications and libraries/Theorem provers

### From HaskellWiki

< Applications and libraries(Difference between revisions)

Line 6: | Line 6: | ||

:Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with [[Dependent type]]s. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future. | :Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with [[Dependent type]]s. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future. | ||

− | ;[http:// | + | ;[http://citeseer.ist.psu.edu/29367.html A resolution-based theorem prover for FOL] |

− | : | + | :Haskell implementation of a resolution based theorem prover for first order logic. |

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila] | ;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila] | ||

:Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the [[Analysis and design|analysis and design]] page. | :Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the [[Analysis and design|analysis and design]] page. | ||

− | |||

;[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne] | ;[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne] | ||

:Cayenne is a functional language with a powerful [[Dependent type|dependent type system]]. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system. | :Cayenne is a functional language with a powerful [[Dependent type|dependent type system]]. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system. | ||

+ | ;[http://www.cwi.nl/~jve/demo/ DEMO] | ||

+ | :Model checking for dynamic epistemic logic. DEMO is a tool for modelling change in epistemic logic (the logic of knowledge). Among other things, DEMO allows modeling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, translation of dynamic epistemic formulas to PDL (propositional dynamic logic) formulas. More materials and other Haskell resources on dynamic epistemic modelling (and more generally on logic and [[linguistics]]) can be found on [http://homepages.cwi.nl/~jve/index.html Jan van Eijck's page]. | ||

+ | ;[http://darcs.augustsson.net/Darcs/Djinn Djinn] | ||

+ | :Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus. | ||

+ | ;[http://www.haskell.org/dumatel/ Dumatel] | ||

+ | : Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning | ||

;[http://www.e-pig.org/ Epigram] | ;[http://www.e-pig.org/ Epigram] | ||

:Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design. | :Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design. | ||

+ | ;[http://www.cs.chalmers.se/~koen/pubs/dagstuhl05-equinox.ppt Equinox] | ||

+ | :Equinox is a new theorem prover for pure first-order logic with equality. It finds ground proofs of the input theory, by solving successive ground instantiations of the theory using an incremental SAT-solver. Equality is dealt with using a Nelson-Oppen framework. | ||

+ | ;[http://fldit-www.cs.uni-dortmund.de/~peter/#1 Expander2] | ||

+ | :Expander2 is a flexible multi-purpose workbench for rewriting, verification, constraint solving, flow graph analysis and related procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as 2D structures ranging from trees and rooted graphs to tables, fractals and other turtle-system-generated pictures. | ||

+ | |||

+ | ;[http://www.cs.yale.edu/homes/cc392/report.html FOL Resolution Theorem Prover] | ||

+ | :An implementation of a simple theorem prover in first-order logic using Haskell. | ||

;[http://taz.cs.wcupa.edu/~dmead/code/halp/ Halp] | ;[http://taz.cs.wcupa.edu/~dmead/code/halp/ Halp] | ||

:Haskell Logic Prover is written in Haskell supports first order logic with plans to add predicates. Also included is a simple frontend written in Java 5. | :Haskell Logic Prover is written in Haskell supports first order logic with plans to add predicates. Also included is a simple frontend written in Java 5. | ||

− | ;[http://www. | + | ;[http://www.math.chalmers.se/~koen/paradox/ Paradox] |

− | : | + | :Paradox processes first-order logic problems and tries to find finite-domain models for them. |

;[http://proofgeneral.inf.ed.ac.uk/Kit Proof General Kit] | ;[http://proofgeneral.inf.ed.ac.uk/Kit Proof General Kit] | ||

:The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface. | :The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface. | ||

− | ;[http:// | + | ;[http://www.haskell.org/yarrow/ Yarrow] |

− | : | + | :Yarrow is a proof-assistant for Pure Type Systems (PTSs) with several extensions. In Yarrow you can experiment with various pure type systems, representing different logics and programming languages. |

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

== Libraries == | == Libraries == |

## Revision as of 05:30, 6 December 2006

Tools for formal reasoning, written in Haskell.

## 1 Applications

- 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.

- A resolution-based theorem prover for FOL
- Haskell implementation of a resolution based theorem prover for first order logic.

- Camila
- Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the analysis and design page.

- Cayenne
- Cayenne is a functional language with a powerful dependent type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system.

- DEMO
- Model checking for dynamic epistemic logic. DEMO is a tool for modelling change in epistemic logic (the logic of knowledge). Among other things, DEMO allows modeling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, translation of dynamic epistemic formulas to PDL (propositional dynamic logic) formulas. More materials and other Haskell resources on dynamic epistemic modelling (and more generally on logic and linguistics) can be found on Jan van Eijck's page.
- Djinn
- Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus.

- Dumatel
- Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning

- Epigram
- Epigram is a prototype dependently typed functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.

- Equinox
- Equinox is a new theorem prover for pure first-order logic with equality. It finds ground proofs of the input theory, by solving successive ground instantiations of the theory using an incremental SAT-solver. Equality is dealt with using a Nelson-Oppen framework.

- Expander2
- Expander2 is a flexible multi-purpose workbench for rewriting, verification, constraint solving, flow graph analysis and related procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as 2D structures ranging from trees and rooted graphs to tables, fractals and other turtle-system-generated pictures.

- FOL Resolution Theorem Prover
- An implementation of a simple theorem prover in first-order logic using Haskell.

- Halp
- Haskell Logic Prover is written in Haskell supports first order logic with plans to add predicates. Also included is a simple frontend written in Java 5.

- Paradox
- Paradox processes first-order logic problems and tries to find finite-domain models for them.

- Proof General Kit
- The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface.

- Yarrow
- Yarrow is a proof-assistant for Pure Type Systems (PTSs) with several extensions. In Yarrow you can experiment with various pure type systems, representing different logics and programming languages.

## 2 Libraries

- Ivor
- is type theory based theorem proving library -- written by Edwin Brady (see also the author's homepage, there are a lot of materials concerning dependent type theory there).

*This page contains a list of libraries and tools in a certain category. For a comprehensive list of such pages, see Applications and libraries.*