SInE

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 detailed description.

SInE has won the LTB division of CASC-J4 (2008).

Here you can download SInE 0.3 with the E prover as an underlying inference engine.
You can also run SInE online from the System on TPTP web.
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 .



(home)