Abstract
It has been recognized for some time that Prolog will need to be extended in order for it to realize the vision of declarative programming. One example is the so-called problem of equality and functions. The underlying deduction mechanism for Prolog, SLD-resolution, is defined only for languages without equality. As mentioned in chapter 1, current Prolog systems include a collection of interpretations of the equality symbol which are basically inherited from LISP, and that it is even possible for the “equality” predicate to cause the side-effect of binding an uninstantiated variable to an instantiated variable. The absence of equality also means that value-returning functions cannot be defined equationally. Instead, an n-ary function f(x 1,..., x, n ) is defined by an n+1-ary predicate p(x 1,..., x n , x n+l) which “collects” the value in the n + 1st argument. In order for Prolog to reason equationally, rules for rewriting one term to another must be expressed via a distinguished predicate (say rewrite).
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer Science+Business Media New York
About this chapter
Cite this chapter
Raatz, S. (1990). An Equational Extension. In: Graph-Based Proof Procedures for Horn Clauses. Progress in Computer Science and Applied Logic, vol 10. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4899-3556-4_6
Download citation
DOI: https://doi.org/10.1007/978-1-4899-3556-4_6
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-0-8176-3530-5
Online ISBN: 978-1-4899-3556-4
eBook Packages: Springer Book Archive