System
The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation), several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.
E is implemented in C and portable to most UNIX dialects and the Cygwin environment. It is available under the GNU GPL.
Read more about this topic: E Theorem Prover
Famous quotes containing the word system:
“I need not say what match I would touch, what system endeavor to blow up; but as I love my life, I would side with the light, and let the dark earth roll from under me, calling my mother and my brother to follow.”
—Henry David Thoreau (1817–1862)
“Fear, coercion, punishment, are the masculine remedies for moral weakness, but statistics show their failure for centuries. Why not change the system and try the education of the moral and intellectual faculties, cheerful surroundings, inspiring influences? Everything in our present system tends to lower the physical vitality, the self-respect, the moral tone, and to harden instead of reforming the criminal.”
—Elizabeth Cady Stanton (1815–1902)
“Ethics and religion differ herein; that the one is the system of human duties commencing from man; the other, from God. Religion includes the personality of God; Ethics does not.”
—Ralph Waldo Emerson (1803–1882)