A front-end language for a deductive database management system is described. Only passing mention of the actual deductive techniques planned is made (in Section 4); this makes the title somewhat misleading. The language has two parts: a language for defining database schema and a command language for updates, etc. The major features of the schema language are (1) declarations for types and primary relation names that are quite like those of ordinary programming languages, and (2) a first-order-like language for defining views, derived relations and integrity constraints. The extensions over regular first-order logic are mostly syntactic sugar. Numerical quantifiers are allowed, e.g., THERE EXIST 2×P(x). The internal representation for these is not given, but presumably it will involve equality, which will make the deductions relatively harder.
Relations with three or more arguments are written in distributed form, e.g., SUPPLIES (x,y,z) is written as x .IS SUPPLIED TO. y .BY. z. WHO and WHICH can be used to replace the middle variable in a JOIN expression, e.g., BILL .IS FATHER OF. JOHN WHO .IS FATHER OF. BOB. Finally, relations can be written with exponents, e.g., x .IS FATHER OF.:2Wx2 z to represent x is the grandfather of z. One can also write R:2Wx* to represent the transitive closure of R under the Closed World Assumption. The claims that the resulting language is easier to read and write are subjective. The transitive closure operator is nice, but the claim on p. 172 that it would otherwise require an infinite formula is not true.
The second language, the command language, consists of DBA commands, user commands, and DB maintenance commands. These allow for such things as checking for consistency of formulas, suspending and reactivating formulas, answering both open and closed queries, and updating. Users are not allowed to change the database, but they can define their own temporary relations and views. The command language is much less interesting and is given much less treatment.
While it was not the intent of the authors to address implementation, some of the features seem inherently impossible to achieve. The main problem seems to be whether or not function symbols will be allowed. Section 3.1, paragraph 2 (p. 171) states that the language is based on first-order logic without functions. But the language definition allows arbitrary quantifier prefixes (Appendix 1), and wffs are to be Skolemized (Section 4, paragraph 3, p 176). Also, many of the examples involve existentials inside universals, e.g., AGE:0U COND and C2 in the constraints in the example on p. 169. Of course, this makes the logic undecidable, which in turn will cause problems in the implementation of commands like PROVE, APPLY, FIND, etc. It is not clear that FIND, for example, really can find all “objects” satisfying the formula, or that PROVE will be able to ans- wer that the given formula is provable or not provable, or to correctly reject contradictory formulas. In a similar vein, the use of numerical quantifiers may wreak havoc with their theorem prover if it is implemented with equality. Using a general purpose theorem prover, even without the presence of functions, but with general formulas, is not at all easy or straightforward for answering queries.
The paper is easy to read and contains very good examples. There are a few typos, but none are serious. The English is exceptionally good considering the paper was written by non-English speaking authors.
