Equational prover

Last updated

EQP (Equational prover) is an automated theorem proving program for equational logic, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory. It was one of the provers used for solving a longstanding problem posed by Herbert Robbins, namely, whether all Robbins algebras are Boolean algebras.

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

<span class="mw-page-title-main">Boolean algebra (structure)</span> Algebraic structure modeling logical operations

In abstract algebra, a Boolean algebra or Boolean lattice is a complemented distributive lattice. This type of algebraic structure captures essential properties of both set operations and logic operations. A Boolean algebra can be seen as a generalization of a power set algebra or a field of sets, or its elements can be viewed as generalized truth values. It is also a special case of a De Morgan algebra and a Kleene algebra.

<span class="mw-page-title-main">Discrete mathematics</span> Study of discrete mathematical structures

Discrete mathematics is the study of mathematical structures that can be considered "discrete" rather than "continuous". Objects studied in discrete mathematics include integers, graphs, and statements in logic. By contrast, discrete mathematics excludes topics in "continuous mathematics" such as real numbers, calculus or Euclidean geometry. Discrete objects can often be enumerated by integers; more formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics".

<span class="mw-page-title-main">George Boole</span> English mathematician, philosopher and logician (1815–1864)

George BooleJnr was a largely self-taught English mathematician, philosopher, and logician, most of whose short career was spent as the first professor of mathematics at Queen's College, Cork in Ireland. He worked in the fields of differential equations and algebraic logic, and is best known as the author of The Laws of Thought (1854) which contains Boolean algebra. Boolean logic is credited with laying the foundations for the Information Age alongside the work of Claude Shannon.

A computer algebra system (CAS) or symbolic algebra system (SAS) is any mathematical software with the ability to manipulate mathematical expressions in a way similar to the traditional manual computations of mathematicians and scientists. The development of the computer algebra systems in the second half of the 20th century is part of the discipline of "computer algebra" or "symbolic computation", which has spurred work in algorithms over mathematical objects such as polynomials.

Laws of Form is a book by G. Spencer-Brown, published in 1969, that straddles the boundary between mathematics and philosophy. LoF describes three distinct logical systems:

<span class="mw-page-title-main">Marshall H. Stone</span> American mathematician

Marshall Harvey Stone was an American mathematician who contributed to real analysis, functional analysis, topology and the study of Boolean algebras.

<span class="mw-page-title-main">ORACLE (computer)</span>

The ORACLE or Oak Ridge Automatic Computer and Logical Engine, an early computer built by Oak Ridge National Laboratory, was based on the IAS architecture developed by John von Neumann.

In mathematics and abstract algebra, the two-element Boolean algebra is the Boolean algebra whose underlying setB is the Boolean domain. The elements of the Boolean domain are 1 and 0 by convention, so that B = {0, 1}. Paul Halmos's name for this algebra "2" has some following in the literature, and will be employed here.

In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation. The motivating example of a relation algebra is the algebra 2X 2 of all binary relations on a set X, that is, subsets of the cartesian square X2, with RS interpreted as the usual composition of binary relations R and S, and with the converse of R as the converse relation.

In abstract algebra, a Robbins algebra is an algebra containing a single binary operation, usually denoted by , and a single unary operation usually denoted by satisfying the following axioms:

Boolean algebra is a mathematically rich branch of abstract algebra. Stanford Encyclopaedia of Philosophy defines Boolean algebra as 'the algebra of two-valued logic with only sentential connectives, or equivalently of algebras of sets under union and complementation.' Just as group theory deals with groups, and linear algebra with vector spaces, Boolean algebras are models of the equational theory of the two values 0 and 1. Common to Boolean algebras, groups, and vector spaces is the notion of an algebraic structure, a set closed under some operations satisfying certain equations.

MINPACK is a library of FORTRAN subroutines for the solving of systems of nonlinear equations, or the least-squares minimization of the residual of a set of linear or nonlinear equations.

<span class="mw-page-title-main">John Alan Robinson</span> American computer scientist

John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.

<span class="mw-page-title-main">Computational mathematics</span> Area of mathematics

Computational mathematics is an area of mathematics devoted to the interaction between mathematics and computer computation.

<span class="mw-page-title-main">Computer algebra</span> Scientific area at the interface between computer science and mathematics

In mathematics and computer science, computer algebra, also called symbolic computation or algebraic computation, is a scientific area that refers to the study and development of algorithms and software for manipulating mathematical expressions and other mathematical objects. Although computer algebra could be considered a subfield of scientific computing, they are generally considered as distinct fields because scientific computing is usually based on numerical computation with approximate floating point numbers, while symbolic computation emphasizes exact computation with expressions containing variables that have no given value and are manipulated as symbols.

In mathematical logic, minimal axioms for Boolean algebra are assumptions which are equivalent to the axioms of Boolean algebra, chosen to be as short as possible. For example, an axiom with six NAND operations and three variables is equivalent to Boolean algebra:

C. William Gear was a British-American mathematician who specialized in numerical analysis and computer science. Gear was an American citizen.

In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values true and false, usually denoted 1 and 0, whereas in elementary algebra the values of the variables are numbers. Second, Boolean algebra uses logical operators such as conjunction (and) denoted as , disjunction (or) denoted as , and the negation (not) denoted as ¬. Elementary algebra, on the other hand, uses arithmetic operators such as addition, multiplication, subtraction, and division. Boolean algebra is therefore a formal way of describing logical operations, in the same way that elementary algebra describes numerical operations.

Boolean differential calculus (BDC) is a subject field of Boolean algebra discussing changes of Boolean variables and Boolean functions.

References