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).

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Hoder, Kryštof; Voronkov, Andrei: Sine qua non for large theory reasoning (2011)