RelDT is a relational dual tableaux automated theorem prover written in XSB Prolog
RelDT has two components:
- RelDT: Relational Dual Tableaux
- RelDT-DB: Database Relational Dual Tableaux
The first versions of RelDT and RelDT-DB were released July 7, 2005.
See this draft technical report (PDF 258k) for an introduction to dual tableaux. See this preprint (PDF 199k) for an introduction to the typed dual tableaux system.
RelDT was presented at the 3rd Relation Day at Brock on September 6, 2005. The presentation slides are available here. (PDF 171k)