Computing in Horn Clause Theories - Peter Padawitz

. .

Sommaire:
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.