The Gandalf theorem prover is the first-order theorem prover applied to several domain-specific tasks such as Semantic web.
