Computing in Horn Clause Theories. (= EATCS monographs on theoretical computer sciences, Vol. 16). - gebunden oder broschiert

EAN (ISBN-13): 9783540194279
ISBN (ISBN-10): 3540194274
Gebundene Ausgabe
Taschenbuch
Erscheinungsjahr: 1988
Herausgeber: Springer

Buch in der Datenbank seit 2008-04-26T00:06:40+02:00 (Zurich)
Detailseite zuletzt geändert am 2024-03-27T22:37:52+01:00 (Zurich)
ISBN/EAN: 3540194274

ISBN - alternative Schreibweisen:
3-540-19427-4, 978-3-540-19427-9
Alternative Schreibweisen und verwandte Suchbegriffe:
Autor des Buches: horn, padawitz, computing
Titel des Buches: theoretical computer science, computing, peter horn, theorie der metapher, berlin, clause, monographs, theories theories

---

Daten vom Verlag:

Autor/in: Peter Padawitz
Titel: Monographs in Theoretical Computer Science. An EATCS Series; Computing in Horn Clause Theories
Verlag: Springer; Springer Berlin
322 Seiten
Erscheinungsjahr: 1988-08-25
Berlin; Heidelberg; DE
Gedruckt / Hergestellt in Deutschland.
Gewicht: 0,700 kg
Sprache: Englisch
85,55 € (DE)
87,95 € (AT)
88,00 CHF (CH)
Not available, publisher indicates OP

BB; Book; Hardcover, Softcover / Informatik, EDV/Informatik; Computerprogrammierung und Softwareentwicklung; Verstehen; Resolution; program transformation; logic; semantics; programming; language; algorithm; Boolean algebra; Natural; palindrome; algorithms; Computer Science; B; Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Mathematical Logic and Formal Languages; Computation by Abstract Devices; Logics and Meanings of Programs; Software Engineering; Programmier- und Skriptsprachen, allgemein; Compiler und Übersetzer; Theoretische Informatik; Interfacedesign, Benutzerfreundlichkeit (Usability); Computerprogrammierung und Softwareentwicklung; Rechnerarchitektur und Logik-Entwurf; BC; EA

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.