Skip to main content
SpringerLink
Log in

Foundations of Equational Logic Programming

  • Book
  • © 1989

Overview

Editors:
  1. Steffen Hölldobler
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 353)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
Softcover Book USD 37.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (9 chapters)

  1. Front Matter

    Download chapter PDF

  2. Introduction

    Pages 1-14

  3. Preliminaries

    Pages 15-23

  4. Equational Logic Programming

    Pages 24-64

  5. Universal Unification

    Pages 65-75

  6. SLDE-Resolution

    Pages 76-84

  7. Paramodulation

    Pages 85-173

  8. Universal Unification by Complete Sets of Transformations

    Pages 174-200

  9. Lazy Resolution and Complete Sets of Inference Rules for Horn Equational Theories

    Pages 201-207

  10. Conclusion

    Pages 208-230

  11. Back Matter

    Download chapter PDF
Back to top

Keywords

About this book

Equations play a vital role in many fields of mathematics, computer science, and artificial intelligence. Therefore, many proposals have been made to integrate equational, functional, and logic programming. This book presents the foundations of equational logic programming. After generalizing logic programming by augmenting programs with a conditional equational theory, the author defines a unifying framework for logic programming, equation solving, universal unification, and term rewriting. Within this framework many known results are developed. In particular, a presentation of the least model and the fixpoint semantics of equational logic programs is followed by a rigorous proof of the soundness and the strong completeness of various proof techniques: SLDE-resolution, where a universal unification procedure replaces the traditional unification algorithm; linear paramodulation and special forms of it such as rewriting and narrowing; complete sets of transformations for conditional equational theories; and lazy resolution combined with any complete set of inference rules for conditional equational theories.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation