|
Note that this HTML page was
generated from Word 2000. Some
of the code cannot be pasted into Qi. You are advised to download the program
files through the above link. Contents Part I The Core Language 1.1 Declarative Programming 1.2 Mathematical Foundations 1.3 The American Experience 1.4 The British Experience 1.5 SEQUEL – the predecessor of Qi 1.6 The deficiencies of SEQUEL 1.7 The
Evolution of Qi in Britain 1.8
The Evolution of Qi in America 2.1 Starting Up 2.2 Applying Functions 2.3 Repeating Evaluations 2.4 Input/Output 2.5 Strict and Non-Strict Evaluation 2.6 Boolean Operations 2.7 Defining New Functions 2.8 Equations and Priority Rewrite Systems 2.9 A Fruit Machine Program 3.1
Recursion and Infinity 3.2 Tail and Linear Recursion 3.3 Tree Recursion 3.4 Guards 3.5 Mutual Recursion 3.6 Counting Change 3.7 Non-terminating Functions 4.1 Representing Lists in Qi 4.2 Building Lists with Cons 4.3 | is Shorthand for Cons 4.4 Head and Tail Access Parts of
Lists 4.5 Characters 4.6 Recursive List Processing 4.7 Local Assignments 4.8 Goldbach’s Conjecture Revisited Chapter 5 Higher Order
Programming 5.1 Higher Order Functions 5.2 Abstractions, Currying and Partial Applications 5.3 Using Abstractions in Higher Order Programs 5.4 Getting Rid of One-Off Functions 5.5 Taking Advantage of Similarities 5.6 Using Functions as Data 6.1
Simple Assignments 6.2 Arrays 6.3 Property Lists 6.4 Building Semantic Nets 7.1 Non-deterministic Algorithms 7.2 Backward Chaining 7.3 Representing Proof Trees 7.4 Chronological Backtracking in Qi 7.5 Soundness and Completeness 7.6 Writing Refinement Rules: a
Preview 7.7 Selecting the Failure Object 7.8 The Static Elimination of Backtracking in Qi 8.1 Building a Parser in Qi 8.2 Recursive Descent Parsing in Qi 8.3 The eval Function Chapter 9 Writing Good Programs Part II Working with Types 10.1
Types and Type Security 10.2 Modifying the Read-Evaluate-Print
Loop 10.3 Base Types and Operators 10.4 The list Type Operator 10.5 The Function Space Operator ® 10.6 The Product Type Operator * 10.7 Polytypes 10.8 Using Type Checking 10.9 Loading Files 11.1 Enumeration Types 11.2 Side Conditions 11.3 Synonyms 11.4 Left and Right Rules 11.5 Defining Recursive Types 11.6 Simulating a Calculator 11.7 Verified Objects 11.8 Defining Type Operators 11.9 Working with Functions Other than
Cons 11.10 Subtypes 11.11 Type Checking Assignments 11.12 Structures 11.13
Abstract Datatypes 12.1 The Lambda Calculus 12.2 Reasoning with the Lambda Calculus 12.3 The Church-Rosser Theorems 12.4 Representing Things in Lambda
Calculus 12.5 Recursion and the Y-combinator 12.6 From Lambda Calculus to
Functional Programming 12.7 The Compilation of Qi to L 12.8 The Compilation of L
to Lambda Calculus Chapter 13 Type Checking as Proof 13.1 The Qi Type System 13.2 Type Checking Applications 13.3 Choosing Values by Unification 13.4 Type Checking Abstractions 13.5 Polymorphic Functions 13.6 Typing Special Forms 13.7 Internal Forms 13.8 Mutual Recursion 13.9 Global Variables 13.10 Procedure T* 13.11 From Type Checking to Automated
Deduction Part III Automated Reasoning,
Expert Systems and Intelligent Agents 14.1 Building Automated Theorem
Provers 14.2 Proof Systems 14.3 Propositional Calculus 14.4 Propositional Calculus in Qi 14.5 The Proof Tool 14.6 Solving Goals in Qi 14.7 A Decision Procedure for PC 14.8 Expressing our Heuristics for PC in Qi 14.9 Special Variables 14.10 Modal Logic and Non-Monotonic Logic 15.1 The Syntax and Proof Theory of
FOL 15.2 Expressing FOL in Qi 15.3 Coding Quantifier Refinement
Rules 15.4 A Simple Proof in First-Order
Logic 15.5 Automating Proof in FOL 15.6 Skolemisation 15.7 Prenex Form 15.8 Rectification 15.9 Universal Quantifiers and
Unification 15.10 Skolemisation in Sequent Systems 15.11 Clause Form 15.12 The Refinement Rules for
AUTOFOL 15.13 Representing Bindings with the
Notepad 15.14 Some AUTOFOL Proofs 15.15 The Incompleteness of AUTOFOL 15.16 A Complete AUTOFOL 15.17 Optimising AUTOFOLC |