In short
DTC is a typechecker for Prolog based on a research carried out by Witold Charatonik and Andreas Podelski. DTC has been implemented by Jacek Śliwerski.
Download
Requirements
DTC is written in Nemerle and thus it runs on almost any .NET platform. However, Unix environment is recommended.