SInE (Sumo Inference Engine) is a metaprover targeted on large
theories, especially on SUMO.
Given a theory and a conjecture, SInE selects some axioms from the theory
and runs an underlying theory prover on them (and the conjecture, of course). Axiom selection is based on
symbols used in the conjecture -- we take axioms which somehow "define"
the meaning of conjecture's symbols. Go here for more
SInE has won the LTB division of CASC-J4 (2008).
you can download SInE 0.3 with the E prover
as an underlying inference engine.
For the CASC-22 the last year's version of SInE was slightly modified in order to comply with the new rules of the LTB category. It can be downloaded here
It has won the SMO category of the LTB
division and placed third in the division. Also, four best provers of the division were all using the SInE axiom selection strategy.
Based on several suggestions of Geoff Suttcliffe
, a version with improved "user experience" was created and is available here
The development of SInE started as part of my
Master thesis at the Charles University in Prague.
SInE is distributed under GPLv3. If you're using SInE on something else than TPTP problems, please let me know at .