RESTIVO@SU-SCORE.ARPA (05/06/85)
From: Chuck Restivo (The Moderator) <PROLOG-REQUEST@SU-SCORE.ARPA>
PROLOG Digest Monday, 6 May 1985 Volume 3 : Issue 21
Today's Topics:
Announcement - Workshop,
Implementation - Control & CP,
LP Library - Manna Book
----------------------------------------------------------------------
Date: Wed, 1 May 85 19:01:22 -0200
From: Ehud Shapiro <Udi%Wisdom.bitnet@WISCVM.ARPA>
Subject: Workshop
As a welcome party for the summer and for our summer
students, guests, and visitors, we will hold on Tuesday
and Wednesday, June 28 and 29, and informal workshop on
"Logic Programming and Parallel Processing". If you
plan to be in Israel during that time, and would like
to participate and/or contribute, please let me know.
-- Ehud Shapiro
------------------------------
Date: 2 May 1985 0843-CDT
From: THRIFT%TI-CSL.CSNet@csnet-relay.arpa
Subject: Control annotation in CP
In reference to a previous note on control annotation
for CP:
I have been made aware that the 'mode annotation' for
procedure heads (input and output restrictions) was
first made in IC-Prolog. The annotation here is '?' for
input and '^' for output.
For example (Clark,K.L. "Predicate Logic as a
Computational Formalism")
append([X1|X]?,Y?,[Z1|Z]^) :- append(X,Y,Z).
restricts the use of this clause to a case where the
first two arguments are input and the third is output.
My apologies for missing this.
Although I realize that the control achieved through the
read-only annotation is greater than that achieved by
the mode annotation, I would like to see a practical
(that is, not 'artificial') example showing this.
------------------------------
Date: 03 May 85 1425 PDT
From: Yoni Malachi <YM@SU-AI.ARPA>
Subject: More details on "The Logical Basis for
THE LOGICAL BASIS FOR COMPUTER PROGRAMMING
Volume 1: Deductive Reasoning
ZOHAR MANNA and RICHARD WALDINGER
Addison-Wesley, ISBN: 0-201-18620-2
This exceptionally clear text, laced with many examples,
provides a most readable introduction to the logical
concepts and techniques underlying computer programming.
Computational notions are explored in a logical realm
independent of any programming language or any machine.
The text is accessible to readers with no background in
mathematics or computer programming, yet it supplies
axiomatization for a rich collection of abstract data
types.
This book provides the intellectual tools for studying
artificial intelligence, software engineering, automatic
programming, database theory, logic programming, and the
theory of computation.
A forthcoming second volume, DEDUCTIVE SYSTEMS, describes
logical techniques for automated theorem proving and its
applications.
The Authors:
ZOHAR MANNA is Professor of Computer Science at Stanford
University; he is the author of the textbook "Mathematical
Theory of Computation."
RICHARD WALDINGER is Staff Scientist in the Artificial
Intelligence Center at SRI International.
TABLE OF CONTENTS:
Part I. Mathematical Logic
Chapter 1: Propositional Logic
Introduction. The Language. The Meaning of a Sentence.
Properties of Sentences. Truth Tables. Semantic Trees.
Proof by Falsification. Valid Sentence Schemata.
Substitution. Extended Interpretation. Equivalence.
Problems.
Chapter 2: Predicate Logic: Basic
Introduction. The Language. The Meaning of a Sentence.
Semantic Rules. Validity. Universal and Existential
Closure. Problems.
Chapter 3: Predicate Logic: Advanced
Valid Sentence Schemata. Equivalence. Safe Substitution.
The Value Property. Valid Schemata with Substitution.
Function Introduction and Elimination.
Problems.
Chapter 4: Special Theories
Definition of a Theory. Augmenting Theories. Relationship
between Theories. Theory of Strict Partial Orderings.
Theory of Equivalence Relations. Problems.
Chapter 5: Theories with Equality
Theory of Equality. Theory of Weak Partial Orderings.
Theory of Associated Relations. Theory of Groups. Theory
of Pairs. Relativized Quantifiers. The Lexicographic
Relation. Problems.
Part II. Theories with Induction
Chapter 6: Nonnegative Integers
Basic Properties. The Addition Function. Multiplication
and Exponentiation. Predecessor and Subtraction.
Decomposition Induction. The Weak Less-than Relation.
The Strict Less-than Relation. Complete Induction.
Quotient and Remainder. Proof of Complete Induction. The
Divides Relation. The Least-Number Principle. Problems.
Chapter 7: Strings
Basic Properties. The Head and Tail Functions. The
Concatenation Function. The Reverse Function. The
Decomposition Induction Principle. The Substring Relation.
The Complete Induction Principle. Nonnegative Integers
and Strings. String Representation of Integers. Problems.
Chapter 8: Trees
Basic Properties. The Left and Right Functions. The
Subtree Relation. Strings and Trees. Problems.
Chapter 9: Lists
Basic Properties. The Head and Tail Functions. Append
and Member. Example: Flatlist. Tree Representation of
Lists. Example: Parsing. Problems.
Chapter 10: Sets
Basic Properties. The Equality Proposition. The Choice
and Rest Functions. The Union and Intersection
Functions. The Deletion and Difference Functions.
The Subset Relation. The Set Constructor. Cardinality.
Singleton Sets. Problems.
Chapter 11: Bags
Basic Properties. The Equal-Multiplicity Relation.
Multiplicity and Equality. The Count Function.
Additional Functions and Relations. Sum, Union,
and Intersection. Problems.
Chapter 12: Tuples
Basic Properties. Nonnegative Integers and Tuples.
Mapping Tuples into Sets and Bags. The Permutation
Relation. The Ordered Relation. The Sort Function.
Recursive Definition of Functions. Problems.
Related Textbooks
Index of Symbols
General Index
------------------------------
End of PROLOG Digest
********************