Talos, named for the ancient Greek mythological robot is a DCEC* focused prover based on SPASS. It is build upon the resolution based theorem prover SPASS and is fast and efficient on the majority of proofs. As a resolution based theorem prover Talos is very efficient at proving or disproving theorems, but its proof output is bare bones at best. Talos is designed to function both as it’s own python program encapsulating the SPASS runtime or as a web interface to a version hosted at RAIR Labs.

Prover interface: https://prover.cogsci.rpi.edu/DCEC_PROVER/index.php, contact RAIR Labs for API keys to run the prover.

Example file for remotely calling Talos prover in Python

Github repo for the python shell: https://github.com/JamesPane-Joyce?tab=repositories