equational logic

(logic)

First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into Universal algebra by Birkhoff et al. [Birkhoff, Gratzer, Cohn]. It was later made into a branch of category theory by Lawvere ("algebraic theories").

This article is provided by FOLDOC - Free Online Dictionary of Computing (foldoc.org)

Mentioned in

References in periodicals archive

In practice, most equational logic programs are constructor-based; symbols, called constructors, that construct data terms are distinguished from those, called defined functions or operations, that operate on data terms (see, e.g., the Equational Interpreter [O'Donnell 1985] and the functional logic languages ALF [Hanus 1990], BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992], K-LEAF [Giovannetti et al.

Programming in equational logic: Beyond strong sequentiality.

A Needed Narrowing Strategy

For recent notable work, I focus on some significant theorem-proving systems: the geometry theorem provers of Chou (Chou, Gao, and Zhang 1994; Chou 1988); the Boyer and Moore (1988) interactive theorem prover NQTHM and its successor ACL2 (Kaufmann and Moore 1996); the rewrite rule laboratory (RRL) of Kaput and Zhang (1995); the resolution prover OTTER (McCune and Otter 1997; McCune 1994) and the equational logic prover EQP by McCune (1996); the interactive higher-order logic provers NUPRL (Constable et al.

I mentioned that the term-rewriting community is central to the work in equational logics. This point warrants elaboration.

Automated Deduction Looking Ahead

Incremental constraint satisfaction for equational logic programming.

Partial Evaluation of Functional Logic Programs

But it seems that the complexity of the equational logic of nondeterminism exceeds by far the complexity of classical equational reasoning.

Algebraic approaches to nondeterminism: an overview

In summary, the declarative control architecture implements, with an equational logic formalism, a combination of planning, inference and feedback control principles.

Declarative control architecture

PIM is an equational logic designed to function as a "transformational toolkit" for compilers and other programming tools that analyze and manipulate imperative languages.

This article is an effort to contribute to a better understanding of these issues by presenting a formal account of properties of an equational logic called PIM [Field 1992].

Toward a complete transformational toolkit for compilers