E Theorem Prover - System

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:

    Few white citizens are acquainted with blacks other than those projected by the media and the so—called educational system, which is nothing more than a system of rewards and punishments based upon one’s ability to pledge loyalty oaths to Anglo culture. The media and the “educational system” are the prime sources of racism in the United States.
    Ishmael Reed (b. 1938)

    The moral immune system of this country has been weakened and attacked, and the AIDS virus is the perfect metaphor for it. The malignant neglect of the last twelve years has led to breakdown of our country’s immune system, environmentally, culturally, politically, spiritually and physically.
    Barbra Streisand (b. 1942)

    In the end we beat them with Levi 501 jeans. Seventy-two years of Communist indoctrination and propaganda was drowned out by a three-ounce Sony Walkman. A huge totalitarian system ... has been brought to its knees because nobody wants to wear Bulgarian shoes.... Now they’re lunch, and we’re number one on the planet.
    —P.J. (Patrick Jake)