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:

    Short of a wholesale reform of college athletics—a complete breakdown of the whole system that is now focused on money and power—the women’s programs are just as doomed as the men’s are to move further and further away from the academic mission of their colleges.... We have to decide if that’s the kind of success for women’s sports that we want.
    Christine H. B. Grant, U.S. university athletic director. As quoted in the Chronicle of Higher Education, p. A42 (May 12, 1993)

    To care for the quarrels of the past, to identify oneself passionately with a cause that became, politically speaking, a losing cause with the birth of the modern world, is to experience a kind of straining against reality, a rebellious nonconformity that, again, is rare in America, where children are instructed in the virtues of the system they live under, as though history had achieved a happy ending in American civics.
    Mary McCarthy (1912–1989)

    Authority is the spiritual dimension of power because it depends upon faith in a system of meaning that decrees the necessity of the hierarchical order and so provides for the unity of imperative control.
    Shoshana Zuboff (b. 1951)