Slate (overview) is an intelligent system developed for ARDA, DARPA, and Rensselaer’s logic, mathematics, and computer science curricula.

Since 2005, Slate (in conjunction with NDL) has been used by students in the Introduction to Logic course at RPI as an intelligent assistant for designing, specifying, and validating or invalidating proofs and arguments.

Slate has many distinguishing characteristics that make it quite unique, including:

• Methods and an interface that supports rendering arguments, proofs, scenarios, counterexamples, etc. in visual form.
• Powered by new forms of visual reasoning that exceed standard linguistic/textual reasoning in standard logics (like first-order logic).
• Seamless integration with all the fastest standard provers in the world today (e.g., Vampire, Otter, Oscar, etc.), and with the best model finder as well.
• Automatic generation of first drafts of English reports to then be polished by the human user.
• Built-in libraries of case studies and problems.
• Support for all established forms of reasoning: deduction, induction, abduction (particularly the Wigmorean variety), probabilistic — all of these available in a visual form.
• New, effective forms of hypothesis generation.
• CL/IKL-compatible for interoperability with existing and future databases, knowledge bases, and other IA tools and technologies.

While Slate would seem to be almost everything one might want in a logical assistant, there is one thing Slate is not:

A replacement for human reasoners!