SInE 0.4

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 the conjecture's symbols.

This version of SInE uses E as the underlying prover. Vampire can also be used.




For the purpose of submitting this package to Fedora, here is the RPM spec file.

Back to the RPMS

Last modified: Tue Jan 21 08:48:00 MST 2014 by Jerry James