E equational theorem prover
- E equational theorem prover
E is a modern, high performance theorem prover for full first-order logic with equality. It has been developed primarily in the "Automated Reasoning Group" at TU Munich.
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. It is available under the GNU GPL and can be downloaded from the home page linked below.
References
*cite journal
first=Stephan
last=Schulz
title=E - A Brainiac Theorem Prover
journal=Journal of AI Communications
volume=15
issue=2/3
pages=111–126
year=2002
* Schulz, Stephan (2004). System Description: E 0.81. Proceedings of the 2nd International Joint Conference on Automated Reasoning, Springer LNAI 3097.
External links
* [http://www.eprover.org E home page]
* [http://www4.in.tum.de/~schulz E's developer]
Wikimedia Foundation.
2010.
Look at other dictionaries:
Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… … Wikipedia
List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic … Wikipedia
Superposition calculus — The superposition calculus is a calculus for reasoning in equational first order logic. It has been developed in the early 1990s and combines concepts from first order resolution with ordering based equality handling as developed in the context… … Wikipedia
Stephan Schulz — Infobox Scientist name = Stephan Schulz image width= 200px caption = Stephan Schulz residence = Germany nationality = German field = Computer Technology known for = E equational theorem proverStephan Schulz is a German computer scientist working… … Wikipedia
Attribute sequence — A clause attribute is a characteristic of a clause. Some examples of clause attributes are: the number of literals in a clause (i.e., clause length) the number of term symbols in a clause the number of constants in a clause the number of… … Wikipedia
E (disambiguation) — E is the fifth letter of the Latin alphabet. E may also refer to:Medicine and genetics*E number, a number code for a food additive, an EU labelling requirement * Haplogroup E (mtDNA), a human mitochondrial DNA (mtDNA) haplogroup * Haplogroup E (Y … Wikipedia
Logic programming — is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy s [1958] advice taker proposal, logic is used as a purely declarative… … Wikipedia
Harald Ganzinger — (October 31 1950 June 3 2004) was a German computer scientist that together with Leo Bachmair developed the superposition calculus, which is (as of 2007) used in most of the state of the art automated theorem provers for first order logic.He… … Wikipedia
Prover9 — is an automated theorem prover for First order and equational logic developed by William McCune. Prover9 is the successor of the Otter theorem prover.Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples … Wikipedia
LF (logical framework) — In type theory, the LF logical framework provides a means to define (or present) logics. It is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but… … Wikipedia
