Write an introduction to the README

README.md

@@ -1,6 +1,12 @@
 # anthem
 
-A translator between answer set programs and first-order logic
+`anthem` is a command line application for translating answer set programs in the mini-gringo dialect of [clingo](https://potassco.org/clingo/) to first-order theories.
+Using an automated theorem prover, these theories can then be used to verify properties of the original programs, such as strong and external equivalence.
+
+Check out the [Manual](https://potassco.org/anthem/) to learn how to install and use `anthem`.
+
+If you want to use `anthem` as a library to build your own application, you can do so.
+Check out the [API documentation](https://docs.rs/anthem/) for the available functionalities.
 
 ## License