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:
“Delight at having understood a very abstract and obscure system leads most people to believe in the truth of what it demonstrates.”
—G.C. (Georg Christoph)
“While the system of holding people in hostage is as old as the oldest war, a fresher note is introduced when a tyrannic state is at war with its own subjects and may hold any citizen in hostage with no law to restrain it.”
—Vladimir Nabokov (1899–1977)
“A person, seasoned with a just sense of the imperfections of natural reason, will fly to revealed truth with the greatest avidity: while the haughty Dogmatist, persuaded that he can erect a compleat system of Theology by the mere help of philosophy, disdains any further aid, and rejects this adventitious instructor.”
—David Hume (1711–1776)