Siekmann, J. H. (Ed.): 8th International Conference on Automated Deduction. Oxford, England, July 27–August 1, 1986, Proceedings. Lecture Notes in Computer Science Vol. 230. Springer-Verlag, Berlin – Heidelberg – New York – Tokyo 1986, IX, 708 pp., DM 96,– ISBN 3-540-16780-3
✍ Scribed by D. Seese
- Publisher
- John Wiley and Sons
- Year
- 1988
- Tongue
- English
- Weight
- 184 KB
- Volume
- 30
- Category
- Article
- ISSN
- 0323-3847
No coin nor oath required. For personal study only.
✦ Synopsis
Part two bantains four lectures. G. Huet: Deduction and Computation, 31. E. Stickel: An Introduction to Automated Deduction, A W. Biermann: Fundamental Mechanisms in Machine Learning and Inductive Inference and W. Bibel: Methods of Automated b o n i n g . The first lecture introduces formal IanguagM and their syntax and inference rulss and handles rewriting inference and equational logic, confluence and termination, the Knuth-Bendix theorem, sequential computations, I-calculus, GentZen's natural deduction. Milner's Theorem and ends with a sketch on some development8 concerning dependent types. In the second lecture all essential aspects of resolution, unification and equality reasoning, as e.g. Prolog, linear resolution, connection method, nonclausal resolution, theory resolution, commutative, associative and many-sorted unification, demodulation, poramodulation and Knuth-Bendix method are presented. The third lecture treats the learning of finite functions and of grammars, the infering of programs from computation trcrces, the construction of LISP programs from example input-output behaviors and the synthesis of PROLOG programs from examples. In the last lecture of the second part non-monotonic reasoning, negation as failure circumscription, meta-reasoning and reaeoning about uncertainty as e.g. Bayesian inference and fuzzy logic are handled. Part three contains two Iecturck: Ph. Jorrand: Term %writing as a Basis for the Design of a Functional 8ndParal~e~ Programming Language. A case study: the language FP2 and E. Shapiro: Concurrent PROLOG: A Progreee Report.