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:
“There are obvious places in which government can narrow the chasm between haves and have-nots. One is the public schools, which have been seen as the great leveler, the authentic melting pot. That, today, is nonsense. In his scathing study of the nation’s public school system entitled “Savage Inequalities,” Jonathan Kozol made manifest the truth: that we have a system that discriminates against the poor in everything from class size to curriculum.”
—Anna Quindlen (b. 1952)
“The twentieth-century artist who uses symbols is alienated because the system of symbols is a private one. After you have dealt with the symbols you are still private, you are still lonely, because you are not sure anyone will understand it except yourself. The ransom of privacy is that you are alone.”
—Louise Bourgeois (b. 1911)
“Whoever places his trust into a system will soon be without a home. While you are building your third story, the two lower ones have already been dismantled.”
—Franz Grillparzer (1791–1872)