Skip to main content
SpringerLink
Log in

Computing in Horn Clause Theories

  • Textbook
  • © 1988

Overview

Authors:
  1. Peter Padawitz

    1. Fakultät für Mathematik und Informatik, Universität Passau, Passau, Germany

    View author publications

    You can also search for this author in PubMed   Google Scholar

Part of the book series: Monographs in Theoretical Computer Science. An EATCS Series (EATCS, volume 16)

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

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.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

    Pages I-XI
    Download chapter PDF

  2. Introduction

    • Peter Padawitz
    Pages 1-5

  3. Basic Notions

    • Peter Padawitz
    Pages 7-13

  4. Sample Specifications

    • Peter Padawitz
    Pages 15-52

  5. Models and Theories

    • Peter Padawitz
    Pages 53-111

  6. Resolution and Paramodulation

    • Peter Padawitz
    Pages 113-137

  7. The Relevance of Constructors

    • Peter Padawitz
    Pages 139-152

  8. Reduction

    • Peter Padawitz
    Pages 153-186

  9. Narrowing

    • Peter Padawitz
    Pages 187-240

  10. Church-Rosser Criteria

    • Peter Padawitz
    Pages 241-305

  11. Back Matter

    Pages 307-322
    Download chapter PDF
Back to top

Keywords

About this book

At least four research fields detennine the theoretical background of specification and deduction in computer science: recursion theory, automated theorem proving, abstract data types and tenn rewriting systems. As these areas approach each other more and more, the strong distinctions between functional and relational views, deductive and denotational approaches as well as between specification and programming are relieved in favour of their integration. The book will not expose the lines of this development; conversely, it starts out from the nucleus of Hom clause logic and brings forth both known and unknown results, most of which affect more than one of the fields mentioned above. Chapter 1 touches on historical issues of specification and prototyping and delimits the topics handled in this book from others which are at the core of related work. Chapter 2 provides the fundamental notions and notations needed for the presentation and interpretation of many-sorted Horn clause theories with equality. Chapter 3 supplies a number of sample Hom clause specifications ranging from arithmetic through string manipulation to higher data structures and interpreters of programming languages. Some of these examples serve as a reference to illustrate definitions and results, others may throw a light on the strong link between specifications and programs, which are executed by applying deduction rules. Thus we have included examples of how to use program trans/ormation methods in specification design.

Authors and Affiliations

  • Fakultät für Mathematik und Informatik, Universität Passau, Passau, Germany

    Peter Padawitz

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation