Chapter
1.4 Representing symbolic objects
1.5 Unification of typed first-order terms
2 First-Order Horn Clauses
2.2 Logic programming and search semantics
2.3 Horn clauses and their computational interpretation
2.4 Programming with first-order Horn clauses
2.4.1 Concrete syntax for program clauses
2.4.2 Interacting with the λProlog system
2.4.3 Reachability in a finite-state machine
2.4.4 Defining relations over recursively structured data
2.4.5 Programming over abstract syntax representations
2.5 Pragmatic aspects of computing with Horn clauses
2.6 The relationship with logical notions
2.6.1 The cut rule and cut-elimination
2.6.2 Different presentations of fohc
2.7 The meaning and use of types
2.7.1 Types and the categorization of expressions
2.7.3 Type checking and type inference
2.7.4 Types and run-time computations
3: First-Order Hereditary Harrop Formulas
3.1 The syntax of goals and program clauses
3.2.1 Inferences among propositional clauses
3.2.2 Hypothetical reasoning
3.3 Universally quantified goals
3.3.1 Substitution and quantification
3.3.2 Quantification can link goals and clauses
3.4 The relationship with logical notions
3.4.1 Classical versus intuitionistic logic
3.4.2 Intuitionistic versus minimal logic
3.4.3 Notable subsets of fohh
4: Typed λ-Terms and Formulas
4.1 Syntax for λ-terms and formulas
4.2 The rules of λ-conversion
4.3 Some properties of λ-conversion
4.4 Unification problems as quantified equalities
4.4.1 Simplifying quantifier prefixes
4.4.2 Unifiers, solutions, and empty types
4.4.3 Examples of unification problems and their solutions
4.5 Solving unification problems
4.6 Some hard unification problems
4.6.1 Solving Post correspondence problems
4.6.2 Solving Diophantine equations
5 Using Quantification at Higher-Order Types
5.1 Atomic formulas in higher-order logic programs
5.1.1 Flexible atoms as heads of clauses
5.1.2 Logical symbols within atomic formulas
5.2 Higher-order logic programming languages
5.2.1 Higher-order Horn clauses
5.2.2 Higher-order hereditary Harrop formulas
5.2.3 Extended higher-order hereditary Harrop formulas
5.3 Examples of higher-order programming
5.4 Flexible atoms as goals
5.5 Reasoning about higher-order programs
5.6 Defining some of the logical constants
5.7 The conditional and negation-as-failure
5.8 Using λ-terms as functions
5.8.1 Some basic computations with functional expressions
5.8.2 Functional difference lists
5.9 Higher-order unification is not a panacea
5.10 Comparison with functional programming
6: Mechanisms for Structuring Large Programs
6.1 Desiderata for modular programming
6.3 Matching signatures and modules
6.4 The logical interpretation of modules
6.4.1 Existential quantification in program clauses
6.4.2 A module as a logical formula
6.4.3 Interpreting queries against modules
6.4.4 Module accumulation as scoped inlining of code
6.5 Some programming aspects of the modules language
6.5.1 Hiding and abstract datatypes
6.5.2 Code extensibility and modular composition
6.5.3 Signature accumulation and parametrization of modules
6.5.4 Higher-order programming and predicate visibility
6.6 Implementation considerations
7: Computations over λ-Terms
7.1 Representing objects with binding structure
7.1.1 Encoding logical formulas with quantifiers
7.1.2 Encoding untyped λ-terms
7.1.3 Properties of the encoding of binding
7.2 Realizing object-level substitution
7.4 Computing with untyped λ-terms
7.4.1 Computing normal forms
7.4.2 Reduction based on paths through terms
7.4.4 Translating to and from de Bruijn syntax
7.5 Computations over first-order formulas
7.6 Specifying object-level substitution
7.7 The λ-tree approach to abstract syntax
7.8 The Lλ subset of λProlog
8: Unification of λ-terms
8.1 Properties of the higher-order unification problem
8.2 A procedure for checking for unifiability
8.2.1 Simplification of rigid-rigid equations
8.2.2 Substitutions for equations between flexible and rigid terms
8.2.3 The iterative transformation of unification problems
8.2.4 Unification problems with only flexible-flexible equations
8.2.5 Nontermination of reductions
8.3 Higher-order pattern unification
8.4 Pragmatic aspects of higher-order unification
9: Implementing Proof Systems
9.1 Deduction in propositional intuitionistic logic
9.2 Encoding natural deduction for intuitionistic logic
9.3 A theorem prover for classical logic
9.4 A general architecture for theorem provers
9.4.2 Combining tactics into proof strategies
10: Computations over Functional Programs
10.1 The miniFP programming language
10.2 Specifying evaluation for miniFP programs
10.2.1 A big-step-style specification
10.2.2 A specification using evaluation contexts
10.3 Manipulating functional programs
10.3.1 Partial evaluation of miniFP programs
10.3.2 Transformation to continuation passing style
11: Encoding a Process Calculus Language
11.1 Representing the expressions of the π-calculus
11.2 Specifying one-step transitions
11.3 Animating π-calculus expressions
11.4 May- versus must-judgments
11.5 Mapping the λ-calculus into the π-calculus
Appendix: The Teyjus system
A.1 An overview of the Teyjus system
A.2 Interacting with the Teyjus system
A.3 Using modules within the Teyjus system
A.4 Special features of the Teyjus system
A.4.1 Built-in types and predicates
A.4.2 Deviations from the language assumed in this book
Programming with Higher-Order Logic
Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.