Automated theorem proving in Haskell

Automated reasoning is a prerequisite for computers to be able to deduce logical conclusions, i.e. to make decisions on their own. It can for example be used to provemathematical theorems. This report presents implementations of three automated theorem provers capable of proving theorems in first-order logic. They are based on resolution, narrowing and method of analytic tableau and are compared with respect toperformance, readability of generated proofs and difficulty of implementation.

All the details can be viewed in the report (which is written in Swedish).

View the report