상세정보

Program synthesis is a solution to the software crisis. If we had a program that develops correct programs from specifications, then program validation and maintenance would disappear from the software life-cycle, and one could focus on the more creative tasks of specification elaboration, validation, and maintenance, because replay of program development would be less costly.
This monograph describes a novel approach to Inductive Logic Programming (ILP), which cross-fertilizes logic programming and machine learning. Aiming at the synthesis of recursive logic programs only, and this from incomplete information, we take a software engineering approach that is more appropriate than a pure artificial intelligence approach.
This book is suitable as a secondary text for graduate level courses in software engineering and artificial intelligence, and as a reference for practitioners of program synthesis.

Program synthesis is a solution to the software crisis. If we had a program that develops correct programs from specifications, then program validation and maintenance would disappear from the software life-cycle, and one could focus on the more creative tasks of specification elaboration, validation, and maintenance, because replay of program development would be less costly.
This monograph describes a novel approach to Inductive Logic Programming (ILP), which cross-fertilizes logic programming and machine learning. Aiming at the synthesis of recursive logic programs only, and this from incomplete information, we take a software engineering approach that is more appropriate than a pure artificial intelligence approach.
This book is suitable as a secondary text for graduate level courses in software engineering and artificial intelligence, and as a reference for practitioners of program synthesis.

정보제공 :

CONTENTS
Lists of Logic Algorithms, Figures, and Tables = ⅸ
Foreword = xi
Preface = xiii
Ⅰ STATE OF THE ART
  1 Automatic programming = 3
    1.1 The Grand Aim of Automatic Programming = 3
    1.2 Specification, Algorithm, and Programming Languages = 6
    1.3 A Classification of Synthesis Mechanisms = 10
    1.4 Requirements and Promises of Automatic Programming = 11
    1.5 Sample Problems = 13
  2 Deductive Inference in Automatic Programming = 15
    2.1 Specifications by Axioms = 15
    2.2 Deductive Inference = 18
      2.2.1 Transformational Synthesis = 18
      2.2.2 Proofs-as-Programs Synthesis = 19
      2.2.3 Schema-Guided Synthesis = 21
    2.3 Functional Program Synthesis from Axioms = 21
      2.3.1 Transformational Synthesis of LISP Programs = 21
      2.3.2 Proofs-as-Programs Synthesis of LISP Programs = 22
      2.3.3 Schema-Guided Synthesis of LISP Programs = 23
    2.4 Logic Program Synthesis from Axioms = 23
      2.4.1 Transformational Synthesis of Prolog Programs = 24
      2.4.2 Proofs-as-Programs Synthesis of Prolog Programs = 26
      2.4.3 Schema-Guided Synthesis of Prolog Programs = 27
    2.5 Conclusions on Program Synthesis from Axiomatizations = 28
  3 Inductive Inference in Autornatic Programming = 29
    3.1 Specifications by Examples = 29
    3.2 Inductive Inference = 32
      3.2.1 Components of a Learning System = 33
      3.2.2 Rules of Inductive Inference = 33
      3.2.3 Empirical Learning from Examples = 34
      3.2.4 Algorithm Synthesis from Examples as a Niche of = 39
      3.2.5 Pointers to the Literature = 41
    3.3 Functional Program Synthesis from Examples = 42
      3.3.1 Synthesis from Traces = 42
      3.3.2 Trace-Based Synthesis from Examples = 42
      3.3.3 Heuristic Synthesis from Examples = 45
    3.4 Logic Program Synthesis from Examples = 46
      3.4.1 Shapiro's Model Inference System = 46
      3.4.2 Other Model-Based Synthesis Systems = 51
    3.5 Conclusions on Program Synthesis from Examples = 52
  4 A Logic Program Development Methodology = 55
    4.1 Elaboration of a Specification = 56
    4.2 Design of a Logic Algorithm = 56
    4.3 Transformation of a Logic Algorithm = 61
    4.4 Derivation of a Logic Program = 61
    4.5 Transformation of a Logic Program = 62
  5 Objectives = 63
    5.1 Precise Statement of the Objective = 63
    5.2 Motivating Examples = 64
      5.2.1 Sample Logic Algorithms = 64
      5.2.2 Some Comments on Logic Algorithms = 71
    5.3 Challenges = 75
Ⅱ BUILDING BLOCKS
  6 A Specification Approach = 79
    6.1 Specifications by Examples and Properties = 79
    6.2 Sample Specifications by Examples and Properties = 80
    6.3 Future Work = 83
    6.4 Related Work = 83
    6.5 Conclusion = 84
  7 A Framework for Stepwise Logic Algorithm Synthesis = 85
    7.1 Correctness of Logic Algorithms = 85
      7.1.1 Logic Algorithm and Intentions = 87
      7.1.2 Logic Algorithm and Specification = 89
      7.1.3 Specification and Intentions = 90
    7.2 Comparison of Logic Algorithms = 90
      7.2.1 Semantic Generalization = 9l
      7.2.2 Syntactic Generalization = 91
    7.3 Stepwise Logic Algorithm Synthesis Strategies = 93
      7.3.1 An Incremental Synthesis Strategy = 93
      7.3.2 A Non-Incremental Synthesis Strategy = 94
    7.4 Future Work = 99
    7.5 Related Work = 99
    7.6 Conclusion = 100
  8 Algorithm Analysis and Algorithm Schemata = 101
    8.1 Introduction to Algorithm Schemata = 101
    8.2 A Divide-and-Conquer Logic Algorithm Schema = 103
      8.2.1 Divide-and-Conquer Logic Algorithm Anal = 104
      8.2.2 Integrity Constraints on Instances = 107
      8.2.3 Justifications = 108
      8.2.4 Discussion 109
    8.3 Stepwise, Schema-Guided Logic Algorithm Syntheis = 110
    8.4 Future Work = 111
    8.5 Related Work = l12
    8.6 Conclusion = 114
  9 The Proofs-as-Programs Method = 115
    9.1 The Problem = 1l5
    9.2 A Method = 116
    9.3 Correctness = 122
    9.4 Illustration = 123
    9.5 Future Work = 130
    9.6 Related Work = 130
    9.7 Conclusion = 132
  10 The Most-Specific-Generalization Method = 133
    10.1 Most-Specific-Generalization of Terms = 133
    10.2 Objective and Terminology = 134
    10.3 The Ground Case = 136
    10.4 The Non-Ground Case = 139
    10.5 Future Work = 142
    10.6 Related work = 143
    10.7 Conclusion = 144
Ⅲ A LOGIC ALGORITHM SYNTHESIS MECHANISM
  11 Overview of the Synthesis Mechanism = 147
    11.1 Desired Features = 147
    11.2 Preliminary Restrictions = 151
    11.3 A Sample Synthesis = 152
  12 The Expansion Phase = 159
    12.1 Step l : Syntactic Creation of a First Approximation = 160
    12.2 Step 2 : Synthesis of Minimal and NonMinimal = 161
    12.3 Step 3 : Synthesis of Decompose = 166
    12.4 Step4 : Syntactic Introduction of the Recursive Atcms = 171
  13 The Reduction Phase = 175
    13.1 Step 5 : Synthesis of Solver and the SolveNonMin(k) = 175
    13.2 Step 6 : Synthesis of the Process(k)and Compose(k) = 181
    13.3 Step 7 : Synthesis of the Discriminate(k) = 186
  14 Conclusion = 191
    14.1 Summary = 191
    14.2 Extensions = 196
      14.2.1 Negation = 196
      14.2.2 Auxiliary Parameters = 197
      14.2.3 Supporting Other Schemata = 198
      14.2.4 The Synthesis Method = 198
    14.3 A Methodology for Choosing "Good" Examples and Pro = 204
    14.4 The SYNAPSE System = 206
      14.4.1 The Architecture of SYNAPSE = 206
      14.4.2 Target Scenarios for SYNAPSE = 207
    14.5 Evaluation = 211
      14.5.1 Insights = 211
      14.5.2 Comparison with Related Systems = 213
Appendix Conventions, Abbreviations, and symbols = 215
References = 219
Subject Index = 235
List of Logic Algorithms
Logic Algorithm 4-1 : LA(compress) = 57
Logic Algorithm 4-2 : LA(firstPlateau) = 57
Logic Algorithm 4-3 : LA(compress-int-L) = 61
Logic Algorithm 5-1 : LA(compress-ext-L) = 64
Logic Algorithm 5-2 : LA(compress-int-C) = 65
Logic Algorithm 5-3 : LA(compress-ext-C) = 65
Logic Algorithm 5-4 : LA(delOddElems-L) = 66
Logic Algorithm 5-5 : LA(efface-L) = 66
Logic Algorithm 5-6 : LA(firstN-L) = 66
Logic Algorithm 5-7 : LA(firstN-N) = 67
Logic Algorithm 5-8 : LA(insert-L) = 67
Logic Algorithm 5-9 : LA(insert-R) = 67
Logic Algorithm 5-10 : LA(member-L) = 68
Logic Algorithm 5-11 : LA(merge-) = 68
Logic Algorithm 5-12 : LA(parity-L) = 69
Logic Algorithm 5-13 : LA(partition-L) = 69
Logic Algorithm 5-14 : LA(permutation-L) = 69
Logic Algorithm 5-15 : LA(plateau-N) = 70
Logic Algorithm 5-16 : LA(sort-int-L) {Insertion-Sort} = 70
Logic Algorithm 5-17 : LA(sort-ext-L) {Quick-Sort} = 70
Logic Algorithm 5-18 : LA(sort-ext-L) {Merge-Sort} = 70
Logic Algorithm 5-19 : LA(split) = 71
Logic Algorithm 12-1 : LA₁(firstPlateau) = 161
Logic Algorithm 12-2 : exp(LA₁(fristPlateau)) = 161
Logic Algorithm 12-3 : LA₂(firstPlateau) = 166
Logic Algorithm 12-4 : exp(LA₂(firstPlateau)) = 166
Logic Algorithm 12-5 : LA₃(firstPlateau) = 170
Logic Algorithm 12-6 : exp(LA₃(firstPlateau)) = 170
Logic Algorithm 12-7 : LA₄(firstPlateau) = 174
Logic Algorithm 12-8 : exp(LA₄(firstPlateau)) = 174
Logic Algorithm 13-1 : LA5 (firstPlateau) = 180
Logic Algorithm 13-2 : exp( LA5 (firstPlateau)) = 180
Logic Algorithm 13-3 : LA6 (firstPlateau) = 185
Logic Algorithm 13-4 : exp( LA6 (firstPlateau)) = 185
Logic Algorithm 13-5 : LA7 (firstPlateau) = 190
Logic Algorithm 13-6 : exp( LA7 (firstPlateau)) = 190