Computing in Horn Clause Theories

Computing in Horn Clause Theories by Peter Padawitz.

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 functi...

Full description

Saved in:
Bibliographic Details
Main Author: Padawitz, Peter (Author)
Corporate Author: SpringerLink (Online service)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1988.
Edition:1st ed. 1988.
Series:Monographs in Theoretical Computer Science. An EATCS Series, 16
Springer eBook Collection.
Subjects:
Computer programming.
Software engineering.
Programming languages (Electronic computers).
Mathematical logic.
Computers.
Computer logic.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • 1 Introduction
  • 2 Basic Notions
  • 2.1 Preliminaries
  • 2.2 The Syntax of Specifications
  • 2.3 Models of a Specification
  • 3 Sample Specifications
  • 3.1 Boolean Algebra
  • 3.2 Arithmetic
  • 3.3 Program Transformations
  • 3.4 A Store-based Language Interpreter
  • 3.5 Binary Numbers
  • 3.6 Decoding Binary Numbers
  • 3.7 Sequences
  • 3.8 Palindromes
  • 3.9 Sorting
  • 3.10 Unordered Combinations
  • 3.11 Binary Trees
  • 3.12 Search Trees
  • 3.13 2-3 Trees
  • 3.14 Tree Domains
  • 3.15 A Stream Language Interpreter
  • 4 Models and Theories
  • 4.1 Introduction
  • 4.2 The Horn Clause Calculus
  • 4.3 Initial Semantics
  • 4.4 Initial Correctness
  • 4.5 Final Semantics
  • 4.6 Final Correctness
  • 4.7 The Refutation of Inductive Theorems
  • 4.8 Internalized Logic
  • 4.9 Horn Clause Versus Sequent Logic
  • 4.10 Bibliographic Notes
  • 5 Resolution and Paramodulation
  • 5.1 Introduction
  • 5.2 Resolution
  • 5.3 Paramodulation
  • 5.4 Most General Unification
  • 5.5 Lazy Resolution
  • 5.6 Bibliographic Notes
  • 6 The Relevance of Constructors
  • 6.1 Introduction
  • 6.2 Partial Semantics
  • 6.3 Inductionless Induction
  • 6.4 Bibliographic Notes
  • 7 Reduction
  • 7.1 Introduction
  • 7.2 The Classical Approach
  • 7.3 The Congruence Class Approach
  • 7.4 The Normal Form Approach
  • 7.5 The Weak Normal Form Approach
  • 7.6 From Equations to Horn Clauses
  • 7.7 Term and Goal Reduction
  • 7.8 Confluence Properties
  • 7.9 Strategy-controlled Reduction
  • 7.10 Basic Reduction
  • 7.11 Bibliographic Notes
  • 8 Narrowing
  • 8.1 Introduction
  • 8.2 The Narrowing Calculus
  • 8.3 Strategy-controlled Narrowing
  • 8.4 Narrowing Strategies
  • 8.5 Ground Term Generating Term Sets
  • 8.6 Basic Narrowing
  • 8.7 Reduced Narrowing
  • 8.8 Reduced Basic Narrowing
  • 8.9 Optimized Narrowing
  • 8.10 Optimizing Functions
  • 8.11 Lazy Narrowing
  • 8.12 Bibliographic Notes
  • 9 Church-Rosser Criteria
  • 9.1 Introduction
  • 9.2 Fully Parallel and Overlapping Reductions
  • 9.3 Convergence Properties
  • 9.4 Critical Pairs
  • 9.5 Confluence of NAX
  • 9.6 Strong Confluence of NAX
  • 9.7 Confluence of ̃NAX
  • 9.8 BAX-compatibilityof NAX
  • 9.9 An Algorithm for Church-Rosser Proofs
  • 9.10 Bibliographic Notes
  • References
  • Notation Index
  • Definition Index.

Similar Items