Logical Foundations of Object-Oriented and Frame-Based Languages

Michael Kifer^{∗} Georg Lausen^{†} James Wu^{‡}

Techical Report 90/14 (2-nd revision) August 1990

Department of Computer Science SUNY at Stony Brook, NY 11794-4400

∗Department of Computer Science SUNY at Stony Brook Stony Brook, Stony Brook, NY 11794. Work sponsored in part by the NSF grants DCR-8603676 and IRI-8903507.

†Fakultaet fuer Mathematik und Informatik, Universitaet Mannheim, D-6800 Mannheim, Germany.

‡Department of Computer Science SUNY at Stony Brook Stony Brook, Stony Brook, NY 11794. Work sponsored in part by the NSF grant IRI-8903507.

Logical Foundations of Object-Oriented and Frame-Based Languages

Michael Kifer ^{§}  Georg Lausen ^{¶}  James Wu ^{∥}

Abstract

We propose a novel logic, called Frame Logic (abbr., F-logic), that accounts in a clean declarative fashion for most – if not all – of the features of object-oriented and frame-based languages, such as object identity, complex objects, inheritance, polymorphic types, methods, encapsulation, and so on. In a sense, F-logic stands in the same relationship to the object-oriented paradigm as the classic predicate calculus stands to relational programming. The syntax of F-logic is higher-order which, among other things, allows the user to reason about data and schema using the same declarative language. F-logic has a model-theoretic semantics and a sound and complete resolution-based proof procedure.

§Department of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794, U.S.A. Work supported in part by the NSF grants DCR-8603676 and IRI-8903507;

¶Fakultät für Mathematik und Informatik, Universität Mannheim, D-6800 Mannheim, West Germany ∥Department of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794, U.S.A. Work supported in part by the NSF grant IRI-8903507

Contents

1 Introduction 1

2 Object-Oriented vs. Declarative Programming 2

3 Syntax and Semantics of F-logic 4 3.1 F-logic by Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.4 Untyped Semantic Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.5 Incorporating Relational-Style Programming . . . . . . . . . . . . . . . . . . . . . . . . . 17

4 F-logic as a Programming Language 19 4.1 Databases and Queries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.2 Class-Hierarchies, Types, and Objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

4.2.1 ISA Hierarchies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 4.2.2 Type Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

4.3 Well-Typed Canonic Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.4 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.5 Inheritance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

4.5.1 Monotonic Inheritance of Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.5.2 Nonmonotonic Inheritance of Methods . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.5.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

5 Skolemization and Herbrand’s Theorem 36 5.1 Skolem Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.2 Herbrand Interpretations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.3 Correspondence between Herbrand Interpretations and Semantic Structures . . . . . . . . 39 5.4 Herbrand’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

6 Proof Theory 41 6.1 Unifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 6.2 Core Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 6.3 ISA Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6.4 Type Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 6.5 Miscellaneous Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 6.6 Comments on the Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.7 Soundness of the Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.8 Completeness of the Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

7 Other Issues 51 7.1 Classes and Individual Objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 7.2 Objects that “Exist” . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 7.3 Complex Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 7.4 Encapsulation, Database Views . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 7.5 Versions Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 7.6 Path Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 7.7 User-defined Inheritance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

8 Assorted Examples 58 8.1 Browsing Database Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 8.2 Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 8.3 Analogies and the Like . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 8.4 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

9 Overview of the F-logic Tool Kit 66

10 Conclusion 69

References 69

A The Perfect-model Semantics for F-logic 76

B Interaction of Inheritance and Deduction: Examples 78

C Perfect Models in the Presense of Inheritance 81

D An Algorithm for F-term Unification 82

1 Introduction

In the past decade object-oriented approach has generated considerable interest in the database and programming languages communities. Although the very term “object-oriented” is only loosely defined, a number of concepts, such as complex objects, object identity, methods, encapsulation, typing and inheritance, have been identified as the most salient features of that approach [Ban88, SB86, ZAB*85, Weg87, ABD*89].

In databases, one of the main driving forces behind the recent interest in object-oriented languages is the promise they show in overcoming the, so called, impedance mismatch [Mai87, ZAB*85] between programming languages used to code applications and database languages used to retrieve data. In parallel, another, deductive, approach has gained enormous popularity both in databases and programming languages. Since logic can be used as a full-fledged computational formalism as well as a database specification language, proponents of the deductive approach also have argued that it is capable of overcoming the aforesaid mismatch problem. However, in their present form both approaches have shortcomings. One of the main problems with the object-oriented approach is the lack of logical semantics, which traditionally was considered to be very important for database programming languages. On the other hand, deductive databases normally use flat data model and do not support the concept of object and data abstraction. It therefore can be expected that combining the two paradigms may yield significant benefits.

A great number of attempts to combine the two approaches have been reported in the literature (e.g. [AB87, AG87, AK89, BK86, BNST87, BNT88, CW89, KW89, Kup87, KV84, Mai86, RKS85, Bal86]) but, in our opinion, none of them has successfully achieved the goal. These approaches either do not support object identity, or restrict the type of complex objects and queries one can use, do not support inheritance or typing, sacrifice declarativeness, and so on.

In this paper we propose a formalism, called Frame Logic (abbr., F-logic), that achieves all of the goals listed above and, in addition, is suitable for defining and manipulating database schema and types. F-logic is a full-fledged logic, which has the advantage when tackling problems in knowledge representation that go beyond the limits of traditional logic programming. In a sense, F-logic stands in the same relationship to the object-oriented paradigm as the classic predicate calculus to relational programming. Our work has also implications for frame-based languages in AI [FK85, Min81], which are essentially scaled-down versions of complex objects with identity, inheritance, and deduction. It is this connection that the name “F-logic” was derived from. However, most of our terminology comes from the object-oriented parlance. Thus, we will be talking about objects, methods, and attributes instead of frames, slots, and the like.

Similarly to predicate calculus, F-logic is much more general than what is normally needed for knowledge representation and logic programming. Although most of this paper deals with the general properties of the formalism, i.e. its syntax, semantics, and proof theory, Sections 4 and 7 outline an actual programming language anchored in F-logic.

To reason about inheritance and objects’ schema we need capabilities of higher-order logics. However, these are usually much too powerful to be useful for our purposes. A number of researchers have suggested that the “useful” higher-order concepts of knowledge-representation languages can be given a first-order semantics by encoding these concepts in predicate calculus [Hay79, McC79]. Unfortunately, this provides only an indirect semantics, does not adequately capture many aspects, and is not true to the spirit of object-oriented programming and frame-based languages in AI. In contrast, we propose a logic that, according to the classification of [CKW89b, CKW89a], has a higher-order syntax, but a natural direct first-order semantics. A sound and complete resolution-based proof procedure for F-logic is described in Section 6.

This work is based on the two previous papers [KW89, KL89], which in turn borrowed several important ideas from Maier’s O-logic [Mai86]. In [KW89], we described a logic that adequately covered the structural aspect of complex objects but was short of capturing methods, types, and inheritance. The original F-logic, as reported in [KL89], was a first step towards higher-order syntax. In particular, this gave us the ability to talk about methods, objects schema, and certain kinds of inheritance. However, the first version of F-logic suffered from several drawbacks as far as its modeling capabilities were concerned.

One of the problems was that objects and classes were required to form a lattice, which turned out to be impractical for a logic-based language. Another problem was that the earlier version of F-logic in [KL89] formalized the values of object attributes through the means suitable for modeling attribute types rather than values. As a result, attribute values often behaved like types, while true typing was not supported at all. All these problems have been corrected in the present paper and, in addition, the logic was extended to accommodate types, type checking and nonmonotonic inheritance.

One aspect of knowledge-base systems that is not addressed in this work is the language for updates. Although updates can be explained in our framework as transformations of theories (or canonical models), no agreement exists regarding the ways of accommodating updates in declarative languages. Some of the existing proposals [MW88, NT89, GdS89] can be used meanwhile.

This paper is organized as follows: We could not resist the temptation to propose our own characterization of object-orientedness; this characterization is presented in Section 2. In Section 3 we describe the syntax and semantics of F-logic. After that, in Section 4 we discuss the issues pertaining to logic programming based on F-logic, such as negation, typing, and inheritance. Sections 5 and 6 present a proof theory for F-logic. An array of issues such as specification of individual objects, the role of pure values, versions control, database views and encapsulation is covered in Section 7. Section 8 demonstrates the modeling power of F-logic via a number of representative examples. In Section 9 we discuss the relationship among the internal components of F-logic and relate this logic to the standard predicate calculus; Section 10 concludes the paper.

2 Object-Oriented vs. Declarative Programming

Recently, a number of researchers have expressed the view that Object-Oriented programming is based on a strain of languages that is fundamentally different and incompatible with other paradigms, especially with logic programming [Ull87, Mai89], while others claimed to the contrary. This debate was a reflection of the failure of previous works to formalize many aspects of object-oriented programming. Another reason was the lack of a framework which would allow to classify various approaches and see their differences and common points in a right perspective. In this section we echo this debate and propose a classification that, we believe, fills in this gap.

Only a handful of researchers ever tried to define the notion of object-orientation, and even when this was attempted it was usually done in a non-systematic way – typically, by overwhelming the reader with a number of “golden” properties of object-oriented systems. Some works (e.g. [ABD*89]) go even further and subdivide these properties into “mandatory” and “optional” ones. In our view, such definitions fail to recognize the fact that whether a language is object-oriented or relational is merely an issue in data representation.

Relational representation is characterized by the fact that – at the logical level – data is grouped by properties. For instance, information regarding one person may be split among different relations, such as EMP, MGR, PROJ, each describing different properties attributed to persons. On the other hand, tuples describing distinct persons that deal with the same property (e.g., “project”) are grouped together in one relation (P ROJ[emp no, projname], in this case). In contrast, object-oriented representation seeks to group data around objects (again, at the logical level). According to this philosophy in language development, the user should be able to access all the public information about any specific object once he has a “handle” on that object. Such a handle is usually referred to as object identity [KC86]—an implementational notion whose conceptual counterpart is object denotation.^{1} The view of object ids as object denotations was first expressed in [KW89] and later also discussed in [CW89, Bee89].

Having decided to group data around objects, one can now try to exploit the potential of such representation and start talking about object denotations (i.e., object identities), hierarchies of classes, inheritance, typing, and so on. The difference between optional and mandatory properties of [ABD*89] now becomes a subjective question of what one perceives to be the most important features of this mode of data representation.

Languages can also be classified along another dimension—according to their programming paradigm. Here one can point at the following three major groups of languages: procedural, functional, and declarative. Figure 1 shows how various languages fit into this framework. By looking at the picture, it becomes clear that the misconception about incompatibility of declarative and object-oriented languages comes from overlooking the fact that the two classification axes are orthogonal. What was commonly referred to as deductive databases, is simply a class of languages characterized by relational data representation and declarative programming paradigm. In contrast, most of the systems that bear the object-oriented label are procedural. Only recently, a number of upward-compatible object-oriented logics have been introduced [CW89, KW89, KL89], which made it possible to see how the perceived incompatibility gap could be bridged. The revised version of F-logic presented here continues this line of research, filling in the gaps and rectifying the flaws of our earlier attempts [KW89, KL89].

1The term object name seems more appropriate here, but it is overused in the database context.

[figure: . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . . .; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}; Declarative; Functional; Procedural; Relational; oriented; Object; paradigm; Representation; Glue [PUM90]; Pascal-R [Sch77]; O_{2} [LR89]; Prolog [CM81]; Daplex [Shi81]; IQL [AK89]; paradigm; Programming; FQL [BF79]; C-logic [CW89]; O-logic [KW89]; F-logic; Orion [KBC*87]; Exodus [CDV88]; Rel. Algebra; ISBL; NAIL! [MNS*87]; LDL [NT89]]

Figure 1: Classification of Programming Languages

We also note that practical considerations sometimes dictate that a mixture of paradigms be available under the same roof. For instance, Prolog [CM81] has control primitives that give it a procedural flavour. The logical object-oriented languages [KW89, CW89, KL89, AK89] allow grouping of data around properties (i.e., relationally) as well as around objects. IQL [AK89] also has a number of nonlogical features and thus, in Figure 1, it slides down towards the procedural paradigm.

In general, we believe that the future belongs to multi-paradigm languages, and so the aforementioned “impurity” is not necessarily detrimental. An important research issue is, however, finding ways for clean integration of different kinds of languages. It will be clear from this paper that inside the declarative domain, relational and object-oriented languages go hand-in-hand. Interfaces between relational (declarative and procedural) and object-oriented (declarative and procedural) languages are also known. However, we are unaware of any clean solution to integration of procedural object-oriented languages with relational ones; likewise, there is no generally agreed upon framework for absorbing functional languages into the declarative paradigm.

3 Syntax and Semantics of F-logic

In this section we describe the proposed logic by means of an example, which is followed by a formal account of the syntax and semantics.

[figure: person; young; midaged; student; empl; string; “CS ”; “Mary”; “Bob”; john; sally; yuppie; 20; 30; 40; child(john); report; article; seminal paper; alice; child(person); faculty; mary; bob; phil; hi paid empl; ms; phd; cs_{1}; cs_{2}; dept; degrees]

Figure 2: Part of ISA-Hierarchy

3.1 F-logic by Example

In developing F-logic we were motivated by a desire to capture in a logically clean way a number of knowledge representation scenarios several of whose most salient features are depicted by way of an example in Figures 2, 3, and 4. Figure 2 shows part of the class hierarchy. All classes and individual objects are taken from the same domain and are organized in a hierarchy. This hierarchy asserts that a faculty and a hi paid empl are employees, student and empl are persons, “Mary” and “CS ” are strings, mary is a faculty, while sally is a student. Note that classes are reified by being placed in the same domain as their instances. Thus the same term, say, empl can be viewed as an instance of its superclass, person, and, at the same time, as a class of all objects that are below empl in the hierarchy. In the actual syntax of F-logic, the hierarchy of Figure 2 is recorded as shown in Figure 3. Here statements such as empl : person say that empl is a subclass of person (i.e., every employee is a person); john : empl says that john is a subclass of empl, and so on. Notice that john is just a constant denoting an object. F-logic treats john as a class since it has no way of knowing whether john is meant to be an individual object, that is, an object representing itself, or a collection of other objects. Section 7.3 discusses several ways of distinguishing between individual objects and classes, especially recommending one of them. Until then, however, we will not emphasize the distinction between classes and individuals.

Figure 4 describes a database fragment containing information about employees, students, and others. The first clause says that the object bob is a faculty whose name is “Bob”. Note: bob is an id or a denotation empl : person yuppie : young student : person 20 : young child(person) : person 40 : midaged john : student “CS” : string john : empl “Bob” : string cs_{1} : dept alice : child(john)

. . . . . . . . .  . . . . . . . . .
. . . . . . . . .  . . . . . . . . .

Figure 3: F-logic Representation of the ISA-Hierarchy of Figure 2

of the object, while “Bob” is a string-object representing the value of one of bob’s attributes, called name. Additionally, this clause states that bob works in the department cs_{1}, the department’s name is “CS ”, and its manager is described by the object bob. We thus see that bob is, in effect, a cyclic object. Clause (2) represents similar information about mary. Note that the friends and the degrees attributes in mary’s record are set-valued, which is syntactically expressed by means of the double-headed arrow “→ →” and the braces “{ }”.

Clauses (3) to (6) provide general information about classes and their signatures. Clause (3), for instance, says that attributes age and degrees of every object in class faculty must be of types midaged and degrees, respectively, while the attribute boss must simultaneously be of types faculty and hi paid empl. This means that, for every faculty, the values of these attributes (considered as objects) must belong to the aforementioned classes. The reader may have already noticed that double-shafted arrows ⇒, ⇒ ⇒ are used for typing, while arrows →, → → for describing values of attributes. Also, double-headed arrows → → and ⇒ ⇒ are used in conjunction with set-valued attributes while →, ⇒ signify functional (also called single-valued) attributes. Different kinds of information about objects can be mixed in one clause. For instance, in Clause (3), the fragment degrees ⇒ ⇒ degrees specifies the type of the attribute degrees (in F-logic, using the same symbol for types and attributes is legal), while degrees → → {phd} describes its value. Assigning a value to a class-attribute has the effect that every object of class faculty inherits the value phd of the attribute degrees, unless stated otherwise.

Clauses (4) to (6) specify typing constraints for the classes person, empl, and dept. Alternatively, it can be said that these terms define signatures of methods attached to these classes. Two things are noteworthy in Clause (4). First, the fragment joint works @ person ⇒ ⇒ report describes a method, joint works, which is a function that expects one argument of type person and returns a set of elements of type report. In object-oriented terms, this means that whenever a person-object, obj, receives a message joint works with an argument of class person, then the reply-message returned by obj will consist of a set of objects, each of which is in the class report. Note that there is no essential difference between methods and attributes: the latter are simply methods without arguments. Strictly speaking, in Figure 4 we should have written name @ ⇒ string and age @ → 40 instead of name ⇒ string and age → 40, but the latter shorthand notation is convenient when no arguments are expected. Many more Database Facts:

(1) bob[name → “Bob”; age → 40; employed → cs_{1}[dname → “CS”; mngr → bob; assistants → → {john, sally}] ]

(2) mary[name → “Mary”; degrees → → {ms}; friends → → {bob, sally}; employed → cs_{2}[dname → “CS” ] ]

General Class Information:

(3) faculty[boss ⇒ {faculty, hi paid empl}; % Typing: functional attribute age ⇒ midaged; degrees ⇒ ⇒ degrees; papers ⇒ article; degrees → → {phd}] % degrees = {phd}—a property of class faculty

(4) person[name ⇒ string; employed ⇒ dept; friends ⇒ ⇒ person; % Typing: set-valued attribute children ⇒ ⇒ child(person); % Typing: each child is in class child(person) joint works @ person ⇒ ⇒ report] % Typing: set-valued method, one argument

(5) empl[employed ⇒ dept] % Typing: employees work in departments

(6) dept[assistants ⇒ ⇒ {student, empl}] % Typing: assistants are students & employees Deductive Rules:

(7) E[boss → M ] ← E : empl[employed → D : dept[mngr → M : empl] ]

(8) X[joint works @ Y → → {Z}] ← Y : faculty[papers → → {Z}] & X : faculty[papers → → {Z}]

Queries:

(9) ? − X : empl[boss → Y; age → Z : midaged; employed → D[dname → “CS” ] ]

(10) ? − mary[joint works @ Y → → {jacm90}]

(11) ? − mary[joint works @ phil → → {Z}]

Figure 4: A Sample Database

examples of methods in F-logic appear in Section 8.2.

The second thing to be noted in Clause (4) is the fragment children ⇒ child(person) that specifies a type constraint for the attribute children. Here, child is a unary function symbol and person is a constant denoting a class. Together, they form a denotation of a new class child(person)—in F-logic, function symbols can be used to construct new object/class denotations out of existing ones. This provides a sufficient supply of object identities to choose from, and obviates the need in extra-logical constructs such as new in [AK89].

Occasionally, we may omit braces when the set in question contains only one element. Thus, we can write name ⇒ string instead of name ⇒ {string}. However, in boss ⇒ {faculty, hi paid empl} of Clause (3) and in assistants ⇒ ⇒ {student, empl} of Clause (6), braces must be kept to indicate that the values of attributes boss and assistant must belong to each of the specified classes. (In fact, Clause (6) is equivalent to a pair of clauses dept[assistants ⇒ ⇒ student] and dept[assistants ⇒ ⇒ empl], but the notation with braces is shorter in this case).

Clause (7) is a deductive rule that defines a new attribute, boss, for objects of class empl. It says that employee’s boss is the manager of the department the employee works in. Here we follow the standard convention in logic programming that requires names of logical variables to begin with a capital letter. Clause (8) defines a method joint works. For any object in class person, it is a function that takes an object of type person and returns a set of objects of type report; each object in this set represents a joint paper of the two persons involved. Informally, this rule should be read as follows: If a report-object, Z, simultaneously belongs to the sets determined by the attribute papers for the faculty-objects X and Y, then Z must also belong to the set returned by the method joint works when invoked in the scope of X on the argument Y. Note that we do not need the restriction Z : report in the rule body, because for each faculty the attribute papers specifies a set of article-objects, according to clause (4), and article is a report (see Figure 2). However, if we were interested in seminal papers only, then the restriction Z : seminal paper would have been needed in the body of (8).

Two applications of the method joint works are demonstrated in (10) and (11). Query (10) asks about the co-author of mary’s jacm90 paper, while (11) requests all joint papers that mary wrote with phil. Query (9) inquires about all middle-aged employees working in “CS ” departments. In particular, for every such employee, the attributes boss, age, and employed are requested. The expected answer to (9) is

(12) bob[boss → bob; age → 40; employed → cs_{1}].

The object mary does not qualify because of the unknown or undefined age.

In the above example and in the rest of this paper, the term “type” is used interchangeably to denote classes of various objects as well as method signatures. The appropriate meaning should be clear from the context.

Before bidding farewell to this example, we would like to make few more remarks highlighting other features of F-logic. First, if in Clause (1) the manager were phil rather than bob, then we would have had a type error. Here, phil would have caused a type error because on one hand he is not a faculty (and is not a hi-paid-empl—see Figure 2) and, on the other hand, rule (7) implies that phil is bob’s boss. This contradicts the typing of the boss-attribute in Clause (3). As will be seen in Section 4.2.2, the notions of well-typedness and type error have precise model-theoretic meaning.

Another point is that F-logic enforces class signatures. In our case, this means that the only allowable methods for objects of the class faculty are

• name, friends, children, and joint works—the methods inherited from person;

• employed—a method inherited from empl; and

• boss, age, degrees, and papers—the methods directly specified for the class faculty.

However, it would be illegal (a type error) to apply methods in the last group to objects that are employees but not faculty. Likewise, it would be illegal to apply the attribute employed to unemployed persons (unless type inference is allowed; see Section 4.3).

Yet another point is that method names can be “overloaded” with respect to arities. This means that writing, say, john[grade @ db → “C”] and students[grade @ students, courses ⇒ grades] is legal and, in fact, the two occurrences of grade are represented by two different functions. Similar overloading was shown to be very convenient in logic programming languages, such as Prolog.^{2}

Another kind of overloading occurs when the same method’s name is declared to be both set-valued and functional. For instance, suppose the following types are defined:

\begin{matrix}empl[joint works @ person ⇒ ⇒ report] \\ student[joint works @ person ⇒ list(report)]. \end{matrix}

In the first case, joint works is a set-valued method of one argument that for any employee and a given person returns the set of this employee’s joint works with that person. In the second case, joint works returns only one value—a term representing the list of student’s joint papers. (Lists are defined in Section 4.2.1; for the time being, the reader can think of list(report) as a class of objects with object identities such as cons(popl88, cons(jacm89, nil)).) So, if sally is both an employee and a student, the programmer can invoke the set-valued incarnation of the method by using the term

… ← … & sally[joint works @ bill → → {X}] & …

or the single-valued implementation of the method, using

… ← … & sally[joint works @ bill → X] & …

On the other hand, it would be a type error to invoke the set-valued version of joint works on objects that are not employees; likewise it is an error to use the functional version of joint works for someone who is not a student.

It has been argued that in frame-based languages the programmer should be able to block the inheritance mechanism for certain attributes. For example, average salary may be a meaningful attribute for the class empl, e.g., empl[avg salary → 40K], but makes no sense (or, at least, has completely different meaning) when it is applied to an individual employee, e.g., john. In Section 4.5 we present a simple modification to the semantics of F-logic that allows to declare some methods as non-inheritable.

The example in Figures 2, 3, and 4 alludes to the point that in F-logic we are dealing with higher-order concepts. For instance, in Figure 4, the attribute friends is a set-valued function that for each person returns a set of persons. Similarly, the user can think of objects in the class hierarchy of Figure 2 as sets ordered by the subset relation. We will also see that variables can range over methods and attributes. However, the underlying semantics formally remains first-order [CKW89a], which allows us to overcome the difficulties normally associated with semantically higher-order theories.

2Adopting such overloading reflects our personal bias in language design; it is not intrinsic in F-logic and can be repealed with only minor changes to the semantics and the proof theory.

The first-order behaviour with respect to sets is achieved by precluding variables from being bound to sets. Sets can be represented by other objects, though, and variables can be bound to these latter ones. Formally, F-logic has flat sets only, but we can model arbitrarily-deeply nested sets in a very natural way. F-logic shares this behaviour with respect to sets with other related formalisms [CW89, KW89]; more discussion can be found in [KW89]. The first-order behaviour with respect to the class/subclass hierarchy is achieved, again, by viewing classes intensionally, that is, as objects distinguished by their denotations, rather than extensionally, as sets determined by their contents. For a comprehensive discussion of the semantic subtleties of higher-order logic languages the reader is referred to [CKW89b, CKW89a].

3.2 Syntax

The alphabet of an F-logic language L consists of (1) a set of object constructors F, (2) an infinite set of variables V, and (3) usual logic connectives and quantifiers ∨, ∧, ¬, ← , ∀, ∃.

“Objects” in F-logic are either individual objects in the usual sense, or classes of objects. Unlike other approaches that treat classes and individual objects as inherently different entities, we do not emphasize the distinction (but see Section 7.1 where we do). For instance the object student can be viewed as a representation of the class of students (each individual student being its instance) and at the same time as an instance of its superclass represented by the object person. Thus, in F-logic classes are treated similarly to frame-based languages (e.g. [FK85, Min81]) in the sense that a class is viewed as an instance rather than a subset of its superclasses. This feature comes in handy when one needs to reason about classes as well as individual objects, e.g., for browsing databases or polymorphic type declarations (see also Section 7.1).

Object constructors (elements of F) play the role of function symbols of F-logic. Each function symbol has an arity—a nonnegative integer that determines how many arguments this symbol can take. Symbols of arity 0 play the role of constant symbols; symbols of arity ≥ 1 are used to construct larger terms out of simpler ones. An id-term is a term composed of function symbols and variables in the usual way (as in predicate calculus). The set of all ground (i.e., variable-free) id-terms is denoted by F^{∗}. Conceptually, ground id-terms should be perceived as object denotations, which is a logical abstraction corresponding to the concept of object identity [KC86, AK89] – one of the pillars of the object-oriented paradigm. As we shall see, objects represented by “complex” id-terms (e.g. addr(13, mainstreet, anywhere) ) usually arise when a complex object (or a class) is constructed out of simpler components (13, mainstreet, and anywhere, in our example).

To eliminate needless repetitions, F and F^{∗} will henceforth denote the set of function symbols and ground terms, respectively, of some F-logic language L that will be known from the context.

In O-logic [Mai86, KW89] – a predecessor of F-logic – there was a distinction between objects and attributes and the latter were viewed just as binary relations among objects. This distinction made it difficult to reason about entities and relationships in a uniform framework; it can be traced to the Entity-Relationship model where entities (objects) and relationships (attributes) constitute two disjoint categories.

Every F-logic object can be viewed as an entity or a relationship depending on the situation (namely, on its syntactic position in a formula). In its role as an attribute or, more generally, as a method, an object can be either single-valued (also called functional) or set-valued. The type of an occurrence of a method is determined by the context, as explained below.

The language of F-logic consists of a set of formulae constructed out of the alphabet symbols. Formulae are built from so called F -terms (F-logic terms) by means of the usual connectives ¬, ∨, and ∧, and quantifiers ∃ and ∀. In the examples, the conjunction symbol ∧ will be written as & . Later we shall see that the id-terms introduced earlier can be viewed as a special case of F-terms.

For convenience, we will use the names starting with lower-case letters to denote ground terms, and the names starting with capital letters to denote terms that may be nonground. An F -term is:

1. An is-a F-term, Q : P, where P and Q are id-terms; is-a terms are used to define class-hierarchies;

2. A data F-term,

P [F unM_{1} @ Q_{1,1}, ..., Q_{1,k_{1}} → T_{1}; ...; F unM_{m} @ Q_{m,1}, ..., Q_{m,k_{m}} → T_{m};

SetM_{1} @ R_{1,1}, ..., R_{1,l_{1}} → → {S_{1,1}, ..., S_{1,o_{1}}}; ...; SetM_{n} @ R_{n,1}, ..., R_{n,l_{n}} → → {S_{n,1}, ..., S_{n,o_{n}}}]. Here P is an id-term that denotes an object (or a class); F unM_{i} and SetM_{j} are also id-terms; the names “F unM_{i}”, “SetM_{j}” are chosen to indicate that the syntactic position within the F-term makes F unM_{i} and SetM_{j} play the role of methods (or families of methods, if F unM_{i} and SetM_{j} are nonground) applied to P. The appearance of the set construct, { }, and of the double-headed arrow, → →, indicates that the respective id-terms SetM_{1}, ..., SetM_{n} denote set-valued methods; the rest of the methods, F unM_{1}, ..., F unM_{m}, are functional (i.e., single-valued). The order of methods in an F-term is immaterial. Finally, T_{i} and S_{j,v} denote data F -terms representing the output of the respective methods F unM_{i} and SetM_{j} when invoked in the scope of the object P on the arguments Q_{i,1}, ..., Q_{i,k_{i}} and R_{j,1}, ..., R_{j,l_{j}}, respectively. The latter are also id-terms.

3. A signature F-term,

P [F unM_{1} @ Q_{1,1}, ..., Q_{1,k_{1}} ⇒ {A_{1,1}, ..., A_{1,s_{1}}}; ...; F unM_{m} @ Q_{m,1}, ..., Q_{m,k_{m}} ⇒ {A_{m,1}, ..., A_{m,s_{m}}};

SetM_{1} @ R_{1,1}, ..., R_{1,l_{1}} ⇒ ⇒ {B_{1,1}, ..., B_{1,t_{1}}}; ...; SetM_{n} @ R_{n,1}, ..., R_{n,l_{n}} ⇒ ⇒ {B_{n,1}, ..., B_{n,t_{n}}}]. Here P is an id-term that denotes the class whose objects have the type given by the above signature F-term. The id-terms F unM_{i} and SetM_{j} denote methods (or families of methods, in the nonground case); set-valued methods are distinguished by the double-headed and double-shafted arrow ⇒ ⇒. The signature F-terms A_{i,u} and B_{j,v} represent types of the results returned by the methods F unM_{i} and SetM_{j} when invoked in the scope of an object of class P on arguments of types Q_{i,1}, ..., Q_{i,k_{i}} and R_{j,1}, ..., R_{j,l_{j}}, respectively; Q_{i,u} and R_{j,v} are id-terms.

Intuitively, the data F-term (2) above is a statement about an object, P, asserting that it has properties specified by the methods F unM_{i} and SetM_{j}; these terms are used to define properties (i.e., methods) of objects. A signature F-term (3) specifies typing constraints on objects in the class P (i.e., signatures of methods attached to P). Typing is given both for arguments of methods and for their results. For instance, (3) informally says that F unM_{1} is a single-valued method such that if it is invoked in the scope of an object of class P on arguments belonging to the classes Q_{1,1} through Q_{1,k_{1}}, then the result must simultaneously belong to the classes A_{1,1}, ..., A_{1,s_{1}}. Similarly, the typing for SetM_{1} says that it is a set-valued method (indicated via “⇒ ⇒”) such that if it is invoked in a P -object on arguments belonging to the classes R_{1,1} through R_{1,l_{1}}, respectively, then each element in the result-set will simultaneously belong to the classes B_{1,1}, ..., B_{1,t_{1}}. An is-a F-term of the form (1) asserts that Q is a nonstrict subclass of P (i.e., inclusive of the case when Q = P).^{3}

Notice that terms such as a[mthd @ e → c, mthd @ f → → {d}] are syntactically correct, despite the fact that mthd must be a functional method due to one part of the term, and a set-valued method due to the other. As explained in Section 3.1, such formulas may or may not be type-correct depending on the signature of method mthd.

Also, as mentioned earlier, we do not distinguish between individual objects and classes: any object, d, is treated as a class whose extension contains all objects/classes found below d in the class hierarchy. Therefore, any object denotation p ∈ F^{∗} may appear in an is-a F-term in the “instance position”, as in p : q, and in a “class position”, as in r : p. This and other features make the F-logic language higher-order in nature, although its semantics is, strictly speaking, first-order [CKW89b, CKW89a]. Accordingly, we may use the terms “instance” and “class” to refer to the same object, p, depending on whether we want to emphasize p in its role as a class or as an instance of a superclass.

Every F-term is also a molecular F-formula. Molecular formulas are not really atomic. For instance, an F-term X[attr_{1} → a; attr_{2} → Y] is equivalent to a conjunction of its atoms X[attr_{1} → a] ∧ X[attr_{2} → Y], as follows from the semantics in the next subsection.

F-formulae are constructed from other (simpler) F-formulae by means of logical connectives and quantifiers:

• Molecular formulas are F-formulas;

• φ ∨ ψ, φ ∧ ψ, ¬φ are F-formulae, if so are φ and ψ;

• ∀X φ, ∃Y ψ are formulae, if so are φ, ψ and X, Y are variables.

The implication φ ← ψ is defined in a usual way: φ ∨ ¬ψ.

If in a data or a signature F-term Q[ ] all methods are omitted, we can identify such F-term with the id-term Q; this allows us to view id-terms as a special case of F-terms and write, say, john[age → 23] instead of a more cumbersome john[age → 23[ ] ]. However, to avoid syntactic confusion with predicates (introduced later), we will permit to drop “[ ]” only when the corresponding F-terms appear in a range of a method (cf. mary[cars → → {volvo, bmw}] vs. mary[cars → → {volvo[ ], bmw[ ] }]).

Furthermore, it is sometimes convenient to combine different kinds of F-terms (as in (3), (7) and (8) of Figure 4) and write, say,

Q : P [F unM @ X → Y : S; SetM @ Y, W ⇒ ⇒ {Z : R, T }]

3In the next subsection we will see that, in F-logic, terms such as person : person are tautologies. The intuition here is that person is a “typical element” of the class person. The notion of a typical element has been proved useful in AI, especially in dealing with nonmonotonic inheritance discussed in Section 4.5

as a syntactic sugar for

Q : P ∧ Q[F unM @ X → Y] ∧ Y : S ∧ Q[SetM @ Y, W ⇒ ⇒ {Z, T }] ∧ Z : R.

As mentioned in the previous section, whenever a method does not expect arguments, “ @ ” will be omitted and so we will write T [F unM → V al] instead of T [F unM @ → V al]; similarly for → →, ⇒, and ⇒ ⇒. Likewise, when only one term appears inside the braces denoting a set, we may occasionally write T [… → → S], T [… ⇒ R], or T [… ⇒ ⇒ R] instead of T [… → → {S}], T [… ⇒ {R}], or T [… ⇒ ⇒ {R}], respectively.

3.3 Semantics

Given a pair of sets U and V, T otal(U, V) denotes the set of all total functions U ⟼ V; similarly, P artial(U, V) stands for the set of all partial functions U ⟼ V. The powerset of U is denoted by P(U). Further, given a collection of sets {S_{i}}_{i∈N} parameterized by natural numbers, ∏_{i=1}^{∞} S_{i} denotes the Cartesian product of the S_{i}’s, that is, the set of all infinite tuples ⟨s_{1},…, s_{n},…⟩. Similarly, ∐_{i=1}^{∞} S_{i} denotes the disjoint union of the S_{i}’s.

For a language L of F-logic, its semantic structure, I, is a tuple ⟨U, ≺_{U}, I_{F}, I_{→}, I_{→ →}, I_{⇒}, I_{⇒ ⇒}⟩. Here U is the domain of interpretation and ≺_{U} is a partial order on U. As usual, we write a⪯_{U}b for a≺_{U}b or a = b. By analogy with predicate calculus, it is useful to view U as a set of all actual objects in a possible world I. On the other hand, ground id-terms (the elements of F^{∗}) can be thought of as denotations of objects; these denotations are interpreted by the objects in U via the mapping I_{F}. The ordering ≺_{U} on U is a semantic counterpart of the subclass relationship. Intuitively, a≺_{U}b means that a is a subclass of b. We extend ⪯_{U} in a natural way to tuples and sets over U: for u⃗, v⃗ ∈ U^{n} and S ⊆ U, u⃗⪯_{U}v⃗ if this relation holds component-wise; likewise, u⃗⪯_{U}S if and only if u⃗⪯_{U}s⃗, for every s⃗ ∈ S.

The mapping I_{F} : F ⟼ ∐_{i=0}^{∞} T otal(U^{i}, U) interprets each k-ary object constructor, f ∈ F, by a function U^{k} ⟼ U. For k = 0, I_{F}(f) can be identified with an element of U. Thus, function symbols are interpreted the same way as in predicate calculus.

In their role as methods, objects are interpreted via an assignment of appropriate functions to each element of U, using the maps I_{→} and I_{→ →}. More precisely, for every object, its incarnation as a singlevalued method is obtained via the mapping

• I_{→} : U ⟼ ∏_{k=0}^{∞} P artial(U^{k+1}, U)

that associates to every element of U a tuple of partial functions U^{k+1} → U; there is exactly one such function in the tuple, for every method-arity k ≥ 0. A function per arity arises from the feature mentioned in Section 3.1 that permits us to overload method names by allowing them to accept any number of arguments (and use different implementations for different arities).

Methods can be overloaded in yet another way, by using the same name for their functional and set-valued versions (cf. empl[joint works @ person ⇒ ⇒ report] and student[joint works @ person ⇒ list(report)] of Section 3.1, which are implemented via different functions). Semantically this is achieved by interpreting the set-valued incarnations of methods separately, via the mapping

• I_{→ →} : U ⟼ ∏_{k=0}^{∞} P artial(U^{k+1}, P(U))

that, for every method-arity k, associates a partial function U^{k+1} → P(U) to each element of U.

As seen from the above definitions, I_{→}(m) and I_{→ →}(m), where m ∈ U, are infinite tuples of mappings parameterized by the arity k ≥ 0. To refer to the k-th component of such a tuple, i.e. to a mapping of arity k + 1, we use the notation I(k)_{→}(m) and I(k)_{→ →}(m). As will be seen shortly, a method occurring in the context that calls for a k-argument single-valued method is interpreted by a (k + 1)-ary single-valued partial function I(k)_{→}(m) for some m ∈ U; if a method occurs in a context that calls for a k-argument set-valued method, it is interpreted by a (k + 1)-ary set-valued partial function I(k)_{→ →}(m). The first argument in any such function is always the object/class the method is called from within; the other k arguments correspond to the proper arguments of the method. In the parlance of object-oriented systems, I(k)_{→}(m)(obj, a_{1}, ..., a_{k}) is interpreted as a request to object obj to invoke the functional method m on arguments a_{1}, ..., a_{k}.

Observe that I_{→} and I_{→ →} are associated with elements of U, not F^{∗}, because – strictly speaking – F^{∗} is only a set of object denotations; these are interpreted by the “real” objects in a possible world I and it is the objects – not their denotations – that may assume roles of methods. There is also a technical reason for that, which will become apparent when we define the notion of formula satisfaction with respect to a variable assignment.

In F-logic, signature F-terms are used to describe types of arguments to which methods can be sensibly applied, and types of the results computed by these applications. To capture this semantically, we use the mappings I_{⇒} and I_{⇒ ⇒}:

• I_{⇒} : U ⟼ ∏_{i=0}^{∞} P artialAntiMonotone(U^{i+1}, P_{↑}(U));

• I_{⇒ ⇒} : U ⟼ ∏_{i=0}^{∞} P artialAntiMonotone(U^{i+1}, P_{↑}(U)),

where P_{↑}(U) is a set of all upward-closed subsets of U. A set V ⊆ U is upward closed if v ∈ V and v≺_{U}v′ imply v′ ∈ V. P artialAntiMonotone(U^{i+1}, P_{↑}(U)) denotes the set of partial anti-monotonic functions from U^{i+1} to P_{↑}(U). For a partial function ρ : U^{k} ⟼ P_{↑}(U), anti-monotonicity means that if u⃗, v⃗ ∈ U^{k}, v⃗⪯_{U} u⃗, and ρ(u⃗) is defined, then ρ(v⃗) is also defined and ρ(v⃗) ⊇ ρ(u⃗).^{4}

As with I_{→} and I_{→ →}, we use I(k)_{⇒}(m) and I(k)_{⇒ ⇒}(m) to refer to the k-th components of tuples I_{⇒}(m) and I_{⇒ ⇒}(m), respectively.

The intended meaning of I(k)_{⇒}(m) (or I(k)_{⇒ ⇒}(m) ) is the type of the (k + 1)-ary function I(k)_{→}(m) (resp., I(k)_{→ →}(m) ). In other words, the subset of U^{k+1} where I(k)_{⇒}(m) (or I(k)_{⇒ ⇒}(m) ) is defined should be viewed as a set of (k + 1)-tuples ⟨obj, arg_{1}, ..., arg_{k}⟩ to which I(k)_{→}(m) (resp., I(k)_{→ →}(m) ) can be sensibly applied. For every tuple ⟨o, args^{⟶}⟩ ∈ U^{k+1}, I(k)_{⇒}(m)(o, args^{⟶}) (or I(k)_{⇒ ⇒}(m)(o, args^{⟶}) ) represents the type of I(k)_{→}(m)(o, args^{⟶}) (resp., I(k)_{→ →}(m)(o, args^{⟶}) ), that is, the type of the result of application of the method m to arguments args^{⟶} within object o. This means that I(k)_{→}(m)(o, args^{⟶}) (resp., every element of I(k)_{→ →}(m)(o, args^{⟶}) ) must belong to every class in I(k)_{⇒}(m)(o, args^{⟶}) (resp., in I(k)_{⇒ ⇒}(m)(o, args^{⟶}) ).

4Actually, these functions are monotone with respect to the, so called, Smyth’s ordering [BO89]. For upward-closed sets, S ⊆^{smyth} S′ if and only if S ⊇ S′.

The above interpretation of I(k)_{⇒}(m) and I(k)_{⇒ ⇒}(m) explains the anti-monotonicity and the upwardclosedness requirements to these functions: If, say, I(k)_{→}(m)(o, args^{⟶}) is of type a (i.e., I(k)_{→}(m)(o, args^{⟶}) ⪯_{U}a) then, clearly, I(k)_{→}(m)(o, args^{⟶}) must belong to every supertype of a (i.e., I(k)_{→}(m)(o, args^{⟶})⪯_{U}b, for every b, a≺_{U}b); thus I(k)_{⇒}(m)(o, args^{⟶}) must be upward-closed. Similarly, if I(k)_{→}(m) is sensibly applicable to every tuple of type ⟨o, args^{⟶}⟩ then it must be also sensibly applicable to every tuple of any subtype ⟨o′, args^{⟶} ′⟩ of ⟨o, args^{⟶}⟩ (i.e., whenever ⟨o′, args^{⟶} ′⟩⪯_{U}⟨o, args^{⟶}⟩). Furthermore, the result of application of I(k)_{→}(m) to any of the tuples of type ⟨o′, args^{⟶} ′⟩ must be type-compatible with the type of the result of I(k)_{→}(m) on tuples of type ⟨o, args^{⟶}⟩. In other words, we must have I(k)_{⇒}(m)(o′, args^{⟶}′) ⊇ I(k)_{⇒}(m)(o, args^{⟶}) (i.e., anti-monotonicity); I(k)_{⇒}(m)(o′, args^{⟶}′) is a superset here because I(k)_{→}(m)(o′, args^{⟶}′) must belong to every class to which I(k)_{→}(m)(o, args^{⟶}) belongs. Similarly for I_{→ →} and I_{⇒ ⇒}.

The above intuition about the relationship between I_{→}, I_{→ →}, I_{⇒}, and I_{⇒ ⇒} is semantically expressed by the following conditions that glue together the semantics of objects and types: The Well-Typing Conditions: For all m, o, p_{1}, ..., p_{k} ∈ U,

• If I(k)_{→}(m)(o, p_{1}, ..., p_{k}) (or I(k)_{→ →}(m)(o, p_{1}, ..., p_{k}) ) is defined then so is I(k)_{⇒}(m)(o, p_{1}, ..., p_{k})

(resp., I(k)_{⇒ ⇒}(m)(o, p_{1}, ..., p_{k}) );

• If q = I(k)_{→}(m)(o, p_{1}, ..., p_{k}) (or q ∈ I(k)_{→ →}(m)(o, p_{1}, ..., p_{k}) ) for some q ∈ U,

then q⪯_{U}r, for all r ∈ I(k)_{⇒}(m)(o, p_{1}, ..., p_{k}) (resp., I(k)_{⇒ ⇒}(m)(o, p_{1}, ..., p_{k}) ).

A variable assignment, ν, is a mapping from the set of variables, V, to the domain U. Variable assignments are extended to id-terms in the usual way: ν(d) = I_{F}(d) if d ∈ F has arity 0 and, recursively, ν(f(..., T, ...)) = I_{F}(f)(..., ν(T), ...). We further extend them to F-terms as follows: ν( Q[…] ) = ν(Q) and ν(T : S) = ν(T).

Let I be a semantic structure and ν a variable assignment. Intuitively, an F-term T is true under a semantic structure I with respect to a variable assignment ν, denoted I ⊧_{ν} T, if and only if I has an object ν(T) with properties specified in ν(T). Formally:

• For an is-a F-term Q : P, we write I ⊧_{ν} Q : P if and only if

(1) ν(Q)⪯_{U}ν(P).

• For a data F-term

T =^{def} P [ ...; F unM_{i} @ Q_{1}, ..., Q_{k} → T_{i}; ...; SetM_{j} @ R_{1}, ..., R_{l} → → {S_{1}, ..., S_{m}}; …],

I ⊧_{ν} T if and only if the following conditions hold:

(2) For every id-term F unM_{i} that appears in T in a context that calls for a functional method,

– I(k)_{→}( ν(F unM_{i}) )(ν(P), ν(Q_{1}), ..., ν(Q_{k})) is defined;

– ν(T_{i}) = I(k)_{→}( ν(F unM_{i}) )(ν(P), ν(Q_{1}), ..., ν(Q_{k})); and

– I ⊧_{ν} T_{i}.

(3) For every id-term SetM_{j} that appears in T in the context that calls for a set-valued method,

– I(l)_{→ →}( ν(SetM_{j}) )(ν(P), ν(R_{1}), ..., ν(R_{l})) is defined;

– {ν(S_{1}), ..., ν(S_{m})} ⊆ I(l)_{→ →}( ν(SetM_{j}) )(ν(P), ν(R_{1}), ..., ν(R_{l})); and

– I ⊧_{ν} S_{k}, for k = 1, ..., m.

• For a signature F-term

T =^{def} P [ ...; F unM_{i} @ Q_{1}, ..., Q_{k} ⇒ {R_{1}, ..., R_{m}}; …; SetM_{j} @ V_{1}, ..., V_{s} ⇒ ⇒ {W_{1}, ..., W_{l}}; …],

I ⊧_{ν} T if and only if the following conditions hold:

(4) For every id-term F unM_{i} that appears in T in the context that calls for a functional method,

– I(k)_{⇒} (ν(F unM_{i})) ( ν(P), ν(Q_{1}), ..., ν(Q_{k}) ) is defined;

– {ν(R_{1}), ..., ν(R_{m})} ⊆ I(k)_{⇒} (ν(F unM_{i})) ( ν(P), ν(Q_{1}), ..., ν(Q_{k}) ); and

– I ⊧_{ν} R_{t}, for t = 1, ..., m.

(5) For every id-term SetM_{j} that appears in T in the context that calls for a set-valued method,

– I(s)_{⇒ ⇒} (ν(SetM_{j})) ( ν(P), ν(V_{1}), ..., ν(V_{s}) ) is defined;

– {ν(W_{1}), ..., ν(W_{l})} ⊆ I(s)_{⇒ ⇒} (ν(SetM_{j})) ( ν(P), ν(V_{1}), ..., ν(V_{s}) ); and

– I ⊧_{ν} W_{t}, for t = 1, ..., l.

Here (1) says that the object ν(Q) must be in the class ν(P) in the possible world I. In (2) and (3), the first two conditions say that for a data F-term to be true in I with respect to ν, the appropriate functions must be defined and yield the expected results. In (4) and (5), the first and the second conditions say that for a signature F-term T to be satisfied by I, both input and output of functions that implement the methods (i.e., ν(F unM_{i})) must be of appropriate types. The third condition in (2) and (3) simply states that the properties asserted in T (i.e., the T_{i}, S_{j}, etc.) must also be true in I with respect to ν. The third condition in (4) and (5) asserts that signatures specifying the outputs of methods defined for T (i.e., the R_{i}’s and W_{j}’s) must be true in I.

Notice the role played by the first condition in (4) and (5). Its implication is that signatures such as a[attr ⇒ { }] and a[attr ⇒ ⇒ { }] are not tautologies, since there are semantic structures in which, say, I(0)_{⇒}(ν(attr)) is undefined on ν(a). This property will be profitably utilized in Section 4.2.2 to enforce method signatures.

Meaning of the formulae φ ∨ ψ, φ ∧ ψ, and ¬φ is defined in the standard way: I ⊧_{ν} φ ∨ ψ (or I ⊧_{ν} φ ∧ ψ, or I ⊧_{ν} ¬φ) if and only if I ⊧_{ν} φ or I ⊧_{ν} ψ (resp., I ⊧_{ν} φ and I ⊧_{ν} ψ, resp., I |̸=_{ν} φ). The meaning of quantifiers is also standard: I ⊧_{ν} ψ, where ψ = (∀X)φ (or ψ = (∃X)φ), if for every (resp., some) μ that agrees with ν everywhere, except possibly on X, I ⊧_{μ} ψ.

Clearly, for a closed formula, ψ, its meaning is independent from variable assignments, and we can simply write I ⊧ ψ. A semantic structure I is a model of ψ if I ⊧ ψ. If S is a set of formulae and φ a formula, we write S ⊧ φ (φ is logically implied or entailed by S) if and only if φ is true in every model of S.

3.4 Untyped Semantic Structures

To be able to talk about well-typed vs. ill-typed F-logic programs, we also introduce untyped semantic structures and models.

Untyped semantic structures for an F-logic language L are defined similarly to the ordinary F-logic semantic structures, except that the former are not required to satisfy the well-typing conditions of the previous subsection.

The notion of formula satisfaction by untyped structures goes unchanged. We use the same notation I ⊧_{ν} ψ (I ⊧ ψ, for closed formulas) to denote the fact that I satisfies ψ. An untyped semantic structure I such that I ⊧ ψ is called an untyped model of ψ.

It is easy to see that every typed semantic structure (or model) is also an untyped structure (resp., model) and that if I is an untyped model that is also a typed semantic structure then it is a typed model.

Although the notion of untyped logical entailment between formulas is immediate, we are not going to use it in the future. Therefore, if S is a set of formulas then S ⊧ ψ will always stand for the “typed” entailment defined in Section 3.3.

In the sequel, unqualified references to semantic structures (or models) will be made only to the typed versions of these concepts. However, for contrast, we will often add the qualifier “typed.” On the other hand, when untyped semantic structures are meant, the qualifier “untyped” will always be present.

3.5 Incorporating Relational-Style Programming

It is often convenient to have usual first-order predicates on a par with objects (cf. [CW89, KW89, AK89]). This happens when an application is more naturally described in a value-based setting, or when a mixture of predicates and objects is called for. For instance, one can primarily talk about objects, but occasionally may need to verify that certain objects stand in a particular (possibly user-defined) symmetric relationship to each other (e.g., equality, adjacency). Although such relationships can always be encoded as objects, often this is not the most natural representation. For instance, it would be awkward and unusual to represent equality between objects or inequality between numbers in this way. In this section we first show how predicates can be encoded as F-terms and then incorporate predicate terms into F-logic as first-class citizens, both syntacticly and semantically.

Predicates can be simulated in F-logic in several different ways. The approach described here is an adaptation from [KW89]. To encode an n-ary predicate symbol, p, introduce a new class, p. Let p tuple be a new n-ary function symbol. We then assert (∀X_{1} … ∀X_{n})(p tuple(X_{1}, ..., X_{n}) : p) and represent the predicate calculus atoms of the form p(T_{1}, ..., T_{n}) by means of F-terms

p tuple(T_{1}, ..., T_{n})[arg_{1} → T_{1}; ...; arg_{n} → T_{n}].

It is easily seen that by choosing p tuple(T_{1}, ..., T_{n}) to represent ids we made these objects value-oriented in the sense of [Ull87], that is, fully dependent on the values of their attributes.

To eliminate the need in going through the mental exercise of converting predicates into F-terms, we incorporate them into the semantics directly. In this paper, we leave the typing theory for predicates out and refer the reader to [KW90] for more details.

The expanded language now has a set ℘ of predicate symbols. If p ∈ ℘ is an n-ary predicate symbol and T_{1}, ..., T_{n} are F-terms, then p(T_{1}, ..., T_{n}) is a predicate term (abbr., P-term)

In accordance with the syntactic tradition of object-oriented languages, the syntax of P-terms is made slightly more general than that of atomic formulas in predicate calculus. For instance, project(john, oo hype[manager → you know who]) is a syntacticly correct P-term.

Observe that P-terms cannot be syntacticly confused^{5} with id-terms: Since we do not allow to drop brackets in degenerated molecular formulas, such as state(new york)[ ], the id-term state(new york) cannot be confused with a predicate term. Likewise, in bill[works for → state(new york)], state(new york) cannot be confused with a P-term, since P-terms cannot occur inside F-terms. However, as before, we will allow to drop “[ ]” in F-terms of the form T [ ], whenever these appear inside P-terms, which will permit us to write, say, p(t_{1}, ..., t_{n}) in lieu of p(t_{1}[ ], ..., t_{n}[ ]).

It should be also clear from the above encoding that the syntax of P-terms can be extended in the direction of HiLog [CKW89a, CKW89b] by allowing variables and even complex id-terms in place of predicate symbols; we will not pursue this extension here in order to leave room for other important issues.

A molecular formula (abbr., a molecule) is now either an F-term or a predicate term (including the equality, e.g., T ≐ S). A literal is either a molecular formula or a negated molecular formula.

Predicate symbols are interpreted as relations on U of appropriate arities, using the function I_{℘}:

• I_{℘}(p) ⊆ U^{n}, for any n-ary predicate symbol p ∈ ℘.

Given a semantic structure I = ⟨U, ≺_{U}, I_{F}, I_{℘}, I_{→}, I_{→ →}, I_{⇒}, I_{⇒ ⇒}⟩ and a variable assignment ν, I ⊧_{ν} p(T_{1}, ..., T_{n}) if and only if

• ⟨ν(T_{1}), ..., ν(T_{n})⟩ ∈ I_{℘}(p); and

• for i = 1, ..., n, I ⊧_{ν} T_{i}.

We also fix an interpretation for the equality predicate “≐”:

5We refer to the kind of a confusion that may arise in logic programming, where symbols are not explicitly declared to be functional or predicate.

• I_{℘}(≐) =^{def} {⟨a, a⟩|a ∈ U},

which implies that if T and S are id-terms, then I ⊧_{ν} (T ≐ S) if and only if ν(T) = ν(S).

It is easily seen that the above semantics for predicates coincides with the usual one when all the T_{i} are plain id-terms. To fully integrate P-terms into F-logic, we now let F-formulae to be built not only out of F-terms but also out of predicate terms (plus connectives and quantifiers). Truth of formulas in semantic structures and the notion of a model is defined in an obvious way.

4 F-logic as a Programming Language

To equip the reader with a better understanding of the intended usage of various components of Flogic, this section outlines an object-oriented declarative language based on this logic. We show that the monotonic semantics based on the entailment relation “⊧” of Section 3.3 is too weak for a logic programming language and introduce a nonmonotonic semantics on top of the monotonic one. A proof theory for the monotonic part of F-logic is given in Section 6; computational issues related to the nonmonotonic semantics will be discussed in a companion paper.

4.1 Databases and Queries

The simplest way to define a database or a logic program would be to say that it is a set of F-logic formulae. This definition is way too general, though, and we will soon restrict it to a more usable form. For the time being we will stay with this general concept and introduce some important notions, adapted from classic logic programming.

Given a language L with a set of variables V, a substitution is a mapping σ : V ⟼ {id-terms of L} that is an identity everywhere outside some finite set dom(σ) ⊆ V. This set is called the domain of σ. Any substitution can be extended to a mapping on id-terms as usual: σ(f(t_{1}, ..., t_{n})) = f(σ(t_{1}), ..., σ(t_{n})), and then to is-a and data F-terms: σ(Q : P) = σ(Q) : σ(P) and σ( Q[…; F unM @ R_{1}, …, R_{n} → T; ...; SetM @ V_{1},…, V_{m} → → {…, S, …}]; …) = σ(Q)[…; σ(F unM) @ σ(R_{1}),…, σ(R_{n}) → σ(T); …; σ(SetM) @ σ(V_{1}),…, σ(V_{m}) → → {…, σ(S), …}; …]. Extending σ to P-terms and signature F-terms is similar. Finally, substitutions are extended to F-formulae by letting them commute with logical connectives and quantifiers.

A substitution is ground if σ(X) ∈ F^{∗} for each X ∈ dom(σ), that is, if σ(X) has no variables. Given a substitution σ and a formula φ, σ(φ) is called an instance of φ. It is a ground instance if it contains no variables; a formula is ground if it has no variables.

A query is a statement of the form ? − Q, where Q is an F-term. The set of answers to ? − Q with respect to a program P is the smallest set of F-terms that

1. contains all instances q of Q logically entailed by P (i.e., P ⊧ q); and

2. is closed under “⊧”.

The second condition here is rather technical; it is included for the following simple reason: Suppose the database contains john[children → → {bob, sally}] and the query is ? − john[children → → {X}]. Then there are two instances of the query implied by this database: john[children → → {bob}] and john[children → → {sally}]. However, without the second condition, john[children → → {bob, sally}] would not be considered as an answer to the query, even though it is a logical consequence of the first two answers. On the other hand, john[children → → {bob, sally}] would be viewed as an answer to a logically equivalent query ? − john[children → → {X, Y }]. Condition (2) above eliminates such an anomaly.

In general, closing query answers with respect to “⊧” provides a simple and convenient way of talking about query equivalence and containment without having to bother with minor syntactic differences that may occur in essentially similar queries.

4.2 Class-Hierarchies, Types, and Objects

An F-logic program (or a database) consists of a set of oriented clauses, also called deductive rules, just as in classic logic programming. Each rule is assumed to be implicitly universally quantified. The difference, of course, is that F- and P-terms are used instead of atomic formulas of predicate calculus. As usual, rule-heads are positive literals. Literals in the body may be negated.

F-logic programs specify what each method is supposed to do, define method signatures, and organize objects along class hierarchies. Every program can be conceptually split into three disjoint components:

1. An object-base definition—containing all rules with P-terms and data F-terms in the head;

2. A class-hierarchy declaration—containing rules with is-a terms in the head;

3. A signature (or type) declaration—containing all rules with signature F-terms in the heads.

Nevertheless, as we shall see, these components cannot be considered independently from each other, since the rule-bodies in one component may contain literals defined in other components.

Informally, an object-base definition specifies what each method is supposed to do. Object definitions may be explicit or implicit, via deductive rules. Class-hierarchy declarations – as their name suggests – organize objects and classes into ISA-hierarchies. Signature declarations specify the types of arguments each method can take as well as the type of the method’s output.

Sometimes it may be desirable to circumscribe the equality, that is, to introduce an inference rule for deriving inequalities based on the fact that some equalities cannot be proved. In this case, F-logic programs may have an additional component, the equality definition. This issue is discussed in Section 4.4.

4.2.1 ISA Hierarchies

A program P determines its ISA-hierarchy as follows: if P ⊧ q : p then q is a subclass of p or an individual object belonging to p. It is also possible that P ⊧ (p ≐ q) (which entails both p : q and q : p), meaning that certain distinct denotations (object ids) do, in fact, refer to the same object or class, e.g., john ≐ father(mary) or children ≐ child(person).

Unfortunately, defining class hierarchies in the above way is not quite satisfactory, since logic rules cannot specify what is not a subclass of something. In general, specifying such negative information explicitly requires a huge and often infinite number of clauses of the form ¬q : p. To cope with this problem, researchers have been commonly using various techniques of nonmonotonic reasoning. In the simplest case of definite Horn clauses, a standard technique is the so called Reiter’s Closed World Assumption (abbr., CWA) that says that whenever P |̸= p : q then nonmonotonicly derive ¬p : q. For definite Horn clauses, CWA is tantamount to restricting logical entailment to minimal models only.

When logical rules have negation in the body, a number of (often incompatible) extensions of Reiter’s CWA have been proposed, which includes the perfect model semantics [Prz88], the stable model semantics [GL88], the well-founded semantics, [GRS88, Van89, Prz89], and the inflationary semantics [AV88, KP88]. Each of these semantics can be adapted to F-logic. As an illustration, Appendix A describes an adaptation of the perfect model semantics [Prz88]. In the present section, however, all examples involve definite Horn clauses only and therefore the aforesaid Reiter’s CWA suffices to describe the semantics of class hierarchies.

A common feature of all of the approaches mentioned above is that each distinguishes a subset of models, called canonic, and then defines the program semantics with respect to those models only. To assist the reader in coping with examples, we first define a simpler notion of minimal models; for definite Horn clauses, minimal models coincide with canonical models of all major approaches (at least in the Herbrand case).

Formally, we write M≪^{♯}N if and only if for every F- or P-term T, whenever M ⊧ T then also N ⊧ T. An untyped model M of a program P is minimal if for every untyped model N of P, N≪^{♯}M implies M≪^{♯}N. A typed minimal model is an untyped minimal model that in addition satisfies the well-typing conditions of Section 3.3 (i.e., is a typed semantic structure). Notice that to be a typed minimal model is a stronger requirement than to be ≪^{♯}-minimal within the class of all typed models of P.

Observe that our notion of minimality is defined for semantic structures with arbitrary domains, not necessarily for Herbrand interpretations. (Herbrand interpretations are defined in Section 5.2). Therefore, even for definite Horn clauses there may be several minimal models. However, if M and N are minimal models for a set of Horn clauses then the sets of all ground molecules that are true in M and N, respectively, coincide. We call semantic structures for a language L that agree on all ground molecules of L, equivalent. Furthermore, as in the classic theory, definite Horn programs have precisely one minimal Herbrand model.

An example of a class-hierarchy declaration is given in Figures 2 and 3 of Section 3.1. Among other things, it states that john is both a student and an employee, while phil is an employee but not a student. The latter is not stated explicitly and cannot be derived using the normal logical implication “⊧” of Section 3.3; it can be derived nonmonotonicly, though, since ¬phil : student holds in all minimal models of the formulas listed in Figure 3.

Some of the clauses in Figure 3, such as empl : person and student : person, actually deal with classes rather than individual objects; they illustrate a form of inclusion polymorphism available in Flogic. Saying that students and employees are persons implies that all properties (i.e., methods) defined for persons must automaticly hold for employees as well as students. For instance, in Figure 4 such properties are name (a single-valued 0-ary method that returns objects of class string), joint works (a set-valued method that expects a single argument of class person and returns results of type report), and so on.

In F-logic, classes are denoted by id-terms, so they may contain variables. This gives us the flexibility needed to support parametric polymorphism. For example, the following pair of clauses defines a parametric polymorphic type list(T):

\begin{matrix}nil : list(T) \\ cons(X, Y) : list(T) ← X : T & Y : list(T). \end{matrix}

For instance, if int denotes the type of integers then list(int) is the type of lists of integers containing elements such as nil, cons(0, nil), cons(0, cons(1, nil)), and so on.

As noted earlier, ISA-hierarchies may depend on other data. This is especially useful when classes need be determined dynamicly, based on properties of objects that are expected to populate these classes:

Car : diesel cars(Y ear) ← Car : automobile[engine type → “diesel”; make year → Y ear].

The above rule defines a set of classes, diesel cars(Y ear), parameterized by the year in which these cars were produced. Each class, e.g., diesel cars(1990), is inhabited by objects representing cars made in 1990 and having a Diesel engine. Furthermore, ISA-hierarchies may depend on objects’ typing, as in

X : sellable item ← X[price ⇒ { }],  (1)

which defines the class of all sellable items, that is, objects to which the attribute price is applicable.^{6} Thus, an object is sellable even though the price-attribute may not have any value, at present. For instance, if P is a program, we may have P ⊧ john[price ⇒ $$] (i.e., john is up for sale) but P |̸= ∃Xjohn[price → X] (i.e., john hasn’t made up his mind yet as to how much he is worth). Nevertheless, even though price of john is undefined here, (1) guarantees that P ⊧ john : sellable item holds true.

4.2.2 Type Declarations

Typing is a popular concept in programming languages; in its primitive form it was used in traditional database systems under the disguise of schema declaration. Typing can be very useful both as a debugging aid and as a means of maintaining data integrity. It allows the user to define correct usage of objects and then let the system detect ill-typed data and queries. The purpose of type declarations is to impose type-constraints on arguments of methods as well as on the results returned by the methods. For instance, in

6This example is due to Serge Abiteboul.

\begin{matrix}faculty[boss ⇒ \{faculty, mngr\}] \\ empl[salary @ year ⇒ \{int\}], \end{matrix}

the first F-term states that boss is a function that, when applied in the scope of a faculty-object, returns an object that simultaneously belongs to classes faculty and mngr. The second clause says that salary must be a function that, when applied in the scope of an empl-object to a year-object, returns an integer. It is easy to see from the definitions that these type-constraints do force employees’ salaries in any given year to be an integer, provided that only typed minimal models are considered.

Suppose that not only do we want to enforce types for the methods specified in signature F-terms, but also to make it illegal for an object to use any method whose signature was specified neither for this object nor for one of its superclasses. For instance, in relational model one can only use attributes that are defined for a particular relation and any attempt to use an attribute that is not defined for this relation will normally result in an error. Similar policies are enforced in a number of strongly typed object-oriented languages. In the above example, one may want to make it illegal for a faculty-object to use methods other than salary and boss; for employees who are not faculty, even the use of the method boss should be banned. We could say that the signature (or schema, in the database terminology) of empl-objects contains only one method, salary, while the signature of faculty objects has precisely two methods, salary and boss, both functional and expecting one and zero arguments, respectively.

For Horn clauses, the notion of minimal models of the previous subsection can be used to enforce signatures as follows: We say that P is well-typed if and only if at least one of its minimal models is also a typed semantic structure. Suitability of this definition is supported by the following: Let the type-constraints declared in P be the set of all ground signatures that are true in one (and hence in all) minimal untyped models of P. It can be easily verified that well-typedness then means that the domain of definition and the output of every method defined by P satisfies all type-constraints declared in P. Furthermore, the first well-typing condition in Section 3.3 ensures that every method defined by P has a nontrivial declared signature. For instance,

\begin{matrix}john[name → “John”] \\ X : named ← X[name → N] \\ X[name ⇒ string] ← X : named \end{matrix}  (2)

has a minimal typed model (and thus (2) is a well-typed program), while

\begin{matrix}john[age → 49] \\ X : has age ← X[age → A] \\ X[name ⇒ string] ← X : has age \end{matrix}  (3)

does not have such models. Untyped minimal models of (3) do not qualify as typed semantic structures because the method age has no declared signature and hence ¬john[age ⇒ { }] holds true in every such model. This, together with john[age → 49], defeats the first well-typing requirement for typed semantic structures (Section 3.3). Nevertheless, since (3) does have untyped minimal models, this means that the aforesaid problem is due to typing rather than data, that is, (3) is ill-typed.

Note that if we had stated that john[age ⇒ { }] or john[age ⇒ int] then (3) would have had a signature minimal model. The second signature would ensure that the value of age is always an integer. In contrast, the first signature does not impose any restriction on the values of age; its only purpose is to say that age is a legal method applicable to john.

The following are examples of parametric polymorphic signatures expressible via F-logic type declarations:

\begin{matrix}X[self ⇒ X] \\ list(T)[first ⇒ T; rest ⇒ list(T); length ⇒ int; append @ list(T) ⇒ list(T)]. \end{matrix}

Occasionally, methods may have types that are intersections or unions of simpler types:

\begin{aligned}I : or(T_{1}, T_{2}) & ← & I : T_{1} \\ I : or(T_{1}, T_{2}) & ← & I : T_{2} \\ I : and(T_{1}, T_{2}) & ← & I : T_{1} & I : T_{2}. \end{aligned}

Now we can define quite fancy signatures:

company[lucrative products @ and(prestigious category, hi ticket category) ⇒ ⇒
or(financial, merchandise) ]

Here lucrative products is a method that, given an argument of type prestigious category and provided that this is also a category of high-ticket items, returns the set of all products in that category sold by the company. These products may be either financial or merchandise. In particular, the set of objects returned by this method may be heterogeneous.

4.3 Well-Typed Canonic Models

We now define a semantics for F-logic programs more systematicly. It should be clear that, as usual in logic programming, semantics is given non-algorithmicly by characterizing canonic models via certain minimality conditions. Algorithmic aspects of this semantics are beyond the scope of this paper.

A distinctive feature of our approach is its ability to define the concept of type error in precise modeltheoretic terms. This notion was treated only informally in the papers on object-oriented databases (cf. [AK89]). In the works on typed functional languages, well-typedness is usually defined procedurally rather than semantically. In logic programming, model-theoretic characterization of type-correctness was proposed in [Xu89, XW88], where the semantics was given in terms of partial interpretations. However, the theory in [Xu89, XW88] is partly procedural since it involves program transformation. Semantic approaches were also reported in [Mis84, YS87] and several other papers. In all these works, however, the notion of a type is extra-logical (or, better to say, it is part of a logical theory that is distinct from that of the program). In contrast, in our approach types (i.e., signatures) and data are expressed in one universal logical calculus. Our approach is also more expressive, especially when it comes to polymorphic types. We refer the reader to [KW90] for a more detailed discussion.

Let P be a program. As usual in logic programming, we define the semantics of such programs via a subclass of canonic untyped models of P. For concreteness, the reader can assume the perfect-model semantics introduced in Appendix A, in which case an untyped model is canonic if and only if it is perfect (i.e., ≪-minimal among all untyped models of P, where “≪” is the preference quasi-order defined in Appendix A). Those who can live comfortably without negation, may handily think of a simpler notion of ≪^{♯}-minimal untyped models defined in Section 4.2.1 (“≪” reduces to “≪^{♯}” when P consists of Horn clauses). The above canonic models are untyped. To account for type declarations, we define:

• A typed canonic model of P is an untyped canonic model for P that in addition fulfills the well-typing conditions of Section 3.3 (and thus is a typed semantic structure).

Notice that every typed canonic model is also ≪-minimal within the class of typed models of P. However, the latter property does not entail the former: a model M may be ≪-minimal within the class of typed models of P but may not be minimal among the untyped models of P and hence M may not be a typed canonic model.

Semantics of F-logic programs is now defined with respect to the typed canonic models, that is, P |≈ φ if and only if M ⊧ φ, for every typed canonic model M of P.

Unlike many other formalisms, F-logic can formally distinguish between inconsistency due to type errors and inconsistency arising from other causes: A program has a type error if it has no typed canonic model, but does have untyped canonic models.

This definition seems to capture the intuition about type errors quite adequately: If P has an untyped canonic model but has no typed ones, the problem can be clearly traced to the typing. For an example, consider the following program P:

bob : faculty  1989 : year  empl[boss ⇒ {faculty}; salary @ year ⇒ {int}]
mary : faculty  10000 : int  mary[boss → bob]
faculty : empl.

An untyped canonic model of P is any model in which precisely the following holds true:

faculty : empl  bob : faculty  1989 : year
bob : empl  mary : faculty  10000 : int

mary : empl mary[boss → bob]

\begin{matrix}empl[boss ⇒ \{faculty, empl\}; salary @ year ⇒ \{int\}] \\ faculty[boss ⇒ \{faculty, empl\}; salary @ year ⇒ \{int\}] \end{matrix}

(plus tautologies, such as empl : empl, and the logical consequences of the above). Each such model satisfies the well-typing conditions of Section 3.3 and therefore is a typed semantic structure. Hence, P is well-typed.

Suppose now that P contains the term mary[boss → john] instead of mary[boss → bob]. Then P would have had a type error because, in every untyped canonic model, the data F-term mary[boss → john] clashes with the typing empl[boss ⇒ {faculty}], as john is not known to be a faculty (hence ¬john : faculty holds in every untyped canonic model of P). Likewise, the clause mary[salary → 10000] would have caused a type error. Indeed, since no signature has been specified for the 0-ary version of the method salary (P has a signature term only for the 1-ary version of salary), ¬mary[salary ⇒ { }] must hold in every canonic model of P. But this, together with mary[salary → 10000] defeats the first well-typing condition of Section 3.3.

The definition of well-typedness given above provides semantic grounds for developing static typechecking algorithms. Unlike other works, the model-theoretic definition of well-typedness in F-logic makes it possible to prove correctness of various such algorithms and provides a uniform framework for their comparison. We will discuss static type checking in more detail in a companion paper. For classic logic programs, this issue is elaborated upon in [KW90].

The semantics of well-typedness presented here is appropriate for systems that require programmers to supply complete type specifications. It has been argued that in logic programming this may be too burdensome (e.g., [Mis84, XW88]). Adapting the ideas from ML to Prolog, Mishra [Mis84] proposed to use type-inferencing for predicates whose types are not explicitly defined by the programmer, and view the inferred typing as the intended typing specification.

Semantics of type-inference is different from the one outlined above. Briefly, given a program P, its inferred type is the “strongest” type declaration under which P is type-correct. If the pure type-checking idea has been criticized as being too taxing, pure type-inference is too week and cannot capture the concept of method signatures adequately. We feel that type-inference combined with type checking is a suitable compromise. Details of this approach can be found in [KW90]; in a different setting, this idea was also advocated in [YS87, Xu89].

As usual with nonmonotonic theories, the entailment relation “|≈” is not recursively enumerable and therefore a complete proof theory does not exist. This phenomenon is well known even for relatively simple cases, such as stratified logic programs [She88]. In these situations, the standard approach is to find an algorithm that can evaluate most of the interesting queries, where “most” is necessarily taken informally. Such algorithms are beyond the scope of this paper. Instead, in Sections 5 and 6 we study properties of the monotonic part of F-logic^{7} and show that it has a sound and complete proof theory.

4.4 Equality

As discussed earlier, literals involving equality may occur in the rule-heads of object-base definitions. However, such literals may also be generated in other ways. For example, john[father → bob] and john[ father → dad(john)] logically entail bob ≐ dad(john), as do bob : dad(john) and dad(john) : bob. This may be problematic from the practical point of view, since multiply-defined functional methods or cycles in the class-hierarchy may be the result of a programmer’s mistake. Therefore, it may be desirable to regard programs such as { john[father → bob], john[father → dad(john)] } as devoid of canonic models, unless dad(john) ≐ bob is given explicitly. Therefore, we need means to tell the system which equalities are intended and which are not. To this end, one could simply assert t ≠ s for every pair of unequal id-terms, but this would obviously be impractical. A better way to achieve the same goal is to employ the minimization principle once again.

7The monotonic F-logic is characterized by the logical entailment “⊧” defined in Section 3.3, as opposed to the nonmonotonic entailment “|≈” introduced in the present subsection.

Formally, we split each program, P, into two disjoint parts, EQ and P′, where EQ is supposed to define equalities while P′ describes the rest. The equality definition, EQ, consists of a finite set of definite Horn rules involving the equality predicate only. The other part, P′, is as before, except that equality is no longer permitted in the rule heads. Then we can introduce an order on semantic structures ⊑^{eq}, where M⊑^{eq}N if whenever M ⊧ (t ≐ s) then also N ⊧ (t ≐ s).

We then define an untyped model of P =^{def} EQ ∪ P′ to be minimal for equality if it is ⊑^{eq}-minimal among all untyped models of EQ (that are not necessarily the models of P). The desired semantics now results, if in the definition of canonic models we apply ⊑^{eq}-minimization prior to ≪-minimization.

More precisely, when equality is circumscribed, an untyped model of P is canonic if it is ≪-minimal among the untyped models of P that are minimal for equality. Again, P is well-typed if one of the models obtained by this cascaded minimization is also a typed semantic structure.

Coming back to our example, bob ≠ dad(john) holds in all ⊑^{eq}-minimal models of EQ (where EQ is empty in this case) and hence the program { john[father → bob], john[father → dad(john)] } has no ⊑^{eq}-minimal model.

4.5 Inheritance

The notion of inheritance is fundamental in AI and object-oriented programming and a number of researchers worked on combining this idea with programming languages. Cardelli [Car84] considered inheritance in the framework of functional programming. He described a type inference procedure that is sound with respect to the denotational semantics of his system. Sound type inference systems for functional languages were also discussed in [Mit90, CHC90] and in several other papers.

In contrast to all these works, we have devised a first-order logic in which type (signature) inheritance is built into the semantics, and the proof procedure is sound and complete. We also consider nonmonotonic inheritance of methods – not just signatures – where methods defined for subclasses can override those inherited from superclasses. This difficult issue was not addressed in [Car84, Mit90, CHC90] at all.

LOGIN [AN86] was an attempt to incorporate inheritance into logic programming by means of a unification algorithm. However, LOGIN had certain semantic problems and it was not clear in which logic this unification algorithm would yield a sound proof procedure. Only recently it was shown by Chen [Che90] that the LOGIN unification algorithm can be viewed as a form of abductive reasoning about types; this formalism is therefore unsuitable for query answering in databases and logic programming. Similar observation was made in [Mai86].

4.5.1 Monotonic Inheritance of Signatures

In F-logic, signatures are inherited monotonicly in the sense that if r : p and r : q both hold then r inherits the signatures of p and q in a “cumulative” manner. For instance, let the database contain:

\begin{matrix}empl : person & person[name ⇒ \{string\}] \\ assistant : student & student[drinks ⇒ ⇒ \{beer\}; drives @ year ⇒ \{bargain\}] \\ assistant : empl & empl[salary ⇒ \{int\}; drives @ year ⇒ \{vehicle\}]. \end{matrix}

Here assistant inherits the signature assistant[name ⇒ {string}; drinks ⇒ ⇒ {beer}; drives @ year ⇒ {bargain, vehicle}; salary ⇒ {int}]. In other words, an assistant has a name as a person, a salary as an employee, and drinks beverages of type beer; at different times he also drives vehicles (as an employee), which he must have obtained at a bargain price (as a student). Thus, assistants monotonicly “accumulate” all signatures they inherit from student, person, and empl. Monotonic signature-inheritance is a logic counterpart of the so called coherence requirement to method schemes (cf. [AKW90]).

Theorem 4.1 (Inheritance of Signatures) Let P be a program, t = p[ funM @ u_{1}, ..., u_{n} ⇒ {q}; setM @w_{1}, ..., w_{m} ⇒ ⇒ {r}] be a ground F-term and P ⊧ t. Suppose p′ ∈ F^{∗} is a ground id-term such that P ⊧ p′ : p, that is, p′ is an instance or a subclass of class p. Then

P ⊧ p′[funM @ u_{1}, ..., u_{n} ⇒ {q}; setM @ w_{1}, ..., w_{m} ⇒ ⇒ {r}].

In words, whenever p′ is a subclass of p, signatures of methods attached to p are inherited by p′.

Proof: The result directly follows from the definitions: Let s denote p′[funM @ u_{1}, ..., u_{n} ⇒ {q}; setM @ w_{1}, ..., w_{m} ⇒ ⇒ {r}]. Consider a model I = ⟨U, ≺_{U}, I_{F}, I_{℘}, I_{→}, I_{→ →}, I_{⇒}, I_{⇒ ⇒}⟩ of P. Since P ⊧ t, we conclude that I ⊧ t; hence for every variable assignment ν, it follows from (4) and (5) of Section 3.3 that

• ν(q) ∈ I_{⇒}(ν(funM)) (ν(p), ν(u_{1}), ..., ν(u_{n}));

• ν(r) ∈ I_{⇒ ⇒}(ν(setM)) (ν(p), ν(w_{1}), ..., ν(w_{m}));

• I ⊧ q ∧ r (note: q, r are F-terms).

Therefore, since P ⊧ p′ : p and hence ν(p′)⪯_{U}ν(p), we conclude by the anti-monotonicity of I_{⇒}(ν(funM)) and I_{⇒ ⇒}(ν(setM)) (see Section 3.3):

• ν(q) ∈ I_{⇒}(ν(funM)) (ν(p′), ν(u_{1}), ..., ν(u_{n}));

• ν(r) ∈ I_{⇒ ⇒}(ν(setM)) (ν(p′), ν(w_{1}), ..., ν(w_{m}));

• I ⊧ q ∧ r.

I ⊧ s now follows from definitions (4) and (5) of Section 3.3. □

4.5.2 Nonmonotonic Inheritance of Methods

Unlike the monotonic signature-inheritance, F-logic methods are inherited nonmonotonicly, meaning that methods defined for subclasses may override those inherited from superclasses. Nonmonotonic inheritance is a subject of intensive research (e.g., [ER83, Tou86, THT87, HTT87, Bre87, KK89, KKW89b, GV89, KKW89a, PG89]). In this section we give semantics to inheritance in F-logic and point out the differences with some other works.

On one hand, the framework for inheritance set out in [Tou86] (and adopted in most other works) is more general than ours because we distinguish between classes and properties while [Tou86] does not. This enables us to impose a restriction that the subclass relationship is non-defeasible, while property inheritance can be overwritten, which rules out most of the notoriously tricky inheritance networks discussed in the aforementioned papers.^{8} We believe, however, that Touretzky’s model [Tou86] that is in the basis of all of the above approaches is way too general and is more of a philosophic rather than practical interest. This generality seems to be a major obstacle to defining model-theoretic semantics of inheritance networks. Fortunately, because of the special form of inheritance networks arising in F-logic programs, nonmonotonic inheritance in F-logic is better amenable to model-theoretic characterization.

On the other hand, inheritance in F-logic is intermixed with the ordinary logical deduction—an aspect not dealt with in any of the aforementioned works. This interaction between inheritance and deduction makes our task more difficult but also more interesting, contributing to the general understanding of such interaction.^{9} Another generalization is that F-logic classes inherit methods (which are functions), while in [Tou86] and other works classes can inherit values only (i.e., 0-ary functions). It is also unclear how inheritance of our set-valued attributes can be captured in the framework of [Tou86] et. al.

The novelty of our approach is in describing the semantics of inheritance using Shoham’s minimization principle [Sho88] directly on the original set of specifications, which results in a very transparent definition.

The main idea behind the model-theory of nonmonotonic inheritance in F-logic consists in defining a quasi-order ⊑^{inh} over models, where “smaller” means that the results returned by some of the methods change “less” when descending down the class hierarchy. This is close in spirit to the recent paper of Thomason and Horty [TH89]. To illustrate our ideas, consider the following example [Tou86]:

\begin{matrix}royal elephant : elephant & elephant[color → “grey”] \\ clyde : royal elephant & royal elephant[color → “white”]. \end{matrix}

There is a model I where color maps elephant, royal elephant, and clyde to “grey”, “white”, and “white”, respectively, which is smaller than the model I′ in which clyde is mapped to, say, “green.” This is because when we descend from royal elephant to clyde the color does not change in the first model, but does in the second. Notice that the semantic structure I′′ that maps royal elephant and clyde to “grey” is even smaller than I because in I′′ the color does not change also when we descend from elephant to royal elephant. However, I′′ is not a model for the above set of facts, as it violates royal elephant[color → “white”]. So, I is a ⊑^{inh}-minimal model.

8It should be noted that the intended interpretation of some complicated inheritance networks is a subject of debates.

9There are several possible ways to combine inheritance with deduction. Our choice was motivated by the conceptual simplicity of the definitions and of the corresponding computation.

Observe how overriding has taken place in the above example: Royal elephants must be “white” in order to satisfy the fourth clause. Therefore, a model, such as I, in which Clyde’s color is “white” is preferred over the models where Clyde has some other color (e.g., I′), and no other model is ⊑^{inh}-smaller than I.

Put this yet another way, the quasi-order ⊑^{inh} we are looking for must embody the, so called, Touretzky’s principle [Tou86] according to which inheritance of a property from a more specific superclass (e.g., royal elephant) should override inheritance due to a less specific superclass (elephant, in our case). In case of conflicting multiple inheritance, we follow the so called credulous approach [THT87] that allows objects to inherit either of the possibilities. The following example from [Tou86] is commonly known as Nixon’s Diamond:

\begin{matrix}nixon : quaker & quaker[policy → pacifist] \\ nixon : republican & republican[policy → hawk]. \end{matrix}

Here, we have two ⊑^{inh}-minimal models: one in which nixon is a pacifist and another in which he is not. Conflict resolution that follows the credulous approach is not the only possible one; model theory for other approaches used in practice (e.g., skeptic [HTT87, KKW89b]) can be defined along the same lines.^{10} In Section 7.7 we discuss so called user-defined inheritance—an ad hoc idea used in several existing object-oriented languages [Mey88, LR89].

Despite the simple intuition underlying the concept of ⊑^{inh}-ordering, its rigorous definition is not a trivial matter, and some “obvious” solutions do not work. One possible direction is to define a notion of “1-step inheritance” in which I ⊑^{inh} J, where I and J are semantic structures, if I is obtained from J by changing the behaviour of one of the methods, m, on one of the classes, say cl, to the behaviour of m on an immediate superclass, supcl, of cl.^{11} In other words, unlike J, in I the method m, when invoked in the scope of classes cl and supcl, returns the same value for any given set of arguments.^{12} For all other classes and methods, I and J must behave similarly. For instance, in the Royal-Elephant example, the semantic structure I is obtained from I′ by 1-step inheritance (of attribute color) and, in turn, I′′ can be obtained from I by two steps of inheritance (I′′ is not a model in the Royal-Elephant example, though).

Having defined ⊑^{inh} via 1-step inheritance, we could further close it transitively, obtaining a quasiorder. There is a problem with the above definition, though: the very notion of “immediateness’ of a superclass. Even if one restricts the domain of semantic structures to just the Herbrand universe, it is possible to construct a set of deductive rules that force “:” to have condensation points with respect to the order ≺_{U} on the Herbrand universe U. For instance,

10To this end, we will only have to change the definition of ⊑^{inh} below to allow the result of a method to be undefined in case of an inheritance conflict.

11The notion of 1-step inheritance was suggested by Serge Abiteboul for a special case of class hierarchies.

12The requirement that supcl must be an immediate superclass of cl is essential here for, due to Touretzky’s principle mentioned earlier, an intermediate class, cl′, where cl : cl′ : supcl may override inheritance from supcl to cl.

\begin{matrix}a : b & a ≠ b & b : c & b ≠ c \\ X : f(X) ← X : b & X ≠ b & g(Y) : Y ← b : Y & b ≠ Y \\ f(X) : b ← X : b & X ≠ b & b : g(Y) ← b : Y & b ≠ Y \end{matrix}

defines an infinite chain a : f(a) : …: f^{n}(a) : …: b : …: g^{m}(c) : …: g(c) : c. If no other constant of function symbol is present in the language then b has neither an immediate predecessor nor an immediate successor and so, using 1-step inheritance, neither b can inherit from c, nor a from b.

Having absorbed the motivation, we are now in a position to define ⊑^{inh} rigorously. We will use the following notation: Let I be a semantic structure, obj and m be ground id-terms, and args^{⟶}= ⟨a_{1}, ..., a_{k}⟩ be a vector of ground id-terms. Then

I(m, →)[obj](args^{⟶}) = \{ \begin{matrix}\{val | I ⊧ obj[m @ args^{⟶}→ val]\} & if at least one such val exists \\ undefined & otherwise. \end{matrix}

I(m, → →)[obj](args^{⟶}) = \{ \begin{matrix}\{val | I ⊧ obj[m @ args^{⟶}→ → \{val\}]\} & if I ⊧ obj[m @ args^{⟶}→ → \{ \}] \\ undefined & otherwise. \end{matrix}

In other words, I(m, →)[obj](args^{⟶}) (or I(m, → →)[obj](args^{⟶})) is a result of application of a functional (resp., set-valued) method m to arguments args^{⟶} on the object obj with respect to the semantic structure I. Notice that I(m, →)[obj](args^{⟶}) and I(m, → →)[obj](args^{⟶}) are sets of ground id-terms, as opposed to I_{→}(...)(...) and I_{→ →}(...)(...), which are composed of the elements of the domain of I.

The requisite quasi-order, ⊑^{inh}, is now defined as follows: Let I and J be a pair of semantic structures. We write I ⊑^{inh} J if either of the following conditions is satisfied:

• There are ground id-terms obj, m and a vector of ground id-terms args^{⟶} such that I(m, →)[obj](args^{⟶})

is defined and

I(m, →)[obj](args^{⟶}) ≠ J(m, →)[obj](args^{⟶}).

In addition, there is a ground id-term cl such that the following conditions hold true:

– I ⊧ obj : cl, J ⊧ obj : cl, and I(m, →)[cl](args^{⟶}) = J(m, →)[cl](args^{⟶}); and

– For every mid ∈ F^{∗} such that I ⊧ obj : mid ∧ mid : cl, it is the case that

I(m, →)[mid](args^{⟶}) = I(m, →)[cl](args^{⟶}) = I(m, →)[obj](args^{⟶}).

(In particular, I(m, →)[mid](args^{⟶}), I(m, →)[cl](args^{⟶}), and J(m, →)[cl](args^{⟶}) are defined.)

• Similarly for set-valued occurrences of methods: Just replace I(m, →)[…](args^{⟶}) by

I(m, → →)[…](args^{⟶}) and J(m, →)[…](args^{⟶}) by J(m, → →)[…](args^{⟶}).

In addition, to make ⊑^{inh} a quasi-order, we close it transitively.

Informally, I is smaller than J if for some object obj such that I and J disagree on the interpretation of some method m on some arguments args^{⟶}, I can produce an “evidence” that the behaviour of m is obtained by inheritance. Noteworthy, J may produce another evidence in support of its own version of the behaviour for m; in this case J ⊑^{inh} I may hold as well. Therefore, ⊑^{inh} is only a quasi-order.

In the above definition, it is possible that I ⊧ (obj ≐ cl), yet it is always the case that J |̸= (obj ≐ cl). In particular, obj and cl are not identical id-terms. The latter follows from the the definition, since

J(m, →)[obj](args^{⟶}) ≠ I(m, →)[obj](args^{⟶}) = I(m, →)[cl](args^{⟶}) = J(m, →)[cl](args^{⟶}).

We now define models that are minimal for inheritance as follows:

• An untyped model M of P is minimal for inheritance (abbr., ⊑^{inh}-minimal) if and only if for every other untyped model N, N ⊑^{inh} M implies M ⊑^{inh} N.

To combine the perfect-model semantics (see Appendix A) with inheritance, we need to modify the definitions of Section 4.3 as follows. Let P be a program.

• An untyped canonic model of P is any untyped semantic structure that is ≪-minimal^{13} among the ⊑^{inh}-minimal untyped models of P.

• A typed canonic model of P is any typed semantic structure that is also an untyped canonic model for P.

Next we re-define P |≈ q as follows:

• P |≈ φ if and only if M ⊧ φ for every typed canonic model of P.

The above definitions do not assume equality minimization discussed in Section 4.4. If the latter is desired, then the definitions must be modified as follows: The program P will now be a disjoint union of two components: EQ, and P′, where EQ is the equality definition introduced in Section 4.4. In addition, ⊑^{eq}-minimization would have to be performed before the ⊑^{inh}-minimization.

The order in which various quasi-orders are applied is crucial and deserves further comments. Given a program P, the first most important step is to determine object denotations that refer to the same thing. This is done by minimizing the untyped models of EQ (that are not necessarily the models of P) with respect to ⊑^{eq}. The next step is to enforce inheritance by further restricting attention to ⊑^{inh}-minimal models of P among the ⊑^{eq}-minimal models of EQ. Canonic models of P are extracted from the latter by a subsequent minimization relatively to the preference quasi-order “≪”. The ⊑^{inh}-minimization must precede the ≪-minimization, for otherwise programs such as (signatures omitted)

a : b
b[attr → c]
e : f ← a[attr → c]

13As before, “≪” is the preference quasi-order on models, defined in Appendix A. It reduces to the simpler ≪^{♯}-order of Section 4.2.1, provided that P is Horn.

would have “strange” canonic models in which e : f and a[attr → c] are false, because these F-terms would be eliminated by ≪-minimization. On the other hand, if ≪-minimization follows ⊑^{inh}-minimization, the canonic model will satisfy both of these F-terms (because a inherits attr → c from b, by ⊑^{inh}- minimization), which agrees with the intuition. To illustrate some subtleties of our definitions, we do not assume equality minimization in the following examples.

It is important to keep in mind that the desired effect of nonmonotonic inheritance is achieved only with respect to canonic models. An essential ingredient here is the minimality of such models, which acts as an antibody that precludes unwanted inheritance coming from “unintended” superclasses. For instance, minimality precludes clyde from becoming an instance of, say, the class blue-things (in some non-canonic semantic structures), which would have caused clyde to inherit the color “blue”. Recasting our classic examples in terms of this new entailment relation “|≈”, yields:

Royal-Elephant |≈ clyde[color → “white”]
Nixon’s Diamond |≈ nixon[policy → pacifist] ∨ nixon[policy → hawk]

i.e. in the Royal-Elephant example, clyde[color → “white”] is true in every canonic model; in the Nixon’s Diamond case, either nixon[policy → pacifist] or nixon[policy → hawk] should hold in every such model.

The next series of examples illustrates how inheritance-overriding works. Suppose the object-base is

\begin{matrix}a : b \\ b[attr → c] \\ a[attr → d]. \end{matrix}

The intention here is that the clause a[attr → d] should overwrite the inheritance of attr → c from b and that ¬a[attr → c] must hold. Clearly, a[attr → d] holds in all models. The F-term b[attr → c] may also hold in certain models where c ≐ d is satisfied. The definition of ⊑^{inh} is tolerant enough so that among ⊑^{inh}-minimal models there are those in which c ≐ d is satisfied and those in which it is not. However, the non-canonic model where c ≐ d holds will be eliminated later during the ≪-minimization step.

According to our definitions, methods are overwritten not as a whole, but rather point-wise.^{14} For instance, in the following program

\begin{matrix}a : b \\ b[m @ c → d; m @ e → f] \\ a[m @ c → g] \end{matrix}  (4)

inheritance of m @ c → d is overwritten, but that of m @ e → f is not. In particular, the reader can verify that a[m @ c → g; m @ e → f] and ¬a[m @ c → d] hold in all canonic models of (4).

Our next example deals with overriding of set-valued methods. Consider the following example:

\begin{matrix}a : b \\ b[attr_{1} → → \{f, g\}, attr_{2} → → \{f, g\}] \\ a[attr_{1} → → \{f\}, attr_{2} → → \{h, f\}]. \end{matrix}  (5)

Here, a inherits attr_{1} → → {f, g} from b, while the inheritance of attr_{2} → → {f, g} is overwritten. We leave it to the reader to verify that this is indeed the case. A somewhat unusual effect in (5) is that the inheritance of attr_{1} is not overwritten, even though this attribute is explicitly defined for a. In general, according to our semantics of set-valued methods, subsets (like {f} above) do not override supersets (such as {f, g} in (5) ). Whether this is a bug or a feature remains to be seen: our choice was motivated by the conceptual simplicity of the resulting definition for ⊑^{inh}.

14Example (15) of Section 8.2 explains how a method can be overwritten as a whole rather than in a point-wise manner.

Finally, we illustrate how inheritance may interact with typing. Consider the following:

\begin{matrix}two : int & sup[attr → two; attr ⇒ int] \\ sub : sup & sub[attr ⇒ prime] ← sub[attr → two] \\ prime : int. \end{matrix}  (6)

In every untyped canonic model of (6), sub inherits attr → two from sup, and then the last rule derives the signature sub[attr ⇒ prime]. However, this signature conflicts with the atom sub[attr → two], previously obtained by inheritance. The conflict arises because ¬two : prime holds in every untyped canonic model. Therefore, no such model of (6) can be a typed semantic structure. Notice that in the absence of inheritance, the above program would have been well-typed.

In this paper we will not delve into the computational issues related to inheritance. Just to give the reader an idea about the subtlety of interaction between inheritance and deduction (even without considering negation), we will discuss a few typical examples in Appendix B. The perfect-model semantics in the presence of inheritance is given in Appendix C.

4.5.3 Discussion

As we have seen, the monotonic inheritance of signatures is built into the basic semantics of F-logic (i.e., into the logical entailment relation “⊧”), while inheritance of methods is defined at the meta-level, via a minimization principle. This is because method-inheritance involves a non-monotonic derivation rule and, if built into a logic, is likely to upset all chances for finding a complete proof procedure. Although, after the incorporation of nonmonotonic inheritance the entailment relation “|≈” also becomes non-recursively enumerable (and one may want to argue that thus not much has been gained), we believe that it is generally a good idea to decompose a complex task into independent subproblems and treat them separately. Another advantage is that keeping the minimization principle separate from the rest allows us to defer commitment to any specific nonmonotonic theory: F-logic thus becomes a foundation on which several different theories of inheritance can be built.

The monotonic signature-inheritance could also be defined axiomaticly instead of being built-in. For instance, we could define all n-ary signatures to be monotonic via the rules

\begin{aligned}X[F unM @ Z_{1}, ..., Z_{n} ⇒ \{V \}] & ← & Y [F unM @ Z_{1}, ..., Z_{n} ⇒ \{V \}] & X : Y \\ X[SetM @ Z_{1}, ..., Z_{n} ⇒ ⇒ \{V \}] & ← & Y [SetM @ Z_{1}, ..., Z_{n} ⇒ ⇒ \{V \}] & X : Y. \end{aligned}  (7)

Nevertheless, we chose to cast the monotonic inheritance of signatures into the semantics because this does not affect completeness of the proof procedure and because, according to our philosophy, the goal of logical modeling of various knowledge representation paradigms is to develop suitable formalisms that embed as much of the semantics as is practical.

Under these circumstances, the only argument for adopting an axiomatic approach to monotonic inheritance seems to be the fact that then we could selectively override signatures, similarly to overriding method definitions. For instance, the method age could have one signature for the class person and a different one for student. However, signature overriding seems to be defeating the whole purpose of typing and we believe that the perceived need in such overriding is usually caused by poor program design. Besides, the inheritance blocking mechanism described below may be an appropriate substitute for signature overriding.

Finally, observe that the monotonic inheritance can also be defined for methods via axioms similar to (7). For example, to state that some specific n-ary methods, funM and setM, should behave monotonicly with respect to inheritance, we can write:

\begin{aligned}X[funM @ Z_{1}, ..., Z_{n} → V] & ← & Y [funM @ Z_{1}, ..., Z_{n} → V] & & X : Y \\ X[setM @ Z_{1}, ..., Z_{n} → → \{V \}] & ← & Y [setM @ Z_{1}, ..., Z_{n} → → \{V \}] & & X : Y. \end{aligned}  (8)

The monotonic inheritance defined in this way is compatible with the semantics for nonmonotonic inheritance. Indeed, (8) constitutes an explicit definition of funM and setM for every instance X of the class Y, provided that these methods are explicitly defined for Y. Thus, nonmonotonic inheritance has no effect on funM and setM, since it is overwritten by these explicit definitions.

One should also be aware of the fact that, in case of functional methods, monotonic inheritance is likely to cause inconsistency (lack of canonic models). For instance, if the attribute limbs were inherited monotonicly, then { person[limbs → 4], john[limbs → 5] ] } would have been unsatisfiable, if 4 ≠ 5.

The last issue to be discussed in this section is the mechanism for blocking inheritance of certain “protected” methods. As mentioned in Section 3.1, attributes such as avg salary may be applicable to classes of employees or faculty, but have no meaning for individual persons. Furthermore, even though avg salary makes sense for both empl and faculty, the values of avg salary are unlikely to be the same for these two classes. Hence, for faculty, inheriting avg salary from empl makes little sense. In certain other situations, one may decide to “hide” a method defined for a class from all its subclasses (cf. [Mey88]). Again, blocking inheritance could be a suitable device for this end.

The inheritance-blocking effect can be achieved through a minor modification to the semantics of inheritance given earlier. First, the user must designate certain methods as uninheritable. This can be conveniently done by introducing a new sort of variables and function symbols, say, whose name will begin with a “$”-sign. Then, uninheritable methods are assumed to be precisely those whose outermost symbol’s name starts with a “$”, e.g., empl[$avg sal(1990) ⇒ int].

To block the nonmonotonic inheritance of “$”-marked methods, we only need to exclude the methods whose names begins with a “$”-sign from being considered in the definition of ⊑^{inh}.

The suggested change in the definition of ⊑^{inh} achieves its goal in the sense that the behaviour of “$”- marked methods is no longer inherited, since the new definition does not force such methods occurring in the scope of a subclass to copy their behaviour from a superclass.

It is also easy to expand the inheritance-blocking mechanism to method signatures. To that end, we can introduce a subdomain U^{−} ⊆ U and force I_{F} to interpret function symbols of the form $f via the mappings U^{k} ⟼ U^{−}. The monotonic inheritance of signatures will now be blocked if we remove the anti-monotonicity requirement (of Section 3.3) for I_{⇒}(u) and I_{⇒ ⇒}(u), whenever u ∈ U^{−}.

5 Skolemization and Herbrand’s Theorem

5.1 Skolem Theorem

Skolemization in F-logic is similar to its predicate calculus counterpart, since id-terms are identical to terms in predicate calculus and because quantification is defined similarly in both cases. For instance, a Skolem normal form for the F-term (∀X∃Y)g(X, Y)[Y → f(X, Y); a → → {X, Y }] would be (∀X)g(X, h(X))[h(X) → f(X, h(X)); a → → {X, h(X)}], where h is a new 1-ary function symbol.

Theorem 5.1 (cf. Skolem Theorem) Let φ be an F-formula and φ′ be its Skolemization. Then φ is unsatisfiable if and only if so is φ′.

The proof is almost identical to the standard proof in predicate calculus. From now on we assume that all formulas are Skolemized. Furthermore, it is easy to check that De Morgan’s Laws are valid for F-logic and hence every formula has equivalent formulas in conjunctive and disjunctive normal forms. We can therefore transform every Skolemized formula into a logically equivalent set of clauses, where clause is a disjunction of literals.

5.2 Herbrand Interpretations

As we have seen, F-terms may be embedded in other F-terms to an arbitrary depth. To simplify the proof theory, we will restrict our attention to clauses consisting of flat terms only. This does not limit the generality because any predicate or an F-term can be transformed into an equivalent set of flat terms.

A flat term is either an is-a F-term, a signature F-term of the form P [ ...; F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} ⇒ {..., R_{i,j}, ...}; ...; SetM_{l} @ V_{l,1}, ..., V_{l,k_{l}} ⇒ ⇒ {..., W_{l,h}, ...}; ...], a data F-term of the form P [ ...; F unM_{m} @ Q_{m,1}, ..., Q_{m,k_{m}} → T_{m}; ...; SetM_{l} @ V_{l,1}, ..., V_{l,k_{l}} → → {..., S_{l,h}, ...}; ...], or a P-term p(L_{1}, ..., L_{n}); here all the terms R_{i,j}, V_{l,u}, W_{l,h}, T_{m}, S_{l,h}, and L_{j} inside brackets are id-terms. Clearly, every F- or P-term is equivalent to a conjunction of flat F- and P-terms. For instance, a[X → f(Y)[g(b, Y) → → {c}]] is equivalent to a[X → f(Y)] ∧ f(Y)[g(b, Y) → → {c}].

Restricting attention to flat terms greatly simplifies the definitions and notation and, except for some examples, flat F-terms are assumed till the end of this paper.

Given an F-logic language L with F as its sets of function symbols, the Herbrand universe of L is F^{∗}—the set of all ground id-terms. The Herbrand base, HB, is the set of all ground F-logic molecules (including F-terms, equality, and other P-terms).

Let S be a subset of HB; it is a Herbrand interpretation of L if and only if it is closed under the logical implication, “⊧”, introduced in Section 3.3. Requiring the closedness is convenient here since ground molecules may imply other molecules in a non-trivial way, e.g. {a : b, b : c} ⊧ a : c or {a : b, d[m ⇒ a]} ⊧ d[m ⇒ b]. This is reminiscent of the situation in predicate calculus with equality, where sets of ground atomic formulas may imply other atomic formulas.

Truth in Herbrand interpretations is determined by the following rules:

1. A ground molecule t is true in H if and only if t ∈ H;

2. A ground negative literal ¬t is true in H if and only if t ∉ H;

3. A ground clause L_{1} ∨ ⋯ ∨ L_{n} is true in H if and only if at least one literal L_{i} is true in H;

4. A clause C is true in H if and only if all ground instances of C are true in H. If every clause in S is true in H, then we say that H is a Herbrand model of S.

It is easy to verify that Herbrand interpretations have the following closure properties (needed to establish soundness of inference rules in the next section):

1. Equality terms in H form a congruence relation:

Reflexivity:

• For all p ∈ F^{∗}, p ≐ p ∈ H; Symmetry:

• If p ≐ q ∈ H, then q ≐ p ∈ H; Transitivity:

• If p ≐ q, q ≐ r ∈ H, then p ≐ r ∈ H; Substitution:

• If s ≐ t, L ∈ H and L′ is a result of replacing an occurrence of s in L by t, then L′ ∈ H.

2. Is-a F-terms in H define a partial order:

ISA reflexivity:

• p : p ∈ H; ISA transitivity:

• If p : q, q : r ∈ H then p : r ∈ H; ISA acyclicity:

• If p : q, q : p ∈ H then p ≐ q ∈ H.

3. For signature F-terms:

Type inheritance: • If p [funM @ q_{1}, ..., q_{k} ⇒ {s}], r : p ∈ H then r [funM @ q_{1}, ..., q_{k} ⇒ {s}] ∈ H;

• If p [setM @ q_{1}, ..., q_{k} ⇒ ⇒ {s}], r : p ∈ H then r [setM @ q_{1}, ..., q_{k} ⇒ ⇒ {s}] ∈ H.

Supertyping-1:

• If p [funM @ q_{1}, ..., q_{i}, ..., q_{k} ⇒ {s}], q′_{i} : q_{i} ∈ H then p [setM @ q_{1}, ..., q′_{i}, ..., q_{k} ⇒ {s}] ∈ H;

• If p [setM @ q_{1}, ..., q_{i}, ..., q_{k} ⇒ ⇒ {s}], q′_{i} : q_{i} ∈ H then p [funM @ q_{1}, ..., q′_{i}, ..., q_{k} ⇒ ⇒ {s}] ∈ H. Supertyping-2:

• If p [funM @ q_{1}, ..., q_{k} ⇒ {r}], r : s ∈ H, then p [funM @ q_{1}, ..., q_{k} ⇒ {s}] ∈ H;

• If p [setM @ q_{1}, ..., q_{k} ⇒ ⇒ {r}], r : s ∈ H, then p [setM @ q_{1}, ..., q_{k} ⇒ ⇒ {s}] ∈ H. Well-typing:

• If p [funM @ q_{1}, ..., q_{k} → q], p [funM @ q_{1}, ..., q_{k} ⇒ {r}] ∈ H then q : r ∈ H;

• If p [setM @ q_{1}, ..., q_{k} → → {q}], p [setM @ q_{1}, ..., q_{k} ⇒ ⇒ {r}] ∈ H then q : r ∈ H;

• If p [funM @ q_{1}, ..., q_{k} → q] then p [funM @ q_{1}, ..., q_{k} ⇒ { }] ∈ H;

• If p [setM @ q_{1}, ..., q_{k} → → {q}] then p [setM @ q_{1}, ..., q_{k} ⇒ ⇒ { }] ∈ H.

4. For data F-terms:

Functionality:

• If p[funM @ q_{1}, ..., q_{k} → r_{1}], p[funM @ q_{1}, ..., q_{k} → r_{2}] ∈ H, then r_{1} ≐ r_{2} ∈ H.

5. For every id-term t:

• t[ ] ∈ H.

6. For every term t:

• t ∈ H if and only if every atom constituting t is in H.

The atoms mentioned in the last property are essentially flat molecules broken into indivisible pieces; they are formally defined as follows:

1. Every flat P-term or an is-a F-term is its own atom;

2. For a flat signature F-term

P [...; F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} ⇒ {R_{i,1}, ..., R_{i,n_{i}}}; ...; SetM_{j} @ S_{j,1}, ..., S_{j,k_{j}} ⇒ ⇒ {T_{j,1}, ..., T_{j,m_{j}}}; …] its atoms are the following F-terms (for every method F unM_{i} or SetM_{j}):

\begin{matrix}P [F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} ⇒ \{ \}] & P [SetM_{j} @ S_{j,1}, ..., S_{j,k_{j}} ⇒ ⇒ \{ \}] \\ P [F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} ⇒ \{R_{i,1}\}] & P [SetM_{j} @ S_{j,1}, ..., S_{j,k_{j}} ⇒ ⇒ \{T_{j,1}\}] \\ . . . . . . . . . & . . . . . . . . . \\ P [F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} ⇒ \{R_{i,n_{i}}\}] & P [SetM_{j} @ S_{j,1}, ..., S_{j,k_{j}} ⇒ ⇒ \{T_{j,m_{j}}\}]. \end{matrix}

3. For a flat data F-term

P [...; F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} → R_{i}; ...; SetM_{j} @ S_{j,1}, ..., S_{j,l_{j}} → → {T_{j,1}, ..., T_{j,n_{j}}}; ...], its atoms are (for every method F unM_{i} or SetM_{j}):

P [F unM_{i} @ Q_{i,1}, ..., Q_{i,k_{i}} → R_{i}]

P [SetM_{j} @ S_{j,1}, ..., S_{j,l_{j}} → { }]
P [SetM_{j} @ S_{j,1}, ..., S_{j,l_{j}} → {T_{j,1}}]
. . . . . . . . .
P [SetM_{j} @ S_{j,1}, ..., S_{j,l_{j}} → {T_{j,n_{j}}}].

5.3 Correspondence between Herbrand Interpretations and Semantic Structures

There is a natural correspondence between Herbrand interpretations and semantic structures of Section 3.3: Given a semantic structure for a set of clauses S, the corresponding Herbrand interpretation is the set of ground F-logic molecules that are true in the structure. Conversely, for a Herbrand interpretation H, the corresponding semantic structure, I_{H} = ⟨U, ≺_{U}, I_{F}, I_{℘}, I_{→}, I_{→ →}, I_{⇒}, I_{⇒ ⇒}⟩, is defined as follows:^{15}

1. The domain U is F^{∗}/ ≐, the quotient of F^{∗} induced by the equality terms in H. We denote the equivalence class of t by [t].

2. The ordering of U is defined with the help of is-a F-terms in H:

For all [t], [s] ∈ U, [s]⪯_{U}[t] if and only if s : t ∈ H.

3. I_{F}(c) = [c], for every 0-ary function symbol c ∈ F.

4. I_{F}(f)([t_{1}], ..., [t_{k}]) = [f(t_{1}, ..., t_{k})], for every k-ary (k ≥ 1) function symbol f ∈ F.

5. I(k)_{→}([funM])([obj], [t_{1}], ..., [t_{k}]) = \{ \begin{matrix}[s] & if obj[funM @ t_{1}, ..., t_{k} → s] ∈ H \\ undefined & otherwise. \end{matrix}

6. I(k)_{→ →}([setM])([obj], [t_{1}], ..., [t_{k}]) =

\{ \begin{matrix}\{[s] | where obj[setM @ t_{1}, ..., t_{k} → → \{s\}] ∈ H\} & if obj[setM @ t_{1}, ..., t_{k} → → \{ \}] ∈ H \\ undefined & otherwise. \end{matrix}

7. I(k)_{⇒}([funM])([obj], [t_{1}], ..., [t_{k}]) =

\{ \begin{matrix}\{[s] | where obj[funM @ t_{1}, ..., t_{k} ⇒ \{s\}] ∈ H\} & if obj[funM @ t_{1}, ..., t_{k} ⇒ \{ \}] ∈ H \\ undefined & otherwise. \end{matrix}

8. I(k)_{⇒ ⇒}([setM])([obj], [t_{1}], ..., [t_{k}]) =

\{ \begin{matrix}\{[s] | where obj[setM @ t_{1}, ..., t_{k} ⇒ ⇒ \{s\}] ∈ H\} & if obj[setM @ t_{1}, ..., t_{k} ⇒ ⇒ \{ \}] ∈ H \\ undefined & otherwise. \end{matrix}

9. I_{℘}(p) = {⟨[t_{1}], ..., [t_{k}]⟩ | p(t_{1}, ..., t_{k}) ∈ H}.

We remark that in (6), (7) and (8) above, there is a difference between I(k)_{→ →}([setM])([obj], [t_{1}], ..., [t_{k}]) (or I(k)_{⇒}([funM])([obj], [t_{1}], ..., [t_{k}]), I(k)_{⇒ ⇒}([setM])([obj], [t_{1}], ..., [t_{k}]) ) being undefined and being empty. It is undefined if in (6) (resp., (7), (8) ), H contains no atom of the form obj[setM @ t_{1}, ..., t_{k} → → …]; not even obj[setM @ t_{1}, ..., t_{k} → → { }]. In contrast, I(k)_{→ →}([setM])([obj], [t_{1}], ..., [t_{k}]) is empty when H does contain obj[setM @ t_{1}, ..., t_{k} → → { }], but has no atom of the form obj[setM @ t_{1}, ..., t_{k} → → {s}], for some s ∈ F^{∗}.

It is easy to see that I_{H} = ⟨U, ≺_{U}, I_{F}, I_{℘}, I_{→}, I_{→ →}, I_{⇒}, I_{⇒ ⇒}⟩ thus defined is, indeed, a semantic structure. The above correspondence immediately leads to the following result:

15Observe the similarity with the corresponding construction in predicate calculus with equality.

Proposition 5.1 Let S be a set of clauses. Then S is unsatisfiable if and only if S has no Herbrand model.

Proof: It is easy to verify that for any Herbrand interpretation H, H ⊧ S if and only if I_{H} ⊧ S, where I_{H} is the semantic structure corresponding to H, defined earlier. □

5.4 Herbrand’s Theorem

In classic logic, a set S of clauses is unsatisfiable if and only if so is some finite set of ground instances of clauses in S; this property is usually referred to as Herbrand’s theorem. In F-logic, Herbrand’s theorem also holds and plays the same fundamental role. We establish this theorem by considering maximal finitely satisfiable sets, similarly to the proof of the compactness theorem in [End72]. A set S of ground clauses is finitely satisfiable, if every finite subset of S is satisfiable. A finitely satisfiable set S is maximal, if no other set of ground clauses containing S is finitely satisfiable. Some useful properties of finitely satisfiable sets are stated below.

Lemma 5.1 Given a finitely satisfiable set S of ground clauses, there exists a maximal finitely satisfiable set T, such that S ⊆ T.

Proof: Let Λ be a collection of all finitely satisfiable sets of ground clauses that contain S; Λ is partially ordered by set-inclusion. Since S ∈ Λ, Λ is non-empty. Furthermore, for every chain Σ ⊆ Λ, the least upper bound of the chain, ∪Σ, is also in Λ, because:

• ∪Σ contains S; and

• ∪Σ is finitely satisfiable (for, if not, neither is one of the elements of Σ).

By Zorn’s Lemma, there is a maximal element T in Λ. Clearly, it is maximal, finitely satisfiable, and contains S. □

Lemma 5.2 Let T be a maximal finitely satisfiable set of ground clauses.

1. For every ground F-logic molecule T, either T ∈ T or ¬T ∈ T.

2. A ground clause L_{1} ∨ ⋯ ∨ L_{n} ∈ T if and only if some L_{i} ∈ T, 1 ≤ i ≤ n.

Proof: (1) If T is finitely satisfiable, then either T ∪ {T } or T ∪ {¬T } is finitely satisfiable. Therefore, T must contain either T or ¬T, since it is maximal.

(2) Similarly to (1). □

Lemma 5.3 Let T be a maximal finitely satisfiable set of ground clauses. Let H be the set of all ground molecules in T. Then H is a Herbrand interpretation.

Proof: It is easy to see that H is closed under “⊧”, since T is also closed under “⊧” (or else T is not maximal). □

Theorem 5.2 (cf. Herbrand’s Theorem) A set of clauses S is unsatisfiable if and only if so is some finite subset of ground instances of clauses in S.

Proof: The “if” part is easy: When some finite subset of ground clauses of S is unsatisfiable, then S is unsatisfiable, too. The “only-if” part is proved by contradiction. Assume the set S′ of ground instances of clauses in S is finitely satisfiable. We will show that then S is satisfiable.

Since S′ is assumed to be finitely satisfiable, by Lemma 5.1 it can be extended to some maximal finitely satisfiable set T. Let H be the set of all ground molecules in T, which is a Herbrand interpretation, by Lemma 5.3. We claim that for every ground clause C, H ⊧ C if and only if C ∈ T. Consider the following cases:

(i) C is a ground molecule: By definition, H ⊧ C if and only if C ∈ T;

(ii) C is a negative literal ¬P: Then H ⊧ ¬P if and only if P ∉ H. Since H contains all the ground molecules in T, P ∉ H if and only if P ∉ T. Finally, by (1) of Lemma 5.2, P ∉ T if and only if ¬P ∈ T;

(iii) C is a disjunction of ground literals L_{1} ∨ ⋯ ∨ L_{n}: H ⊧ L_{1} ∨ ⋯ ∨ L_{n} if and only if H ⊧ L_{i} for some i, by definition, if and only if L_{i} ∈ T, by the result of the cases (i) and (ii), if and only if L_{1} ∨ ⋯ ∨ L_{n} ∈ T, by (2) of Lemma 5.2.

We have shown that H satisfies every clause of T. Since S′ ⊆ T, H is a Herbrand model of S. By Proposition 5.1, S is satisfiable. □

Herbrand’s Theorem is a basis for the resolution-based proof procedure in predicate calculus [CL73]. In the next section we present a sound and complete resolution-based proof procedure, extending the result of [KW89]. This, in turn, provides a firm basis for the theory of F-logic programming and databases.

As an easy exercise, the reader can try to define an analogue of the T_{P} operator of [Llo87] for the case when P is a set of F-logic Horn clauses, and prove that the least fixed point of T_{P} coincides with the least Herbrand model of P.

6 Proof Theory

This section describes a sound and complete proof theory for the monotonic entailment relation “⊧” of Section 3.3. The theory consists of twelve inference rules and one axiom. The resolution, factoring, and paramodulation rules form the core of the deductive system. However, unlike in predicate calculus, they do not suffice. For a deductive system to be complete, we need auxiliary rules that capture properties of the subclass relationship, types, and other additions to classic logic. The large number of inference rules in F-logic compared to predicate calculus stems from the rich semantics of object-oriented systems and is likely to be the case with any logical system that makes an attempt to adequately capture this paradigm. As will be seen shortly, many rules are quite similar to each other, except that, say, one may deal with data F-terms while another with signature F-terms or with P-terms. It is possible to reduce the number of rules by about half through increasing the power of the resolution rule. For instance, to reduce the size of the deductive system for predicate calculus, factoring is often combined with resolution. However, we prefer to keep inference rules simple while multiplying their number so that it would be easier to see the rationale behind each rule.

6.1 Unifiers

First, we extend the notions of the unifier and most general unifier to F-terms. Unification of id-terms, is-a F-terms, and P-terms is defined the same way as in predicate calculus: Let T_{1} and T_{2} be a pair of such terms. A substitution σ is a unifier of T_{1} and T_{2}, if and only if σ(T_{1}) = σ(T_{2}). This unifier is most general, written mgu(T_{1}, T_{2}), if for every unifier μ of T_{1} and T_{2}, there exists a substitution γ, such that μ = γ ∘ σ.

For data and signature F-terms, rather than requiring the terms to be identical, we merely want one term to be a subterm of the other. Let T_{1} = S[…] and T_{2} = S[…] be a pair of data or signature F-terms with the same object id. We say that T_{1} is a subterm of T_{2}, denoted T_{1} ⊑ T_{2}, if and only if every atom of T_{1} is also an atom of T_{2}. A substitution σ is a unifier of T_{1} into T_{2} (note the asymmetry!) if and only if σ(T_{1}) ⊑ σ(T_{2}).

Defining mgu’s for this kind of F-terms requires more work. Consider the terms T_{1} = a[set → → {X}] and T_{2} = a[set → → {b, c}]. Intuitively, there are two unifiers of T_{1} into T_{2} that can be called “most general”: X\b and X\c. Clearly, none of these unifiers is more general than the other, and therefore the definition of mgu that works for P-terms and is-a F-terms is inappropriate here.

A suitable notion can be defined as follows: Let T_{1} and T_{2} be a pair of signature or data F-terms and let α, β be a pair of unifiers of T_{1} into T_{2}. We say that α is more general than β, denoted α ≤ β, if and only if there is a substitution γ such that β = γ ∘ α. A unifier α of T_{1} into T_{2} is most general if for every unifier β, β ≤ α implies α ≤ β.

A set Σ of most general unifiers of T_{1} into T_{2} is complete if for every unifier θ of T_{1} into T_{2}, there is an α ∈ Σ such that α ≤ θ. Just as there is a unique-up-to-the-equivalence mgu in the classic case, it easily follows from the definitions that the complete set of unifiers of T_{1} into T_{2} is also unique up to the equivalence.^{16} An algorithm that computes a complete set of mgu’s appears in Appendix D.

In predicate calculus, the notion of unifier works for an arbitrary number of terms that are to be unified. Extension of our definitions to accommodate an arbitrary number of id-terms, P-terms, or is-a F-terms is obvious. For data and signature F-terms, we say that a substitution σ is a unifier of T_{1}, ..., T_{n} into S if and only if σ(T_{i}) ⊑ S, for i = 1, ..., n. Generalization of the notion of mgu is straightforward and is left to the reader.

16A set of unifiers Ω_{1} is equivalent to Ω_{2} if for every σ_{1} ∈ Ω_{1} there is σ_{2} ∈ Ω_{2} such that σ_{1} ≤ σ_{2} ≤ σ_{1}, and vice versa.

For notational convenience, we also define mgu’s for tuples of id-terms: Tuples ⟨P_{1}, ..., P_{n}⟩ and ⟨Q_{1}, ..., Q_{n}⟩ are unifiable if and only if there is a substitution σ such that σ(P_{i}) = σ(Q_{i}), i = 1, ..., n. This unifier is most general (written mgu(⟨P_{1}, ..., P_{n}⟩, ⟨Q_{1}, ..., Q_{n}⟩) ), if and only if for every other unifier μ of these tuples, μ = γ ∘ σ for some substitution γ. It is easy to see that mgu of ⟨P_{1}, ..., P_{n}⟩ and ⟨Q_{1}, ..., Q_{n}⟩ coincides with the mgu of f(P_{1}, ..., P_{n}) and f(Q_{1}, ..., Q_{n}), where f is an arbitrary n-ary function symbol.

In the sequel, mgu_{⊑}(T_{1}, T_{2}) will be used to denote some most general unifier of T_{1} into T_{2}. Note that mgu_{⊑}(T_{1}, T_{2}) may exist while mgu_{⊑}(T_{2}, T_{1}) may not. Furthermore, since unification of id-, is-a and P-terms is symmetric, we can still talk about unification of one such term into another, even though the order of terms in this case is immaterial. We adopt this convention, as it obviates the need in repeating certain definitions. Also, in the derivation rules that follow, we use only atoms (not molecules), which is done mostly by type-setting reasons. It should be clear how these rules would look in general.

Finally, we remark that, as in predicate calculus, prior to any application of an inference rule, the clauses involved in the operation must be standardized apart. This means that variables must be renamed so that these clauses will share none. However, clauses used in an inference rule may be instances of the same clause; they can even be identical, if no variables are involved.

6.2 Core Inference Rules

For simplicity, and without loss of generality, only binary resolution is considered.

Resolution: Let C =^{def} ¬T ∨ \overline{C} and C′ =^{def} T′ ∨ \overline{C}′ be a pair of clauses that are standardized apart. Let θ be an mgu of T into T′. Then the resolution rule is as follows:

from C and C′ infer θ(\overline{C} ∨ \overline{C}′).

Notice that when the literals involved in the operation are data or signature F-terms, resolution is asymmetric since θ = mgu_{⊑}(T, T′) may be different from mgu_{⊑}(T′, T), and the latter mgu may not even exist. As in the classic case, binary resolution must be complemented with the so-called factoring rule that seeks to reduce the number of disjuncts in a clause.

Factoring: Consider a clause C =^{def} T ∨ T′ ∨ \overline{C}, where T and T′ are positive literals. Let T be unifiable into T′ with the mgu θ. Then by the factoring rule:

from C infer θ(T ∨ \overline{C}).

In case of negative literals, if C =^{def} ¬T ∨ ¬T′ ∨ \overline{C} and T is unifiable into T′ with the mgu θ, the factoring

rule prescribes the following:

from C derive θ(¬T′ ∨ \overline{C}).

Resolution:  \frac{¬T ∨ C, T′ ∨ C′, θ = mgu_{⊑}(T, T′)}{θ(C ∨ C′)}

Factoring:  \begin{matrix}T ∨ T′ ∨ C, θ = mgu_{⊑}(T, T′) & ¬T ∨ ¬T′ ∨ C, θ = mgu_{⊑}(T, T′) \\ θ(T ∨ C) & θ(¬T′ ∨ C) \end{matrix}

Paramodulation: \frac{L[T] ∨ C, (T′ ≐ T′′) ∨ C′, θ = mgu(T, T′)}{θ(L[T′′] ∨ C ∨ C′)}

Figure 5: Summary of Core Inference Rules

Clauses inferred by one of the two factoring rules are called factors of C.

To account for the equality relation that may arise among id-terms, we need the paramodulation rule. We use the following standard convention: If an expression E (a clause, a literal, or a term) contains an id-term T, we shall sometimes emphasize this fact by writing E[T]. If one single occurrence of T is replaced by S, the result will be denoted by E[S].

Paramodulation: Consider a pair of clauses, C =^{def} L[T] ∨ \overline{C} and C′ =^{def} (T′ ≐ \overline{T}′) ∨ \overline{C}′, with no common variables. If T and T′ are id-terms with an mgu θ then, by the paramodulation rule:

from C and C′ derive θ(L[\overline{T}′] ∨ \overline{C} ∨ \overline{C}′).

6.3 ISA Inference Rules

The following axiom and rules capture the reflexivity, acyclicity and the transitivity of the subclass relationship.

ISA Reflexivity: The following is the ISA-reflexivity axiom:

(∀X) X : X.

ISA Acyclicity: Let C =^{def} P : Q∨\overline{C} and C′ =^{def} Q′ : P′ ∨\overline{C}′ be clauses with no variables in common. Suppose that θ is an mgu of tuples ⟨P, Q⟩ and ⟨P′, Q′⟩ of id-terms. Then by the acyclicity rule:

from C and C′ derive θ(P ≐ Q ∨ \overline{C} ∨ \overline{C}′).

Note that ISA-reflexivity and acyclicity imply reflexivity of equality: X : X is an axiom and X : X and X : X imply X ≐ X, by ISA-acyclicity.

ISA Transitivity: Let C =^{def} P : Q ∨ \overline{C} and C′ =^{def} Q′ : R′ ∨ \overline{C}′ be standardized apart and θ be an mgu of Q and Q′. The transitivity rule then is:

from C and C′ derive θ(P : R′ ∨ \overline{C} ∨ \overline{C}′).

ISA Reflexivity:  X : X
ISA Acyclicity:  \frac{P : Q ∨ C, Q′ : P′ ∨ C′, θ = mgu(⟨P, Q⟩, ⟨P′, Q′⟩)}{θ( (P ≐ Q) ∨ C ∨ C′)}

ISA Transitivity:  \frac{P : Q ∨ C, Q′ : R′ ∨ C′, θ = mgu(Q, Q′)}{θ(P : R′ ∨ C ∨ C′)}

Figure 6: Summary of ISA Inference Rules

6.4 Type Inference Rules

Signature F-terms have the properties of well-typing, type inheritance, and supertyping that are captured by the following inference rules:

Well-Typing: Let C =^{def} P [F unM @ Q_{1}, ..., Q_{k} → R] ∨ \overline{C} and C′ =^{def} P′[F unM′ @Q′_{1}, ..., Q′_{k} ⇒

\{R′\}] ∨ \overline{C}′ be a pair of clauses with no common variables, such that the tuples ⟨P, F unM, Q_{1}, ..., Q_{k}⟩ and ⟨P′, F unM′, Q′_{1}, ..., Q′_{k}⟩ unify with an mgu θ. The well-typing derivation rule then says the following:

from C and C′ derive θ( R : R′ ∨ \overline{C} ∨ \overline{C}′))

and

from C derive P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{ \}] ∨ \overline{C}.

These rules reflect the well-typing requirements to semantic structures (see Section 3.3): The first says that the output of F unM must obey the restrictions imposed by signature terms; the second rule captures the idea that a method is defined on a set of arguments only if the typing of that method is also defined on these arguments.

A similar rule exists for set-valued methods, except that the clauses C and C′ above must be replaced by P [SetM @ Q_{1}, ..., Q_{k} → → \{R\}] ∨ \overline{C} and P′[SetM′ @ Q′_{1}, ..., Q′_{k} ⇒ ⇒ \{R′\}] ∨ \overline{C}′, respectively.

Type Inheritance: Let C =^{def} P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{T \}] ∨ \overline{C} and C′ =^{def} S′ : P′ ∨ \overline{C}′ be a pair of clauses with no common variables such that P and P′ have an mgu θ. The type inheritance rule states the following:

from C and C′ derive θ(S′[F unM @ Q_{1}, ..., Q_{k} ⇒ \{T \}] ∨ \overline{C} ∨ \overline{C}′).

In other terms, S′ inherits the signature of P′. A similar rule exists for set-valued methods. If

C =^{def} P [SetM @ Q_{1}, ..., Q_{k} ⇒ ⇒ \{T \}] ∨ \overline{C} and C′ is as before then:

from C and C′ derive θ(S′[SetM @ Q_{1}, ..., Q_{k} ⇒ ⇒ \{T \}] ∨ \overline{C} ∨ \overline{C}′).

Well-Typing:  P [F unM @ Q_{1}, ..., Q_{k} → R] ∨ C, P′[F unM′ @ Q′_{1}, ..., Q′_{k} ⇒ {R′}] ∨ C′

θ = mgu( ⟨P, F unM, Q_{1}, ..., Q_{k}⟩, ⟨P′, F unM′, Q′_{1}, ..., Q′_{k}⟩) θ( R : R′ ∨ C ∨ C′)

P [F unM @ Q_{1}, ..., Q_{k} → R] ∨ C P [F unM @ Q_{1}, ..., Q_{k} ⇒ { }] ∨ C

similarly for set-valued methods: simply replace ⇒ / → by ⇒ ⇒ / → →

Type Inheritance: \frac{P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{T \}] ∨ C, S′ : P′ ∨ C′, θ = mgu(P, P′)}{θ(S′[F unM @ Q_{1}, ..., Q_{k} ⇒ \{T \}] ∨ C ∨ C′)}

similarly for set-valued methods

Supertyping-1:  \frac{P [F unM @ Q_{1}, ..., Q_{i}, ..., Q_{k} ⇒ \{T \}] ∨ C, Q′′_{i} : Q′_{i} ∨ C′, θ = mgu(Q_{i}, Q′_{i})}{θ(P [F unM @ Q_{1}, ..., Q′′_{i}, ..., Q_{k} ⇒ \{T \}] ∨ C ∨ C′)}

similarly for set-valued methods

Supertyping-2:  \frac{P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{R\}] ∨ C, R′ : R′′ ∨ C′, θ = mgu(R, R′)}{θ(P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{R′′\}] ∨ C ∨ C′)}

similarly for set-valued methods

Figure 7: Summary of Type Inference Rules

Supertyping-1: Let C =^{def} P [F unM @ Q_{1}, ..., Q_{i}, ..., Q_{k} ⇒ \{T \}] ∨ \overline{C} and C′ =^{def} \overline{Q}′_{i} : Q′_{i} ∨ \overline{C}′ be

standardized apart. Suppose also that Q_{i} and Q′_{i} have an mgu θ. Then we can apply the first supertyping rule:

from C and C′ derive θ(P [F unM @ Q_{1}, ..., \overline{Q}′_{i}, ..., Q_{k} ⇒ \{T \}] ∨ \overline{C} ∨ \overline{C}′),

where \overline{Q}′_{i} replaces Q_{i}. A similar rule exists for set-valued methods.

Supertyping-2: Consider a pair of clauses, C =^{def} P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{R\}] ∨ \overline{C} and C′ =^{def} R′ : \overline{R}′ ∨ \overline{C}′, with no common variables, and suppose R and R′ have an mgu θ. The second supertyping rule is:

from C and C′ derive θ(P [F unM @ Q_{1}, ..., Q_{k} ⇒ \{\overline{R}′\}] ∨ \overline{C} ∨ \overline{C}′).

Similar rules apply to set-valued methods.

6.5 Miscellaneous Inference Rules

Functionality of single-valued methods is enforced by the following rule:

Functionality: Consider a pair of clauses that share no common variables:

C =^{def} P [F unM @ Q_{1}, ..., Q_{k} → R] ∨ \overline{C} and C′ =^{def} P′[F unM′ @ Q′_{1}, ..., Q′_{k} → R′] ∨ \overline{C}′.

Suppose there is an mgu θ that unifies the tuple of id-terms ⟨P, F unM, Q_{1}, ..., Q_{k}⟩ with the tuple ⟨P′, F unM′, Q′_{1}, ..., Q′_{k}⟩. Then we can apply the functionality rule:

from C and C′ infer θ( R ≐ R′ ∨ \overline{C} ∨ \overline{C}′).

Next, we introduce the merging rule that seeks to combine information contained in different data or signature F-terms. Let T_{1} and T_{2} be a pair of data F-terms with the same object id. A data F-term T is called a merge of T_{1} and T_{2}, if the set of atoms of T is precisely the union of the sets of atoms of T_{1} and T_{2}. A pair of data or signature F-terms can be merged in several different ways when they have common set-valued methods. For example, the terms

T [F unM → d; SetM → → {e}; SetM @ X → → {b}]  (9)
T [F unM → g; SetM @ Y → → {h}; SetM @ X → → {c}]  (10)

have more than one merge:

\begin{aligned}T [F unM → d; F unM → g; SetM → → \{e\}; & SetM @ Y → → \{h\}; \\ & SetM @ X → → \{b\}; SetM @ X → → \{c\}] \end{aligned}  (11)

and

T [F unM → d; F unM → g; SetM → → {e}; SetM @ Y → → {h}; SetM @ X → → {b, c}].  (12)

However, we distinguish certain kind of merges, which we call canonical, that do possess the uniqueness property.

An invocation of a method consists of the method’s name, its arguments, and the arrow specifying the type of invocation (functional or set-valued). For instance, in the above example, F unM →, SetM → →, SetM @ X → →, and SetM @ Y → → are all distinct invocations. A canonical merge of T_{1} and T_{2}, denoted merge(T_{1}, T_{2}), is a merge that does not contain repeated identical invocations of set-valued methods. In the above, (12) is a canonical merge of (9) and (10). Canonical merging of signature F-terms is defined similarly. Clearly, merge(T_{1}, T_{2}) is unique up to a permutation of atoms and id-terms in ranges of set-valued methods.

Merging: Consider a pair of standardized apart clauses, C =^{def} T ∨ \overline{C} and C′ =^{def} T′ ∨ \overline{C}′, where both T and T′ are data or signature F-terms such that there is an mgu θ unifying the id parts of T and T′. Let R denote the canonical merge of θ(T) and θ(T′). The merging rule sanctions the following derivation:

from C and C′ derive R ∨ θ(\overline{C} ∨ \overline{C}′).

Functionality: P [F unM @ Q_{1}, ..., Q_{k} → R] ∨ C_{1}, P′[F unM′ @ Q′_{1}, ..., Q′_{k} → R′] ∨ C_{2}

θ = mgu( ⟨P, F unM, Q_{1}, ..., Q_{k}⟩, ⟨P′, F unM′, Q′_{1}, ..., Q′_{k}⟩)

θ( R ≐ R′ ∨ C_{1} ∨ C_{2})
Merging:  \frac{P [...] ∨ C, P′[...] ∨ C′, θ = mgu(P, P′), R = merge(θ(P [...]), θ(P′[...]))}{R ∨ θ(C ∨ C′)}

Elimination:  \frac{¬T [ ] ∨ C}{C}

Figure 8: Summary of Miscellaneous Inference Rules

Finally, since for every id-term T, the F-term T [ ] is a tautology, we need the following elimination rule:

Elimination: If C is a clause and T an id-term then:

from ¬T [ ] ∨ C derive C.

Notice that in the elimination rule, if C is empty then we derive an empty clause □ from ¬T [ ].

6.6 Comments on the Inference Rules

With such a multitude of F-logic inference rules, a natural concern is whether there might be an efficient evaluation procedure for F-logic queries. The answer to this question is positive: F-logic queries can be evaluated, say, bottom-up and the optimization strategies developed for deductive databases (e.g., Magic Sets and Templates [BR87, Ram88]) are applicable here as well.

Another important point is that there is no need in using some of the inference rules at run time. For instance, in proof-theoretic terms, the purpose of static type checking is precisely this: elimination of the need in run-time application of the typing rules. Likewise, a compile-time acyclicity-checking algorithm could be used to get rid of the ISA-acyclicity rule at run time. A practical system also is likely to weaken the functionality inference rule and use it only to highlight possible inconsistency detected in functional methods. These topics will be addressed in a companion paper.

6.7 Soundness of the Proof Theory

Given a set S of clauses, a deduction of a clause C from S is a finite sequence of clauses D_{1}, ..., D_{n} such that D_{n} = C and for 1 ≤ k ≤ n each D_{k} is either

• a member of S, or

• is derived from D_{i} alone or from D_{i} and D_{j} (whichever is applicable), where i, j < k, using one of the core, is-a, type, or miscellaneous inference rules.

A deduction ending with the empty clause □ is called a refutation of S. If C is deducible from S, we write S ⊢ C.

Theorem 6.1 (Soundness of F-logic deduction) If S ⊢ C then S ⊧ C.

Proof: Directly follows from the closure properties given in Section 5.2 and from the form of the inference rules. □

6.8 Completeness of the Proof Theory

We follow the standard strategy for proving completeness, adapted from predicate calculus: First, using Herbrand’s theorem, we establish completeness for the ground case. Then, with the help of a result analogous to Lifting Lemma, we show that ground refutations can be “lifted” to the nonground case.

Lemma 6.1 Let S be a set of ground F-logic literals. If S is unsatisfiable then there are molecules P and Q such that P ⊑ Q, ¬P ∈ S and S ⊢ Q. (When P, Q are P-terms or is-a F-terms, P ⊑ Q is defined to mean that P is identical to Q.)

Proof: Suppose to the contrary, that there are no molecules P and Q, such that P ⊑ Q, ¬P ∈ S, and S ⊢ Q. We will show that then S is satisfiable. Consider a set of molecules,

D(S) =^{def} {P | P is a subterm of some molecule deducible (via ⊢) from S }.

In Section 5.3 we showed that for any Herbrand interpretation H there is a corresponding semantic structure I_{H} such that H ⊧ S if and only if I_{H} ⊧ S. Applying the same construction to D(S) we obtain a semantic structure M. Since D(S) is closed under deduction, it is easy to verify that M is indeed a semantic structure. We claim that for every molecule P,

M ⊧ P if and only if P ∈ D(S)  (13)

The “if”-direction follows from soundness of the derivation rules. For the “only if”-direction, consider the following two cases:

1. P is a predicate or an is-a F-term:

Depending on whether P is an is-a or a predicate term, items (2) or (9) in the construction of M in Section 5.3 can be used to show that M ⊧ P if and only if P ∈ D(S).

2. P is a signature or a data F-term composed of atoms τ_{1}, ..., τ_{n}: Then M ⊧ P if and only if M ⊧ τ_{i}, i = 1, ..., n. By items (5), (6), (7), or (8) (of Section 5.3) – depending on whether the method invocation in τ_{i} is functional or set-valued and whether P is a data or a signature F-term – it follows that M ⊧ τ_{i} if and only if τ_{i} ∈ D(S). Therefore, by the definition of D(S), there are terms Q_{1}, ..., Q_{n} deducible from S, such that τ_{i} is a subterm of Q_{i}, for i = 1, ..., n. Let Q be the canonical merge of Q_{1}, ..., Q_{n}. Then P is a subterm of Q (since every atom of P is a subterm of Q) and Q is deducible from S (since Q_{1}, ..., Q_{n} are deducible from S and Q is obtained from Q_{1}, ..., Q_{n} by the merging rule). Hence, P is in D(S), which proves (13).

By the definition of D(S), if P ∈ S is a positive literal then P ∈ D(S). Hence, by (13), M ⊧ P. For every negative literal ¬P in S, P is not a subterm of any molecule deducible from S, by the assumption made at the beginning of the proof. So, P is not in D(S). Again, by (13), M |̸= P and therefore M ⊧ ¬P. Thus, M satisfies every literal of S, that is, it is a model for S. □

Theorem 6.2 (Completeness of ground deduction) If a set of ground clauses S is unsatisfiable then there exists a refutation of S.

Proof: By Herbrand’s Theorem, we may assume that S is finite. Suppose S is unsatisfiable. We will show that there is a refutation of S, using a technique due to Anderson and Bledsoe [AB70]. The proof is carried out by induction on the parameter excess(S), the number of “excess literals” in S:

excess(S) =^{def} ( the number of occurrences of literals in S) − (the number of clauses in S).

Basis: excess(S) = 0. In this case, the number of clauses in S equals the number of literals in S. Hence either □ ∈ S and we are done, or every clause in S is a literal. In the latter case, by Lemma 6.1, S ⊢ ¬P and S ⊢ Q for some molecules P, Q such that P ⊑ Q. Applying the resolution rule to ¬P and Q, we obtain the empty clause.

Induction Step: excess(S) = n > 0. In this case, there must be a clause C in S that contains more than one literal. Let us separate this clause from the other clauses and write S = {C} ∪ S′, where C = L ∨ C′ (C′ ≠ □ since we assumed that C contains more than one literal). By the distributivity law, {L ∨ C′} ∪ S′ is unsatisfiable if and only if so are T_{1} = {L} ∪ S′ and T_{2} = {C′} ∪ S′. Since excess(T_{1}) < n and excess(T_{2}) < n and by the induction hypothesis, there are refutations of T_{1} and T_{2}, separately. Therefore, T_{2} ⊢ □. By applying to T the deduction sequence that derives □ from T_{2}, we can derive either L or □. If □ is so produced, then we are done. Otherwise, if L is produced, using the same deduction sequence that derived □ from T_{1}, we can derive □ from S ∪ {L}. Combining the two deductions, we get a deduction that refutes S. □

Proposition 6.1 There exists a unification algorithm that, given a pair of F-terms T_{1} and T_{2}, yields a complete set of mgu’s of T_{1} into T_{2}.

Proof: The algorithm is given in Appendix D, and its correctness is proved in Lemma D.1. □

Lemma 6.2 (Lifting Lemma) Suppose C_{1}, C_{2} are clauses and C′_{1}, C′_{2} are their instances, respectively. If D′ is derived from C′_{1} and C′_{2} (or from C′_{1} alone) using one of the derivation rules, then there exists a clause D, such that D is derived from the factors of C_{1} and C_{2} (resp., from C_{1} alone) using the same inference rule, and D′ is an instance of D.

Proof: Consider each derivation rule separately. The proof in each case is similar to that in predicate calculus since the notion of substitution is the same in both logics. Simple (but tedious) details are left to the reader. □

Theorem 6.3 (Completeness of F-logic deduction) If a set S of clauses is unsatisfiable, then there is a refutation of S.

Proof: The proof is standard: Consider S^{∗}, the set of ground instances of S. By the ground case (Theorem 6.2), there is a refutation of S^{∗}. With the help of Lifting Lemma, this ground refutation can be lifted to a refutation of S. □

7 Other Issues

7.1 Classes and Individual Objects

In ISA-hierarchies, it is often convenient to distinguish between classes and individual objects. For example, in response to the query ? − X : empl one may expect objects such as john or mary, but perhaps not faculty, librarian and the like. However, the latter objects are likely to be found among answers to this query because F-logic does not distinguish between classes and individuals.

How can the system then tell a class from an individual? There are two basic ways to approach this problem: default and specificational. According to the default approach, an object b is an individual with respect to the class hierarchy defined by a set of clauses ISA if and only if for all c, ISA ⊧ c : b implies c ≐ b. The specificational approach requires explicit declaration of individuals.

At first sight it might seem that the default approach is the way to go, since it does not require any extra effort on the programmer’s part. Unfortunately, this way is blocked by two major obstacles: First, the relation {⟨ISA, a⟩ | ∃b : b ≠ a and ISA ⊧ b : a} is recursively enumerable but non-recursive; hence its complement, {⟨ISA, a⟩ | ∀b : if b ≠ a then ISA |̸= b : a}, is not even recursively enumerable. Therefore, there can be no algorithm to determine whether something is an individual object or not.

Second, the default approach is not robust with respect to updates and may cause previously working programs to go astray. For instance, there is no effective way for the system to find out whether for all joe_{public}, ISA |̸= joe_{public} : empl(acme supplies), because empl(acme supplies) is an individual object in a study of companies in a region, or merely due to the fact that acme supplies exists only in the plans and has no employees, at present. So if a program relies on the default notion of an individual, its behaviour may unexpectedly change once acme supplies starts hiring. Even objects such as john or mary describing individual persons cannot be always trusted: It is quite conceivable that these could be later elaborated upon by adding instances, e.g., john-as-a-teacher or john-as-a-scientist.

The specificational approach, suggests that rather than hard-wiring the concept of an individual into the semantics, we could achieve desired results through syntactic restrictions on the language.

For instance, we could separate all variables and function symbols into three categories according to their names: those starting with a “!”-symbol (e.g., !X, !a), those that begin with a “♯” (e.g., ♯Y, ♯f), and those that begin with a letter, as before (e.g., X, h). Id-terms whose outermost symbol is prefixed with a “!” (or “♯”) are supposed to represent individuals (resp., classes); if the outermost symbol begins with a letter then the corresponding id-term can be either an individual or a class, as it has been so far in the paper. Note that here “!” or “♯” is a part of the corresponding function or variable symbol rather than a special syntactic construct.

The next step would be to restrict signature terms. For instance, in signature F-terms such as T [M @ V_{1}, ..., V_{n} ⇒ W], we may want T, V_{1}, ..., V_{n}, W to represent classes and M to be an individual id-term (i.e., this signature would then have the form ♯T [!M @ ♯V_{1}, ..., ♯V_{n} ⇒ ♯W]). Likewise, for isa F-terms, we may require SupCl to be a class in Cl : SupCl (i.e., it should really be Cl : ♯SupCl). These naming conventions can be easily checked by a compiler; they effectively set out a 3-sorted logic on top of the basic F-logic. Alternatively, this is equivalent to introducing a pair of new unary predicates, class(X) and individual(X), where individual (or class) is true precisely of those ground id-terms whose outermost functor has a name prefixed with a “!” (resp., “♯”). In addition, every rule and query, ρ, should be relativized as follows: For every individual variable !X that appears in ρ, add the conjunct individual(!X) in the body. For every variable ranging over classes, e.g., ♯Y, add class(♯Y) in the body.

In practical languages, it may even be useful to distinguish among other kinds of id-terms as well, e.g., to designate terms that denote methods, or even to differentiate between functional and set-valued method names. Furthermore, it may turn out to be instrumental to permit user-defined naming conventions for id-terms. However, these language-engineering issues are beyond the scope of this paper.

In conclusion, we note that although traditional database queries are concerned with retrieving objects only, the fact that F-logic queries can return classes as answers can be profitably utilized for “intelligent” query answering. For instance, since the number of employees may be quite large, the user may not want to see them all, and the “lazy” answer {faculty, librarian, …} may be a more appropriate response to ?−X : empl. Later, if the user indicates an interest in going into the next level of detail, other subclasses and objects can be shown. Likewise, for the example of Figures 2 and 4 (Section 3.1), a more informative response to the query ? − X[degrees → → phd] may be the lazy partial answer {faculty}, rather than the list of everyone holding a Ph.D. degree.

7.2 Objects that “Exist”

Given a set of clauses S that represent a database, it is easy to verify that S ⊧ t for any id-term t. The question therefore arises as to how can one direct the system to retrieve ids of all objects that exist in the database rather then all possible names of objects specifyable in the language. The answer is that we view “existence” as a property of an object, say, expressed through the value of an attribute exists in db. If the value is true, the corresponding object exists; if S |̸= t[exists in db → true] then the object t does not exist.

To make this idea work, we need to augment every clause T [⋯] ← ⋯ in S, where T [⋯] is a data Fterm, by adding the fragment exists in db → true and transforming this clause into T [⋯; exists in db → true] ← ⋯ (this transformation also applies to the facts—the body-less clauses of S). Similarly, queries should be modified to include the aforesaid fragment. Needless to mention that the user does not need to perform this transformation explicitly since this can be taken care of automatically. Then, the answer to the query ? − X would consist of all and only the id’s of objects defined by S.

7.3 Complex Values

It has been argued in several recent papers [Bee89, AK89, LR89] that pure object-based languages may be inconvenient because identity of certain objects is unimportant to programmers. We too made this point in Section 3.5, advocating the use of predicates on a par with objects. However, it may sometimes be convenient to go beyond simple predicates and introduce object-like but identity-less structures, called values in [Bee89, AK89, LR89]. For instance, adapting an example from [LR89] we could write:

eiffel tower[ name → “Eiffel T ower”; admission fee → 25;
address → [city → paris; street → champ de mars] ].

Here [city → paris; street → champ de mars] is a “pure value” representing an address. In O_{2} [LR89], such constructs have no identity and are distinct from objects. The rationale here is that users do not have to shoulder the responsibility of assigning ids to objects that they are not going to access through these ids.

In the spirit of [AK89, LR89], we could define F-logic values as follows:

1. Any id-term is a value;

2. [ …, F unAttr_{i} → V al_{i}, …, SetAttr_{j} → → {…, V al′_{k,j},…},…] is a value, where F unAttr_{i} and SetAttr_{j} are id-terms and V al_{i}, V al′_{k,j} are values;

3. {…, V al_{i}, …}, is a value, provided that the V al_{i}’s are values.

To account for complex values, the definition of data F-terms in Section 3.2 should be changed to allow T_{i}’s and S_{j,v}’s to be values as well as F-terms.

First, note that Cases (1) and (3) in the above definition are “almost” legal in F-logic: Case (1), of course, does not pose any problem, while Case (3) is a generalization of the F-logic set-construct (where previously only sets of id-terms were allowed).

The next question is the semantics of value-terms introduced in this way. The answer depends on the intended usage of these terms. If they are taken too literally, that is, as values assignable to logical variables, then the logic could be in trouble. Indeed, by Case (1), variables are also value-terms and valueterms must be permitted to unify with other value-terms. Therefore, intuitively, the term obj[attr → X] should be unifiable with either of the following:

\begin{matrix}obj[attr → [set → → \{a, b, c\}] ] \\ obj[attr → → \{a, b, c\} ]. \end{matrix}

In each case we would effectively allow variables to range over sets, which will render the semantics second-order [CKW89b, CKW89a] and add to its conceptual and computational complexity.

Fortunately, the experience with object-oriented systems such as Orion [KBC*87] and O_{2} [LR89] suggests that values are used in fairly restrictive ways—primarily as weak entities of the Entity-Relationship Approach. In other words, they are used as “second-rate objects”, accessible only through other objects.

In our view, values are needed not in order to strip identity from certain objects but to give the ability to omit object identities when they are inessential. To some extent, this is similar to Prolog’s don’t-care variables represented by underscores. By analogy, we could permit the use of don’t-care object ids. For instance, re-drawing the Eiffel Tower Example above, we would get

eiffel tower[ name → “Eiffel T ower”; admission fee → 25;
address → [city → paris; street → champ de mars] ].

It remains to decide on the semantics of the don’t-care id-terms. Among the several possible candidates, the one that seems to be most suitable is as follows: Let

T [ ...; F unM @ S_{1}, ..., S_{n} → […]; ...]

be a term with a don’t-care id-term. It’s meaning can be given through the following encoding:

T [ ...; F unM @ S_{1}, ..., S_{n} → val_{n}(T, F unM, S_{1}, ..., S_{n})[…]; ...]

where val_{n} is an (n + 2)-ary new function symbol, specifically chosen for this kind of encoding. It is not accidental that we did not explain how to interpret don’t-care id-terms appearing inside the setconstruct—we have no elegant solution for formulas of the form

T [ ...; SetM @ R_{1}, ..., R_{m} → → {..., […], ...}; ...].

On the other hand, there is no hard evidence that don’t-care ids inside the set-construct have any practical relevance.

The need in don’t-care identities was also emphasized in ILOG [HY90], where a special “∗”-notation was introduced for this purpose. An invention atom p(∗, t_{1}, ..., t_{n}) of ILOG is semantically identical to the F-term

p tuple(t_{1},…, t_{n}) : p[arg_{1} → t_{1}; …; arg_{n} → t_{n}],

where p tuple is a function symbol specificly chosen to represent “invented objects” of class p. Recalling the discussion in Section 3.5 that precedes the introduction of predicate terms, we see that p(∗, t_{1}, ..., t_{n}) of ILOG is semantically the same as the P-term p(t_{1}, ..., t_{n}). In other words, invention atoms of [HY90] are essentially value-based predicate terms of F-logic. However, the reader should not be misled into thinking that ILOG is a value-based language, since it has other means of creating multiple copies of objects, indistinguishable by their values.

The “∗”-style don’t-care id-terms can be useful for modeling value-oriented objects, such as relations with meaningful attribute names. For instance, we could represent the SUPPLIER relation as a class suppl of objects with the signature

suppl[name ⇒ string; parts ⇒ ⇒ part; addr ⇒ string]

and then define the contents of that relation as follows:

∗ : suppl[name → “XY Z Assoc.”; parts → → all-in-one-thing ; addr → “Main St. USA” ]

∗ : suppl[name → “Info Ltd.”; parts → → know-how ; addr → “P.O. Box OO” ].

Here, the symbol “∗” is used as a shorthand notation that relieves programmers from the tedium of specifying the id-terms suppl tuple(“XY Z Assoc.”, “Main St. USA”) and suppl tuple(“Info Ltd.”, “P.O. Box OO”) for the above tuples (in constructing these id-terms we used only the functional attributes and assumed a fixed order ⟨name, addr⟩ of these attributes).

It should be clear that the “∗”-style objects have different semantics than the “ ”-style objects. For instance, the former are value-based and can be used on their own. Their object ids are replaced “∗” simply because the corresponding id-terms are uniquely determined by the values of the functional attributes, and therefore specifying these ids explicitly would be redundant. In comparison, the “ ”- style objects are not value-based. The identity of such an object, O, depends on the syntactic position occupied by this object inside another F-term; it does not directly depend on the values of attributes on O. However, the commonality between the two styles is that in both cases explicit specification of object identity is redundant, as it is derivable from the context (in each case differently, though).

7.4 Encapsulation, Database Views

Encapsulation is an important ingredient of object-orientedness. In a nutshell, encapsulation is a mechanism that permits different groups of users to have different views of the same object by giving them access to certain methods, while shielding others out of sight and making them inaccessible. For instance, for a class person with the signature

person[name ⇒ string; age @ date ⇒ int; salary @ year ⇒ int],

the method salary may have to be shielded from the public view because of the sensitivity of this information. In other cases, certain methods may be viewed as “internal functions” used to implement other methods, as in

\begin{aligned}rel algebra[…; & select @ relation ⇒ relation; project @ relation ⇒ relation; \\ & get first @ relation ⇒ tuple; get next @ relation, tuple ⇒ tuple; …], \end{aligned}

where the methods get first and get next may be deemed as inaccessible to the general public, since these are low-level internal routines used to implement the relational operations select, project, and so on.

In the framework of F-logic, the semantics of encapsulation can be defined as follows. Let P be a welltyped program. First, with every user (or a group of users) U we associate a type-declaration, T Y P E^{U}, that is supposed to contain appropriate signatures for the user. Then, we define a legal view of U to be any program P^{U} that contains no signatures in the rule heads, such that P |≈ P^{U} and P^{U} ∪ T Y P E^{U} is type-correct (“|≈” is the non-monotonic entailment relation discussed in Sections 4.3 and 4.5.2).

As an illustration, we could define a signature for the user Joe Public as

\begin{matrix}person[name ⇒ string; age @ date ⇒ int] \\ rel algebra[select @ relation ⇒ relation; project @ relation ⇒ relation], \end{matrix}

which will make it a type error for Joe Public to invoke the method salary on any member of the class person or, say, get first on rel algebra.

The concept of database views is a combination of a view-definition mechanism and encapsulation. The former is captured in F-logic in a very general form by means of deductive rules, while the latter is formalized via signature declarations, as explained above.

Many object-oriented languages (e.g., C++ [Str86]) allow classes to share some of their methods (called private methods) with subclasses, but hide them from all other classes. We know of no elegant way of expressing this kind of encapsulation in a logical framework.

7.5 Versions Control

Although versions control is not considered to be a mandatory feature of object-oriented databases, it has been often associated with such databases because of the importance of versions control in CAD. Conceptually, versions control has two distinct functionalities: creation of a new version and navigation among the existing versions. Creation of a new version is similar to an update, except that the old version of the updated object is retained. Fortunately, retaining the history of every object makes logical representation of versions control easier than the related problem of updates. Below we outline one of the several possible schemes for realizing versions control in F-logic.

Suppose Mary and John are working cooperatively on designing a chip, denoted chip123. Each time Mary makes a modification to a version v of the chip, she creates a new object, version_{mary}(v). Likewise, John constructs versions denoted version_{john}(v). Thus, all versions of the chip have the form f_{n}(...(f_{1}(chip123))...), where each f_{i} is either version_{mary} or version_{john}.

Mary and John access the current version of chip123 via the name current(chip123). When they decide to declare, say, the version version_{mary}(version_{john}(version_{john}(chip123))) to be the current one, they assert an equation

current(chip123) ≐ version_{mary}(version_{john}(version_{john}(chip123)))

and retract any other equation of this form that might have been previously asserted.

Navigation through versions is easy. For instance, to get to the previous version of the chip, one can use the following combination:

… ← current(chip123) ≐ V ersionConstructor(P revV ersion) & P revV ersion[…] & …

Strictly speaking, variables over function symbols, such as V ersionConstructor, are not permitted in F-logic, but we can easily accommodate this feature of HiLog, along the lines of [CKW89a].^{17}

Another way to organize versions in F-logic is to define a method, version, that returns appropriate versions, depending on the argument. To access a version of chip123, one could then use

… ← … & chip123[version @ arg → V ersion] & V ersion[…],

where arg is a suitable encoding of the desired version.

17The same effect can be achieved without appealing to HiLog if we encode versions differently, e.g., version(john, chip).

The encoding used earlier seems more natural, though.

7.6 Path Expressions

Many calculus-like object-oriented languages (e.g., [Zan83, BKK88]) use syntactic constructs known as path expressions. For instance, in (9) of Figure 4 they would use a path expression X.employed.dname ≐ “CS” to select employees working in “CS” departments.

Although path expressions are not part of F-logic syntax, they can be introduced as a syntactic sugar to help reduce the number of variables in F-logic rules, e.g. in Figure 4 we could write

? − X : empl[name → N] & X.friends.name ≐ “Bill” & X.employed.dname ≐ “CS”

instead of

? − X : empl[name → N; friends → → {F [name → “Bill”]}; employed → D[dname →
“CS”]] ].

Formal translation of path expressions into F-logic is left to the reader as a simple exercise. The only subtle point here is translation of paths that end with set-valued attributes. For instance,

… ← … & X.friends ≐ Y.enemies & …
… ← … & X.friends ⊆ Y.enemies & …,

where friends and enemies are both set-valued,^{18} should be translated into

… ← … & ¬unequal(X, friends, Y, enemies) & …
… ← … & ¬nonsubset(X, friends, Y, enemies) & …,

where the predicates unequal and nonsubset are defined as follows:

nonsubset(O_{1}, SetAttr1, O_{2}, SetAttr_{2}) ← O_{1}[SetAttr_{1} → → {X}] & ¬O_{2}[SetAttr_{2} → → {X}]
unequal(O_{1}, SetAttr_{1}, O_{2}, SetAttr_{2}) ← nonsubset(O_{1}, SetAttr_{1}, O_{2}, SetAttr_{2})
unequal(O_{1}, SetAttr_{1}, O_{2}, SetAttr_{2}) ← nonsubset(O_{2}, SetAttr_{2}, O_{1}, SetAttr_{1}).

7.7 User-defined Inheritance

DAG-structured class-hierarchies have forced their way into many object-oriented languages because of the convenience and flexibility offered by such systems. However, this convenience comes at a price of having to deal with a new problem: conflicting multiple inheritance. In Section 4.5, we described a credulous approach to resolving inheritance conflicts that takes into account all “possible worlds” obtained by nondeterministically choosing one of the conflicting inherited values. The problem with this approach is that there may be an exponential number of such worlds. Other, skeptic, approaches assert that nothing should be inherited in case of a conflict. Although computationally more tractable, practically this solution may be unacceptable since it may be hard for a programmer to identify inheritance conflicts and correctly anticipate system’s response.

18We ignore the possible ambiguity due to the fact that the same name can be used both for functional and set-valued attributes.

As a pragmatic alternative, several object-oriented languages rely on the user to tell which of the possibilities is to be inherited (e.g., Eiffel [Mey88], C++ [Str86]); inheritance conflicts are then detected at compile and/or run time, and are treated as errors.

Expressing user-defined inheritance in F-logic is easy. To resolve a conflict, say, in a 2-ary method mthd, we first parameterize mthd by defining a series of methods, param(mthd, Class):

Class[param(mthd, Class) @ X, Y → Z] ← Class[mthd @ X, Y → Z].

Now, let super_{1}, ..., super_{n} be all the superclasses of cl to which the method mthd applies. Then cl will inherit the methods param(mthd, super_{1}), ..., param(mthd, super_{n}). This time, however, there is no conflict between these methods, due to parameterization. So, the class cl can invoke the mthd-method defined on any of its superclasses, e.g.

… ← …, cl[param(mthd, super_{7}) @ a, b → Z], …

Another way of handling inheritance explicitly is to redefine mthd on cl, making it behave as mthd, say, on the class super_{7}:

cl[mthd @ X, Y → Z] ← super_{7}[mthd @ X, Y → Z].

The later approach is less general, though.

8 Assorted Examples

8.1 Browsing Database Schema

As explained earlier, although F-logic formally has a first-order semantics, its syntax is higher-order, which makes it possible to model certain higher-order concepts such as sets, class hierarchies, and database schema. The first two are modeled by means of set-valued functions and is-a F-terms, while schema can be reasoned about (browsed) because methods, attributes and objects are represented via the same medium of id-terms and because signature F-terms are ordinary formulas of the logic.

In this subsection we discuss the browsing capabilities of F-logic. Higher-order languages for deductive databases were also discussed in [KN88] and recently in [CKW89b]. However, the treatment in [KN88] is not as general and integrated as in F-logic, while [CKW89b] is more of a relational rather than objectoriented language.

Typically, database queries are specified with respect to an existing scheme that is assumed to be known to the user. The practice shows, however, that this assumption is unrealistic and some kind of browsing through the database is necessary. This means that the user has to apply intuitive or exploratory search through the structure of the scheme and the database at the same time and even in the same query (cf. [Mot86]). Many user interfaces to commercial databases support browsing to different extents. The purpose of the following examples is to demonstrate that F-logic provides a unifying framework both for data and schema exploration. We again refer to the example of Section 3.1.

The following pair of rules collects for each object in class faculty all attributes (including inherited ones) that have a value (or a set of values) in class person:

\begin{aligned}interesting attributes(X) [attributes → → \{L\}] & ← & X : faculty[L → Z : person] \\ interesting attributes(X) [attributes → → \{L\}] & ← & X : faculty[L → → \{Z : person\}]. \end{aligned}  (14)

For every faculty-object, o, these rules define a new object, interesting attributes(o), with a set-valued attribute attributes. The intuitive reading of these rules is: If L is a functional (or a set-valued) attribute that has a person-value Z (resp., set-value containing a person Z) for object X, then L belongs to the set representing the value of attributes on the object interesting attributes(X).

In addition, we ought to specify the type of the new objects created by the above rules. One way to do this is to decide on class membership for interesting attributes(X), e.g.

interesting attributes(X) : interesting attributes(faculty) ← X : faculty

and then postulate

interesting attributes(faculty)[attributes ⇒ ⇒ { }].

Thus, for the example of Figures 2, 3, and 4, we obtain: interesting attributes(bob) = {boss} and interesting attributes(mary) = {friends}. Deleting person in the bodies of rules (14) yields the set of all attributes that have some value.

Another example of browsing is the retrieval of all objects that mention some other object directly or indirectly (via subobjects). This can be specified as a function that returns the set of all objects referring to the object passed as an argument (the Stuff variable):

browser[find @ Stuff → → {X}] ← X[Y → Stuff ]
browser[find @ Stuff → → {X}] ← X[Y → → {Stuff }]
browser[find @ Stuff → → {X}] ← X[Y → Z] & browser[find @ Stuff → → {Z}]
browser[find @ Stuff → → {X}] ← X[Y → → {Z}] & browser[find @ Stuff → → {Z}].

For the running example in Figure 4, the query ? − browser[find @ “CS” → → {X}] will return the set {cs_{1}, cs_{2}, bob, mary }. The type of the browser-object can be given as

browser[find @ object ⇒ ⇒ { }],

where the class object is defined by the clause Y : object.

8.2 Methods

Methods is a way of achieving data abstraction in object-oriented programming. Since they embody the procedural aspect of the object-oriented paradigm, many researchers believed that methods cannot be cast into a declarative setting. For instance, [LR88, LR89] propose a formal data model for a procedural object-oriented language. Similarly, [BNT88] attempts to combine a generally declarative language with methods written in procedural languages.

In F-logic, methods can be defined declaratively. The basic mechanism here is function definition. For instance,

P [graduation dates @ I → → {Y }] ←

I : university[alumni → → {G : alumnus record[stud → P : person; date → Y : year]}]

defines graduation dates as a function from universities to (sets of) years, and one can ask queries

\begin{matrix}? − X[graduation dates @ I → → \{1987\}] \\ ? − john[graduation dates @ I → → \{Y \}] \end{matrix}

to find all persons who graduated from anywhere in 1987, or to find dates and universities john graduated from. Here graduation dates is explicitly defined for every person. Alternatively (and, in fact, closer to the spirit of object-oriented programming), we could specify graduation dates as a method that is explicitly defined only for the class person but is inherited by all members of that class:

person[graduation dates @ P, I → → {Y }] ← I : university[alumni → → {G : alumnus record[stud → P : person, date → Y : year]}].

In object-oriented languages, the ability to inherit methods and build them up incrementally is responsible for much of the success of this approach in human interfaces and graphics. The following example illustrates how this occurs in F-logic.

Suppose that male : person, female : person and writer : person hold true. We can define the function legal names applicable to every object of class person as follows. Normally, the legal name is the last name of a person. However, maiden name of a married female as well as pen-name of a writer is also considered to be a legal name. We can first explicitly define this function for every person:

person[legal names @ year ⇒ ⇒ string; last name @ year ⇒ string]

female[maiden name ⇒ string]
writer[pen name @ year ⇒ string]
X[legal names @ Y → → {N}] ← X : person[last name @ Y → N]

and then refine it for females and writers:

\begin{matrix}X[legal names @ Y → → \{N\}] ← X : female[maiden name → N] & Y : year \\ X[legal names @ Y → → \{N\}] ← X : writer[pen name @ Y → N]. \end{matrix}

Thus, if in 1988 mary was a married female, a writer, and used her husband’s last name, she would have had three different legal names in that year. On the other hand, joe who is a male and not a writer has only one legal name.

Notice that, in the above rules, there is no need for the restriction N : string because the database cannot have facts that would enable these rules with N bound to a non-string. For, if there were such facts, they would be inconsistent with the signatures above, resulting in a type error.

To illustrate the difference between monotonic and non-monotonic inheritance, we represent this problem in yet another way, by writing explicit definitions of legal names for the classes person, female, and writer only; non-monotonic inheritance is then used to propagate these definitions to individual objects:

\begin{aligned}person[legal names @ P, Y → → \{N\}] & ← & P : person[last name @ Y → N] \\ female[legal names @ F, Y → → \{N\}] & ← & F : female[maiden name → N] & Y : year \\ writer[legal names @ W, Y → → \{N\}] & ← & W : writer[pen name @ Y → N]. \end{aligned}

Every female will now inherit the version of the method defined for the class female. For instance, if sally is a female, the query

? − sally[legal names @ sally, 1990 → → {N}]

will return Sally’s maiden name; when applied to a writer, a similar query will return this writer’s penname. For females who are also writers, however, there will be two canonic models: one in which this method is inherited from female and another where the inheritance comes from the class writer. In neither case, will this method return the last name! The culprit here is, of course, the overriding property of nonmonotonic inheritance. To obtain the same result as in the first representation of the legal-names problem, we must force legal names to behave monotonicly (see Section 4.5) by adding the following rule:

X[legal names @ Obj, Y → → {N}] ← X : Z & Z[legal names @ Obj, Y → → {N}].

This rule guarantees that legal names will incrementally accumulate all legal names that can be inherited from superclasses (but weren’t – in the previous case – because of overriding).

If in the previous example we had to make an extra effort to cancel the overriding effect of nonmonotonic inheritance, the following practical problem shows when such inheritance is quite helpful.

Suppose every course has an instructor-defined algorithm for computing a grade for each student. This algorithm is to be applied to each student, unless there are extenuating circumstances, such as illness or extra-credit work. In the latter cases, the grade is computed using special algorithms, depending on the individual situation. Let the normal grade-computation algorithm be accessible via a method grade:

course[grade @ student ⇒ int]

so that, say, the query ? − db[grade @ sally → G] will return sally’s grade earned in the Databases course. Next, we define

student[grade @ Stud, Crs → G] ← Crs[grade @ Stud → G]

to be a method attached to the class student. To override this definition for bob and john, we can write

bob[grade @ bob, vlsi → G] ← some other definition
john[grade @ john, Crs → G] ← yet another definition.

Here bob’s grade-computation is changed only for the VLSI course. In contrast, for john it has been changed for all courses (perhaps because John is a college sportsman or is prominent in some other way). We may further write

Stud[grade @ Crs → G] ← Stud : student[grade @ Stud, Crs → G]

to simplify the calling pattern for the method grade. We can also prevent students from seeing each other’s grades through the mechanism of encapsulation described in Section 7.4. To this end, we can associate an appropriate signature stud obj[grade @ course ⇒ grade] with every student-user, e.g., bob[grade @ course ⇒ grade] can be associated with the user Bob.

To further illustrate the modeling power of F-logic, we exhibit one more way of method overriding, the one that is close to the spirit of Smalltalk [GR83]:

\begin{matrix}student[grading method → default grading] \\ john[grading method → john grading] \\ X[grade @ Crs → G] ← X : student[grading method → M; M @ Crs → G]. \end{matrix}  (15)

The third rule here defines grade as a method whose name is specified as a value of the grading method attribute. This value is normally inherited from the class student (i.e., default grading), unless it is explicitly overwritten, as in the case of john.

8.3 Analogies and the Like

Reasoning by analogy is an active field of research (e.g., see a survey [Hal89]). Apart from the semantic and heuristic issues, there is a need in finding suitable languages to express analogies. In this subsection we show that analogies among methods and classes can be described in F-logic fairly easily.

In Section 3.1, we had a method that, when applied to a person-argument on behalf of a personobject, returns the set of all joint works of the two people. This is just one instance of the situation where joint projects, common hobbies, and other commonalities may be involved. We can abstract this concept and define a “generic” method for joint things:

C[joint(M) @ list(C) ⇒ ⇒ {T ype}] ← C[M ⇒ ⇒ {T ype}]
X[joint(M) @ nil → → {Z}] ← X[M → → {Z}]
X[joint(M) @ cons(F irst, Rest) → → {Z}] ← F irst[M → → {Z}] &
X[joint(M) @ Rest → → {Z}].

The first rule says that, given a method M, the argument-type of the new method, joint(M), is the same as the class on which this method is defined; the type of the output of joint(M) is the same as that of M. The last two rules define the concept of “jointness.”

Our second example describes similarity among classes expressed by the like-relationship (cf. [Hay79, BS88]). For instance, one can say that “Whale is like Fish via habitat” or “Pig-like-person is like Pig via nose and legs.” Notice that the like-similarity is, in a sense, dual to the subclass relationship: A likerelationship says that the two classes are essentially different, except for a small number of properties that one class inherits from another. In contrast, an is-a link means that the two are essentially similar, except for a small number of properties overwritten by the subclass. Smalltalk-80 [GR83] also permits “nonstrict” subclasses that have an option of not inheriting (as opposed to overriding) methods from their superclasses. Such non-strictness is better described via the analogy mechanism rather than through the is-a relationship.

The like-similarity can be expressed by means of a ternary like-predicate. For instance, we could state like(pig-like-person, pig, cons(legs, cons(nose, nil)) ), where the third argument is a list of attributes relating the classes specified in the first two arguments. We could then define:

\begin{aligned}C_{1}[Attr → → \{P \}] ← C_{2}[Attr → → \{P \}] & & like(C_{1}, C_{2}, P ropList) \\ & & member(Attr, P ropList), \end{aligned}

where member is the membership predicate; it can be defined by a simple Prolog program. A similar rule can be used to define similarity between functional attributes.

As we have shown, F-logic has quite powerful tools for defining similarity among classes. However, representing similarity among methods of arbitrary arities would require one like_{n} predicate for each arity n ≥ 0 and one rule of the form

\begin{aligned}C_{1}[M @ X_{1}, ..., X_{n} → P] ← C_{2}[M @ X_{1}, ..., X_{n} → P] & & like_{n}(C_{1}, C_{2}, P ropList) \\ & & member(Attr, P ropList). \end{aligned}

Finding a finite representation for this case is an open research problem.

8.4 Miscellaneous

The following is an F-logic counterpart of a canonic textbook example:

list(T)[append @ list(T) ⇒ list(T)]
L[append @ nil → L] ← L : list(T)
cons(X, L1)[append @ L2 → cons(X, L3)] ← L1 : list(T)[append @ L2 → L3] & X : T.

Here L, L1, etc. are list-objects while append is an attached method that, given a pair of lists, returns a concatenated list. The polymorphic type list(T) was defined in Section 4.2.1.

Writing a comprehensible Prolog interpreter for relational algebra is a rather challenging undertaking. First, one should parse a relational expression given as an input. For example, an expression ((P × V) ∪ W) ⋈_{jcond} (Q − R) would be converted into a term of the form

join( union(prod(P, V), W), minus(Q, R), jcond).

This part of the task is quite simple and can be found in many guides to Prolog. Once an expression is parsed, it has to be evaluated. Surprisingly, evaluators for joins, Cartesian products, and the like are quite cumbersome and take anywhere from one to two pages of Prolog code. The main difficulty here is the fact that arity of expressions is unknown at compile time, which calls for the use of various nonlogical features such as “=..”, “arg”, and “functor”. Also, as pointed out in [CKW89a], another, relatively minor, deficiency is Prolog’s inability to use complex terms as predicate names. We now show how a page-plus-long Prolog program for the relational join evaluator can be written in just three rules in F-logic.

Relations are represented as in Section 3.5, that is, each relation, p, is a class of tuple-objects. Given a pair of relations P, Q and a join condition jcond, the program creates a new relation, join(P, Q, jcond).

Join-conditions are represented as terms of the form jcond(A, B, jcond(…)); e.g., jcond(A_{1}, B_{1}, jcond(A_{2}, B_{2}, nil)), encodes the equi-join condition A_{1} = B_{1} & A_{2} = B_{2}. The first pair of rules computes ids of tuples in the join. The third rule extracts properties of those join-tuples whose ids are already known from the first two rules:

\begin{aligned}jtupl(I, J) : join(P, Q, nil) ← & I : P & J : Q \\ jtupl(I, J) : join(P, Q, jcond(L, M, Rest)) ← & I : P [L → X] & J : Q[M → X] \\ & & jtupl(I, J) : join(P, Q, Rest) \\ jtupl(I, J)[rename1(L) → X, rename2(M) → Y] ← & I : P [L → X] & J : Q[M → Y]. \end{aligned}  (16)

Now, if dept has attributes dname, mngr while the relation empl has attributes dname, ename, the query ? − X : join(dept, empl, jcond(dname, dname, nil))[Y → Z] will return a join of the two relations on the attribute dname. It is easy to see that if the relations to be joined do not have attributes in common or if the join is natural, the function symbols rename1 and rename2 in the third rule can be dropped. Additionally, in case of a natural join, the join-condition itself can be simplified to a list of attributes (compared to a list of pairs of attributes).

In fact, the above program does a more general job by joining classes rather than just relations. It also demonstrates the difference that a language can make: In Prolog, a purely logical specification of join entails a rather sophisticated encoding of relations which – in the end – results in a code that does not deserve to be called “declarative.”

Relations can be represented also in another instructive way—as objects of classes relation(n), for each arity n. Signatures of these classes can be defined as follows:

\begin{matrix}relation(N) & [tuples ⇒ ⇒ \{tuple(N)\}] ← N : int \\ tuple(N) & [arg(M) ⇒ \{ \}] ← 1 ≤ M ≤ N & N : int. \end{matrix}  (17)

To declare an object, e.g., p, as an n-ary relation, we simply write p : relation(n). This causes p to inherit the signature of relation(n), which makes it a set of n-ary tuples. Attributes of p will then be arg(i), i = 1, ..., n. Relational-algebraic operations for this representation are not more difficult than for the representation discussed earlier. It is left as an exercise to adapt the join evaluator (16) to the new representation.

The signatures in (17) do not assign meaningful names to attributes. If attributes are required to have meaningful names (rather than just arg(i) ) then we would have to declare the signature for each relation individually:

\begin{matrix}supplier : relation \\ dept : relation \\ relation[tuples ⇒ ⇒ \{ \}] \\ supplier[tuples ⇒ ⇒ \{tuple(supplier)[sname ⇒ string; part ⇒ part]\}] \\ dept[tuples ⇒ ⇒ \{tuple(dept)[dname ⇒ string; mngr ⇒ mngr]\}] \\ supplier[tuples → → \{∗ : tuple(supplier)[sname → “acme”; part → gadget123]\}] \\ supplier[tuples → → \{∗ : tuple(supplier)[sname → “acme”; part → gadget321]\}] \\ dept[tuples → → \{∗ : tuple(dept)[dname → “CS”; mngr → bob]\}]. \end{matrix}  (18)

Since in this new schema of things we do not know the structure of various relations in advance, the signature for the class relation does not supply much information. The primary purpose of this class would be to help distinguish between relations and non-relations (e.g., as in … ← … & R : relation). Signatures for supplier (or dept) tell us that each tuple of the relation must be in the class tuple(supplier) (resp., tuple(dept) ) and have appropriate attributes. We remind that the constructs part ⇒ part and mngr ⇒ mngr in (18) are legal, since on the left-hand side of the arrow part and mngr are interpreted as methods while on the right-hand side they are seen as objects. Such name overloading helps in making programs more readable and eliminates the need in inventing distinct names, such as “part-as-an-attribute” and “part-as-a-class.” The last triple of facts defines the contents of relations. Recall from Section 7.3 that the “∗”-style don’t-care notation indicates a value-based object (a relational tuple) and is used as a shorthand for supplier tuple(“acme”, gadget123), supplier tuple(“acme”, gadget321) and dept tuple(“CS”, bob), respectively; supplier tuple and dept tuple denote some system-generated new function symbols. As an exercise, the reader may want to rewrite the 3-rule Join Example in (16) using the representation in (18).

Another interesting problem is to define the powerset operation that takes an arbitrary set and constructs its powerset. First, we define the class of sets that contains objects denoted by id-terms of the form add(a, add(…)). The intended meaning of a set-object such as add(a, add(b, add(c, nil))) is the set {a, b, c}. The class of sets is defined as follows:

nil : set
add(X, L) : set ← L : set
add(X, add(Y, L)) ≐ add(Y, add(X, L)).

The last equation asserts that the order in which elements are added to sets is immaterial. Next, we define the attribute self that for every object of the class set returns the set represented by this object:

nil[self → → { }]
add(X, L)[self → → {X}] ← L : set
add(X, L)[self → → {Y }] ← L : set[self → → {Y }].

Finally, the powerset method is defined as follows:

set [ powerset ⇒ ⇒ {set}; self ⇒ ⇒ { }]
S [ powerset → → {nil}] ← S : set
S [ powerset → → {add(Z, L)}] ←  S : set[self → → {Z}; powerset → → {L}]
& L : set & ¬L[self → → {Z}].

The first clause simply establishes signatures of the methods involved; the second one tells us that an empty set is a member of any powerset. Finally, the last rule says that any set constructed from a subset of S by adding to it a new element of S, also belongs to the powerset of S.

Our final example is an adaptation from [AK89]. The problem in question is the representation of data functions of COL [AG87] and grouping of LDL [BNST87].

Consider a graph given as a relation graph(X, Y) whose tuples represent edges of the graph. The task is to re-structure this graph by representing it via a set of nodes such that each node points to a set of its descendants. The corresponding F-logic program is very simple:

rebuilt graph[nodes → → {Node[descendants → → {D}]}] ← graph(Node, D),

where rebuilt graph is a new object. If typing is required, it can be specified as follows:

\begin{matrix}rebuilt graph[nodes ⇒ ⇒ \{node\}] \\ node[descendants ⇒ ⇒ \{node\}]. \end{matrix}

Here node denotes an appropriate programmer-defined class of all nodes.

In fact, extending the syntax in the direction of HiLog [CKW89a] by allowing variables over predicate names, we could rewrite this program in a “generic” way:

rebuilt(Graph)[nodes → → {Node[descendants → → {D}]}] ← Graph(Node, D)_{& Graph : graphs,}

where Graph is a variable and graphs is an appropriately defined class. This rule will restructure any graph that is passed as a parameter, e.g.

? − rebuilt(your favourite graph)[nodes → → {Node[descendants → → {D}]}],

will return a rebuilt version of your favourite graph.

9 Overview of the F-logic Tool Kit

At this point it would be instrumental to take another look at the structure of F-logic and clarify its relationship with predicate calculus. It is not hard to see that the various components of F-logic are independent from each other both semantically and proof-theoretically. A high-level view of the Flogic “guts” is depicted in Figure 9. It shows the two main aspects of F-logic: the monotonic and the nonmonotonic one. The latter is built on top of the former. The proof theory presented in Section 6 is sound and complete for the monotonic part, while the nonmonotonic extension has no complete proof theory. This stems from the fact that even for logic programs with stratified negation [ABW88, Van86] there is no such theory.

The two main components of the monotonic department, the logics of objects and types, are independent from each other, which can be seen by inspecting the semantics and the proof theory presented earlier. The glue between these two sublogics is provided by the well-typing semantic conditions of Section 3.3 and by the well-typing, type inheritance, and the two supertyping inference rules of Section 6. It is easy to see that the two sublogics become completely decoupled once the well-typing conditions in the definition of semantic structures are removed.

The third component, which we call “HiLog-ization”, extends the syntax of F-logic in the direction of HiLog [CKW89b, CKW89a]—a higher-order extension of predicate calculus that allows variables and even complex terms to appear in the positions of predicate and function symbols. For instance,

\begin{matrix}closure(Graph)(F rom, T o) ← Graph(F rom, T o) \\ closure(Graph)(F rom, T o) ← Graph(F rom, Mid), closure(Graph)(Mid, T o) \end{matrix}

e q u a l i t y - m i n i m a l e n t a i l m e n t Nonmonotonic part  L o g i c o f L o g i c o f o b j e c t s  t y p e s Monotonic part  ^{H i L o g - i z a t i o n}^{a n o n m o n o t o n i c t h e o r y o f n e g a t i o n}^{e n t a i l m e n t m i n i m a l f o r i n h e r i t a n c e}

Figure 9: F-logic Tool Kit

is a legal HiLog program. Notice that Graph is a variable ranging over predicates and closure(Graph) is a nonground term appearing in a syntactic position that is normally reserved for predicate symbols in the first-order predicate calculus. The program defines a generic operation of transitive closure of an arbitrary argument-relation: Given a binary relation graph, closure(graph) is another binary relation that is true of a pair ⟨from, to⟩ precisely when graph has a directed path connecting from and to.

The idea underlying HiLog is applicable to a wide range of logical languages, not just to predicate calculus, and the reader familiar with HiLog will have no difficulty to “HiLogize” F-logic. In order not to overwhelm the reader, we have conscientiously omitted all the HiLog features of F-logic in this paper. Nevertheless, on several occasions (e.g. during the discussion of versions control in Section 7.5 and in the graph-restructuring example in Section 8.4) we showed where these features could be helpful.

The nonmonotonic department of F-logic is also composed of a collection of independent tools. One of them is the equality-minimal entailment discussed in Section 4.4; it determines which object denotations refer to the same object. The next two – equally important – determine the semantics of nonmonotonic inheritance and negation. As discussed in Sections 4.5.2 and 4.2.1, there are several suitable nonmonotonic theories that formalize these aspects. Section 4.5.2 presents one such theory, called credulous inheritance. For negation, there is a number of competing proposals, such as stable [GL88], well-founded [GRS88, Van89], or inflationary [AV88, KP88] negation. Each of these can be also a part of the tool kit; Appendix A describes a perfect-model semantics for locally stratified F-logic programs.

Because of the independence of its various components, F-logic can be viewed as a tool-kit for designing custom-tailored declarative languages. In fact, there is a more fine-grained division inside the logic. For instance, the semantics of functional methods is independent from that of set-valued methods and we can consider the capability of handling each type of methods as a separate tool. Likewise, we could restrict the terms that denote classes and methods to be constants; method-name overloading can be also controlled in various ways. This tool-kit-like structure of F-logic is extremely helpful and allows one to address different aspects of the logic in separation from each other, both theoretically and implementationally.

The last issue to be illuminated upon is the relationship between predicate calculus and F-logic. In one direction, predicate calculus is a subset of F-logic and so the latter is more powerful than the former. However, it turns out that, in a sense, the two logics are equivalent. The following claim is left as an exercise to the reader:

Theorem 9.1 There are mappings

Γ : {F-logic well-formed formulas} ⟼ {predicate calculus well-formed formulas}
Φ : {F-logic semantic structures} ⟼ {predicate calculus semantic structures}

such that

M ⊧_{F} ψ if and only if Φ(M) ⊧_{P C} Γ(ψ),

for any F-logic semantic structure M and any F-logic formula ψ; here “⊧_{F} ” and “⊧_{P C}” denote logical entailment in F-logic and predicate calculus, respectively. □

The reader who might be puzzled by the revelation that F-logic is, in a sense, equivalent to predicate calculus, can find comfort in the following arguments: Our declared goal was to provide a logical model for a class of languages that are collectively classified as object-oriented. Taking the mapping Γ of Theorem 9.1 for a meaning of the F-logic language would be a misnomer, since Γ itself is an algorithm that does not give us with much insight into the nature of concepts we are trying to model in this way. The reader who would follow our suggestion and verify the claim of Theorem 9.1 will invariably find out that even for simple F-logic programs their Γ-image is hard to digest. Another argument – well articulated in the concluding section to [CKW89a] – can be summarized as follows: Syntax counts! We hope that the numerous programming examples in this paper speak for themselves. The third point is that Theorem 9.1 relates only the monotonic part of F-logic to predicate calculus. Mapping the nonmonotonic components of F-logic into nonmonotonic theories for predicate calculus result in a conceptual maze.

Apart from its theoretical interest, Theorem 9.1 could be used as a quick argument showing that the monotonic part of F-logic has some complete proof theory. However, such a proof theory can hardly be useful for a practical implementation or for query optimization. One could also employ this theorem in an alternative proof of completeness of the proof theory given in Section 6. Nevertheless, we opted for a direct proof since Theorem 9.1 offers no insight into why this particular proof procedure is complete; nor does the use of this theorem save much space.

10 Conclusion

Unlike the relational approach initiated by Codd [Cod70] that was based on firm theoretical grounds, object-oriented databases were dominated by “grass-roots” activity where several implementations existed [KBC*87, Vba86, MSOP86] without the accompanying theoretical progress. As a result, many researchers had a feeling that the whole area of object-oriented databases is misguided, lacking direction and needing a spokesman, like Codd, who could “coerce the researchers in this area into using common set of terms and defining a common goal that they are hoping to achieve [NS89].”

Our contention is that the problem lies much deeper: When Codd made his influential proposal, he was relying on a large body of knowledge in Mathematical Logic concerning predicate calculus. He had an insight to see how a mere application of what logicians had already known for several decades can revolutionize a very practical field. Until now, logical foundations for object-oriented databases that are parallel to those underlying the relational theory were lacking and this was a major factor for the uneasy feeling. In his pioneering work [Mai86], Maier proposed a framework for defining model-theoretic semantics for a logic with an object-oriented syntax. However, he encountered many difficulties with his approach and subsequently abandoned this direction. As it turned out, the difficulties were not fatal, and the theory was repaired and significantly extended in [CW89, KW89].

In this paper, we proposed a novel logic that takes the C- and O-logics of [CW89, KW89] into a new dimension: F-logic is capable of representing essentially all of what is known as the object-oriented paradigm. We provided a formal semantics and showed that it embodies in a natural way the notions of complex objects, inheritance, methods, types, and so on. F-logic has a sound and complete resolutionbased proof procedure, which makes it also computationally attractive and renders it a suitable basis for developing a theory of object-oriented logic programming. The latter issue will be discussed in a companion paper.

Acknowledgements: We would like to thank Serge Abiteboul, Catriel Beeri, Mira Balaban, Weidong Chen, Rick Hull, David Maier, Shuky Sagiv, Rodney Topor, Moshe Vardi, David Warren and Gio Wiederhold for contributing their time to discuss ideas presented herein.

References

[AB70] R. Anderson and W.W. Bledsoe. A linear format resolution with merging and a new technique for establishing completeness. Journal of ACM, 17(3):525–534, 1970.

[AB87] S. Abiteboul and C. Beeri. On the power of languages for manipulation of complex objects. 1987. manuscript.

[ABD*89] M. Atkinson, F. Bancilhon, D. DeWitt, K. Dittrich, D. Maier, and S. Zdonik. The objectoriented database system manifesto. In Intl. Conference on Deductive and Object-Oriented Databases, pages 40–57, 1989.

[ABW88] K.R. Apt, H. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–148, Morgan Kaufmann, 1988.

[AG87] S. Abiteboul and S. Grumbach. COL: A logic-based language for complex objects. In Workshop on Database Programming Languages, pages 253–276, Roscoff, France, September 1987.

[AK89] S. Abiteboul and P.C. Kanellakis. Object identity as a query language primitive. In Proceedings of the ACM SIGMOD Conference on Management of Data, pages 159–173, 1989.

[AKW90] S. Abiteboul, P.C. Kanellakis, and E. Waller. Method schemes. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 16–27, April 1990.

[AN86] H. Ait-Kaci and R. Nasr. LOGIN: A logic programming language with built-in inheritance. Journal of Logic Programming, 3:185–215, 1986.

[AV88] S. Abiteboul and V. Vianu. Procedural and declarative database update languages. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 240–250, 1988.

[Bal86] M. Balaban. The generalized concept formalism – A frames and logic based representation model. In Proceedings of the Canadian Artificial Intelligence Conference, pages 215–219, 1986.

[Ban88] F. Bancilhon. Object-oriented database systems. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 152–162, 1988.

[Bee89] C. Beeri. Formal models for object-oriented databases. In Intl. Conference on Deductive and Object-Oriented Databases, pages 370–395, Elsevier Science Publ., 1989.

[BF79] P. Buneman and R.E. Frankel. FQL - A functional query language. In Proceedings of the ACM SIGMOD Conference on Management of Data, pages 52–58, 1979.

[BK86] F. Bancilhon and S.N. Khoshafian. A calculus of complex objects. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 53– 59, March 1986.

[BKK88] J. Banerjee, W. Kim, and K.C. Kim. Queries in object-oriented databases. In Proc. of the 4-th Intl. Conf. on Data Engineering, Los Angeles, CA, February 1988.

[BNST87] C. Beeri, S. Naqvi, O. Shmueli, and S. Tsur. Sets and Negation in a Logic Database Language (LDL). Technical Report, MCC, 1987.

[BNT88] C. Beeri, R. Nasr, and S. Tsur. Embedding ψ-terms in a horn-clause logic language. In Third International Conference on Data and Knowledge Bases: Improving Usability and Responsiveness, pages 347–359, Morgan Kaufmann, 1988.

[BO89] P. Buneman and A. Ohori. Using powerdomains to generalize relational databases. Theoretical Computer Science, 1989.

[BR87] C. Beeri and R. Ramakrishnan. On the power of magic. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 269–283, 1987.

[Bre87] G. Brewka. The logic of inheritance in frame systems. In Intl. Joint Conference on Artificial Intelligence, pages 483–488, 1987.

[BS88] M. Balaban and S. Strack. LOGSTER - A relational, object-oriented system for knowledge representation. In Intl. Symposium on Methodologies for Intelligent Systems, pages 210–219, 1988.

[Car84] L. Cardelli. A semantics of multiple inheritance. In Int. Symp. on Semantics of data Types, LNCS 173, pages 51–67, June 1984.

[CDV88] M. Carey, D. DeWitt, and S. Vanderberg. A data model and query language for EXODUS. In Proceedings of the ACM SIGMOD Conference on Management of Data, 1988.

[CHC90] W.R. Cook, W.L. Hill, and P.S. Canning. Inheritance is not subtyping. In ACM Symposium on Principles of Programming Languages, pages 125–136, 1990.

[Che90] W. Chen. A General Logic-Based Approach to Structured Data. PhD thesis, Department of Computer Science, SUNY at Stony Brook, 1990.

[CKW89a] W. Chen, M. Kifer, and D.S. Warren. HiLog: A first-order semantics for higher-order logic programming constructs. In Proceedings of the North American Conference on Logic Programming, October 1989.

[CKW89b] W. Chen, M. Kifer, and D.S. Warren. HiLog as a platform for database programming languages (or why predicate calculus is not enough). In R. Hull, R. Morrison, and D. Stemple, editors, Database Programming Languages, pages 315–329, Morgan-Kaufmann, June 1989.

[CL73] C.L. Chang and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

[CM81] W.F. Clocksin and C.S. Mellish. Programming in Prolog. Springer Verlag, 1981.

[Cod70] E.F. Codd. A relational model for large shared data banks. Communications of ACM, 13(6):377–387, 1970.

[CW89] W. Chen and D.S. Warren. C-logic for complex objects. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 369–378, March 1989.

[End72] H.B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.

[ER83] D.W. Etherington and R. Reiter. On inheritance hierarchies with exceptions. In National Conference on Artificial Intelligence, pages 104–108, Washington, D.C., 1983.

[FK85] R. Fikes and T. Kehler. The role of frame-based representation in reasoning. Communications of ACM, 28(9):904–920, 1985.

[GdS89] G. Gardarin, C. de Maindreville, and E. Simon. Extending a relational DBMS towards a rule-based system: An approach using predicate transition nets. In Thanos and Schmidt, editors, Foundation of Knowledge Base Management, Springer Verlag, 1989.

[GL88] M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Logic Programming: Proceedings of the Fifth Conference and Symposium, pages 1070–1080, 1988.

[GR83] A. Goldberg and D. Robson. Smalltalk-80: The Language and Its Implementation. Addison-Wesley, 1983.

[GRS88] A. Van Gelder, K.A. Ross, and J.S. Schlipf. The well-founded semantics for general logic programs. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 221–230, 1988.

[GV89] H. Geffner and T. Verma. Inheritance = chaining + defeat. In Intl. Symposium on Methodologies for Intelligent Systems, pages 411–418, 1989.

[Hal89] R.P. Hall. Computational approaches to analogical reasoning: A comparative study. Artificial Intelligence, 30:39–120, 1989.

[Hay79] P.J. Hayes. The logic for frames. In D. Metzing, editor, Frame Conception and Text Understanding, pages 46–61, Walter de Gruyter and Co., 1979.

[HTT87] J.F. Horty, R.H. Thomason, and D.S. Touretzky. A skeptical theory of inheritance in nonmonotonic semantic nets. In National Conference on Artificial Intelligence, pages 358–363, 1987.

[HY90] R. Hull and M. Yoshikawa. ILOG: declarative creation and manipulation of object identifiers. 1990. manuscript.

[KBC*87] W. Kim, J. Banerjee, H-T. Chou, J.F. Garza, and D. Woelk. Composite object support in an object-oriented database system. In Proceedings of OOPSLA-87, 1987.

[KC86] S.N. Khoshafian and G.P. Copeland. Object identity. In Proceedings of OOPSLA-86, pages 406–416, 1986.

[KK89] T. Krishnaprasad and M. Kifer. An evidence-based framework for a theory of inheritance. In Intl. Joint Conference on Artificial Intelligence, pages 1093–1098, 1989.

[KKW89a] T. Krishnaprasad, M. Kifer, and D.S. Warren. On the circumscriptive semantics of inheritance networks. In Intl. Symposium on Methodologies for Intelligent Systems, pages 448–457, 1989.

[KKW89b] T. Krishnaprasad, M. Kifer, and D.S. Warren. On the declarative semantics of inheritance networks. In Intl. Joint Conference on Artificial Intelligence, pages 1099–1103, 1989.

[KL89] M. Kifer and G. Lausen. F-logic: A higher-order language for reasoning about objects, inheritance and schema. In Proceedings of the ACM SIGMOD Conference on Management of Data, pages 134–146, 1989.

[KN88] R. Krishnamurthy and S. Naqvi. Towards a real horn clause language. In Intl. Conference on Very Large Data Bases, 1988.

[KP88] P.G. Kolaitis and C.H. Papadimitriou. Why not negation by fixpoint. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 231– 239, 1988.

[Kup87] G.M. Kuper. An Extension of LPS to Arbitrary Sets. Technical Report, IBM, Yorktown Heights, 1987.

[KV84] G. Kuper and M.Y. Vardi. A new approach to database logic. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, 1984.

[KW89] M. Kifer and J. Wu. A logic for object-oriented logic programming (Maier’s O-logic revisited). In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 379–393, March 1989.

[KW90] M. Kifer and J. Wu. A first-order theory of types and polymorphism in logic programming. In Intl. Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 1990. (this is a short version of the technical report 90/23 under the same title, Department of Computer Science, SUNY at Stony Brook, July 1990).

[Llo87] J.W. Lloyd. Foundations of Logic Programming (Second Edition). Springer Verlag, 1987.

[LR88] C. Lecluse and P. Richard. Modeling inheritance and genericity in object-oriented databases. In 2-nd Int. Conf. on Database Theory (ICDT), LNCS 326, pages 223–238, Springer Verlag, Bruges, Belgium, 1988.

[LR89] C. Lecluse and P. Richard. The O_{2} database programming language. In Intl. Conference on Very Large Data Bases, August 1989.

[Mai86] D. Maier. A logic for objects. In Workshop on Foundations of Deductive Databases and Logic Programming, pages 6–26, Washington D.C., August 1986.

[Mai87] D. Maier. Why database languages are a bad idea (position paper). In Proc. of the Workshop on Database Programming Languages, Roscoff, France, September 1987.

[Mai89] D. Maier. Why Isn’t There an Object-Oriented Data Model. Technical Report, Oregon Graduate Center, May 1989.

[McC79] J. McCarthy. First order theories of individual concepts and propositions. In J.E. Hayes and D. Michie, editors, Machine Inteligence, pages 129–147, Edinburgh University Press, 1979.

[Mey88] B. Meyer. Object-Oriented Software Construction. Prentice Hall, 1988.

[Min81] M. Minsky. A framework for representing knowledge. In J. Haugeland, editor, Mind design, pages 95–128, MIT Press, Cambridge, MA, 1981.

[Mis84] P. Mishra. Towards a theory of types in Prolog. In IEEE Symposium on Logic Programming, pages 289–298, 1984.

[Mit90] J.C. Mitchell. Toward a typed foundation for method specialization and inheritance. In ACM Symposium on Principles of Programming Languages, pages 109–124, 1990.

[MNS*87] K. Morris, J. Naughton, Y. Saraiya, J. Ullman, and A. Van Gelder. YAWN! (Yet another window on NAIL!). 1987. unpublished manuscript.

[Mot86] A. Motro. BAROQUE: A browser for relational databases. ACM Trans. on Office Information Systems, 4(2):164–181, 1986.

[MSOP86] D. Maier, J. Stein, A. Otis, and A. Purdy. Development of an object-oriented DBMS. In Proceedings of OOPSLA-86, pages 472–482, 1986.

[MW88] S. Manchanda and D.S. Warren. A logic-based language for database updates. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 363–394, Morgan-Kaufmann, Los Altos, CA, 1988.

[NS89] E. Neuhold and M. Stonebraker. Future directions in DBMS research (The Laguna Beech report). SIGMOD Record, 18(1), March 1989.

[NT89] S. Naqvi and S. Tsur. A Logical Language for Data and Knowledge Bases. Computer Science Press, 1989.

[PG89] H. Przymusinska and M. Gelfond. Inheritance hierarchies and autoepistemic logic. In Intl. Symposium on Methodologies for Intelligent Systems, 1989.

[Prz88] T.C. Przymusinski. On the declarative semantics of deductive databases and logic programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193– 216, Morgan Kaufmann, Los Altos, CA, 1988.

[Prz89] T.C. Przymusinski. Every logic program has a natural stratification and an iterated least fixed point model. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 11–21, 1989.

[PUM90] G. Phipps, J.D. Ullman, and Many Others. Glue-Nail definition. 1990. Draft.

[Ram88] R. Ramakrishnan. Magic Templates: A spellbinding approach to logic programs. In IEEE Symposium on Logic Programming, pages 140–159, 1988.

[RKS85] M.A. Roth, H.F. Korth, and A. Silberschatz. Extended Algebra and Calculus for ¬1NF Relational Databases. Technical Report 84-36, Univ. of Texas at Austin, 1985.

[SB86] M. Stefik and D.G. Bobrow. Object-oriented programming: Themes and variations. The AI Magazine, 40–62, January 1986.

[Sch77] J.W. Schmidt. Some high-level language constructs for data of type relation. ACM Transactions on Database Systems, 2(3):247–261, September 1977.

[She88] J.C. Shepherdson. Negation in logic programming. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 19–88, Morgan-Kaufmann, Los Altos, CA, 1988.

[Shi81] D.W. Shipman. The functional data model and the data language DAPLEX. ACM Transactions on Database Systems, 140–173, 1981.

[Sho88] Y. Shoham. Reasoning about Change. The MIT Press, 1988.

[Str86] B. Stroustrup. The C++ Programming Language. Addison-Wesley, Reading, MA, 1986.

[TH89] R.H. Thomason and J.F. Horty. Logics for inheritance theory. In 2-nd Intl. Workshop on Nonmonotonic Reasoning, Lecture Notes in Computer Science no. 346, pages 220–237, Springer Verlag, 1989.

[THT87] D.S. Touretzky, J.F. Horty, and R.H. Thomason. A clash of intuitions: The current state of nonmonotonic multiple inheritance systems. In Intl. Joint Conference on Artificial Intelligence, pages 476–482, 1987.

[Tou86] D.S. Touretzky. The Mathematics of Inheritance. Morgan-Kaufmann, Los Altos, CA, 1986.

[Ull87] J.D. Ullman. Database theory: Past and future. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 1–10, 1987.

[Van86] A. Van Gelder. Negation as failure using tight derivations for general logic programs. In IEEE Symposium on Logic Programming, Springer Verlag, 1986.

[Van89] A. Van Gelder. The alternating fixpoint of logic programs with negation. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 1– 10, 1989.

[Vba86] VBASE Object Manager. Ontologic, Inc., 1986. User Manual.

[Weg87] P. Wegner. The object-oriented classification paradigm. In B. Shriver and P. Wegner, editors, Research Directions in Object-Oriented Programming, pages 479–560, MIT Press, 1987.

[Xu89] J. Xu. A Theory of Types and Type Inference in Logic Programming Languages. PhD thesis, SUNY at Stony Brook, 1989.

[XW88] J. Xu and D.S. Warren. A type inference system for Prolog. In Intl. Conference on Logic Programming, pages 604–619, 1988.

[YS87] E. Yardeni and E. Shapiro. A type system for logic programs. In E. Shapiro, editor, Concurrent Prolog, MIT Press, 1987.

[ZAB*85] C. Zaniolo, H. Ait-Kaci, D. Beech, S. Cammarata, L. Kerschberg, and D. Maier. Object-Oriented Database and Knowledge Systems. Technical Report DB-038-85, MCC, 1985.

[Zan83] C. Zaniolo. The database language GEM. In Proceedings of the ACM SIGMOD Conference on Management of Data, pages 423–434, 1983.

A The Perfect-model Semantics for F-logic

The general principle that can be used to extend the various semantics for negation (e.g. [Prz88, GL88, GRS88, Van89, Prz89, AV88, KP88]) is that whenever predicates are used in the standard definitions, method names and predicate symbols should be used to port the corresponding notions to F-logic. For instance, for the perfect-model semantics, stratification must be ensured with respect to method names, so that

X[wants → → {Y }] ← ¬X[has → → {Y }]

would be stratified even though there is a recursion through negation within the same object X. In contrast, the rule (cf. [GRS88])

\begin{aligned}silly game[win pos → → \{P os_{1}\}] ← & ¬silly game[win pos → → \{P os_{2}\}] \\ & & P os_{1}[legal moves → → \{P os_{2}\}] \end{aligned}

is not locally stratified (in F-logic) since there is a recursion through negation in the method win pos when both P os_{1} and P os_{2} are instantiated to the same constant, say bad pos.

Another difficulty in adapting the perfect-model semantics to F-logic is the equality predicate “≐”. In [Prz88], perfect models were introduced assuming the so called freeness axioms for equality that postulate that ground terms are equal if and only if they are identical. Without these axioms, perfect models do not provide natural semantics even for simple locally stratified programs. For instance, although

\begin{matrix}a ≐ b ← ¬p(b) \\ p(a) \end{matrix}

has a unique perfect model {p(a), p(b), a ≐ b} (obtained using the definitions in [Prz88] in a simpleminded way), the trouble is that p(b) is not supported by any rule (in fact, p(b) was derived assuming ¬p(b) is true). In classic logic programming, this problem is side-stepped by disallowing equality to appear in the rule heads. Unfortunately, this shortcut does not work for F-logic, since equality is ubiquitous: Even if it is not mentioned explicitly, equality may be present implicitly, for {a : b, b : a} ⊧ (a ≐ b) and {a[attr_{1} ⇒ b; attr_{2} ⇒ c], a[attr_{1} → c; attr_{2} → b]} ⊧ (c : b ∧ b : c) ⊧ (b ≐ c).

Another problem comes from the signature-monotonicity axioms of the form X[M @ arg^{⟶}⇒ Y] ← X : Z & Z[M @ arg^{⟶}⇒ Y] that are built into the semantics of F-logic. These create an effect similar to recursive cycles through negation, when signatures are negatively dependent on other data (e.g. p(a) ← ¬b[attr ⇒ { }], a[attr ⇒ { }] ← p(a)).

A way out of this sticky situation (which also works for predicate calculus with equality) is to prohibit equality P-terms and is-a/signature F-terms to be dependent negatively on other literals. Formally, given an F-logic language L and a program P, we define a dependency graph, D_{L}(P), as follows: Let P^{∗} denote the set of all ground instances of P over L. The nodes of D_{L}(P) correspond to the ground atoms constructible in L (atoms are defined in Section 5.2). A positive arc φ ⟵^{⊕} ψ connects a pair of nodes φ, ψ if and only if there is a rule φ̄ ← …, ψ̄, … in P^{∗} such that φ, ψ are atoms of φ̄, ψ̄, respectively. In this notation, a negative arc φ ⟵^{⊖} ψ exists in D_{L}(P) iff P^{∗} has a rule φ̄ ← …, ¬ψ̄, … In addition to all that, D_{L}(P) has the following arcs: whenever some functional data-atoms a[ m @ b_{1}, ..., b_{n} → c] and a[ m @ b_{1}, ..., b_{n} → d], where a, m, b_{1}, ..., b_{n}, c, d are ground id-terms, appear in the heads of the rules in P^{∗}, then there are positive arcs (c ≐ d) ⟵^{⊕} a[ m @ b_{1}, ..., b_{n} → c] and (c ≐ d) ⟵^{⊕} a[ m @ b_{1}, ..., b_{n} → d]. A directed path or a cycle in D_{L}(P) is negative if it contains at least one negative arc. A program P is locally stratified if:

• D_{L}(P) has no negative paths leading into is-a, signature or equality atoms; and

• D_{L}(P) has no negative cycles.

If P is locally stratified, we can define stratification as a function

• level : {atoms of P^{∗}} ⟼ N

such that if D_{L}(P) has a directed path from φ to ψ then level(φ) ≤ level(ψ); if there is a negative such path, then level(φ) < level(ψ).

To complete the picture, we introduce a preference quasi-order: an untyped semantic structure M (not necessarily Herbrand) is preferable to N, denoted M ≪ N, if whenever there is an atom φ such that M ⊧ φ and N |̸= φ then there is an atom ψ such that level(ψ) < level(φ), N ⊧ ψ, and M |̸= ψ. To make ≪ a quasi-order, we also close it transitively. Models that are minimal with respect to ≪ are called perfect.

Proposition A.1 Every locally stratified program has a unique untyped Herbrand^{19} perfect model.

Proof: The proof is similar to that in [Prz88]. Another (simpler, but indirect) proof can be derived from Theorem 9.1. □

B Interaction of Inheritance and Deduction: Examples

In this appendix we illustrate some subtleties pertaining to the interaction between deduction and inheritance. Although computational details are beyond the scope of this paper, one of the purposes of the examples presented here is to foster the intuition about the underlying computation. Our first series of examples deals with methods that initially are inherited from superclasses and subsequently are modified by deductive rules. Again, to underline the subtlety of interaction between the equality and inheritance, we do not use ⊑^{eq}-minimization. Consider a program

\begin{matrix}b : a \\ a[attr → → e] \\ b[attr → → d] ← b[attr → → e], \end{matrix}  (19)

where signatures are left out. If b inherits attr → → e from a, then this would enable the third clause, yielding b[attr → → d]. So, we would have derived b[attr → → {d, e}]. But this undermines the fact that the value of attr on b was obtained by inheriting the set {e}, not {d, e}. As a result, inheritance does not take place and the answer to the query ? − b[attr → → {X}] is empty. Semanticly this happens for the following reason. There are three kinds of ⊑^{inh}-minimal models in this case:

I: Where ¬b[attr → → { }] holds;
J: Where b[attr → → {d, e}] and d ≠ e hold; and
K: Where b[attr → → {d, e}] and d ≐ e hold.

In the models of types J and K, inheritance does take place, but these models are subsequently eliminated by ≪-minimization. From the computational point of view, the morale is:

Principle 1: Once a class sub inherits m @ args^{⟶} → a (or m @ args^{⟶} → → {a_{1}, ..., a_{n}}) from a superclass sup, subsequent applications of deductive rules should not alter the result of invocation of m on args^{⟶} in the scope of sub. This means that no new fact of the form sub[m @ args^{⟶} → b] (or sub[m @ args^{⟶} → → b]) can be subsequently derived, unless a ≐ b (resp., a_{i} ≐ b) has been established prior to the moment the inheritance took place.

19Herbrand models are defined in Section 5.2.

Our next observation is that not only the inherited method in a subclass should remain undisturbed, but also the superclass-owned method that was used as an inheritance prototype should not be subsequently altered. Suppose that the last clause in (19) is replaced by

a[attr → → d] ← b[attr → → e].  (20)

Because of (20), the result returned by the method attr in the scope of the superclass a will be modified right after this method is inherited by b. Then, arguments similar to those for (19) show that this modification invalidates the inheritance of attr → → e and only the models of type I above will be among the canonic ones. This leads to the following:

Principle 2: Before the behaviour of a method m on args^{⟶} in the scope of a superclass sup can be inherited by a subclass sub, this behaviour must be fully known prior to attempting the inheritance of m; after the inheritance has taken place, subsequent applications of deductive rules cannot change this behaviour without invalidating the inheritance step. More precisely, after the inheritance has taken place, no new fact of the form sup[m @ args^{⟶} → b] (or sup[m @ args^{⟶} → → b]) should be subsequently derived, unless a ≐ b and sup[m @ args^{⟶} → a] (resp., sup[m @ args^{⟶} → → a]) were established earlier.

Inherited methods and their prototypes can be changed in even more subtle ways, as illustrated next. Consider the program:

\begin{matrix}q : p & p[attr → a] \\ r : q & q[attr → b] ← r[attr → a]. \end{matrix}  (21)

Here q inherits attr → a from p and then passes it along to r. The latter enables the last rule, causing q[attr → b] to be derived. However, this leads to a conflict with q[attr → a]. To restore consistency, the latest inheritance (from q to r) must be undone along with the derivation of q[attr → b], as the latter Fterm depends on the invalidated inheritance step. The reader can verify that according to the semantics of nonmonotonic inheritance (Section 4.5.2), the canonic models have the property that q[attr → a] is true but r[attr → a] is false. As before, in some ⊑^{inh}-minimal models inheritance does take place because a ≐ b holds there, but these models are not ≪-minimal and hence do not ultimately survive.

Suppose now that, in addition to (21), we had the rule

(a ≐ b) ← q[attr → a].  (22)

Then there are the following classes of ⊑^{inh}-minimal models:

I: Where q[attr → a] and a ≐ b hold;
J: Where (∀X)¬q[attr → X] and a ≠ b hold.

The models of types I and J are incomparable because I(attr, →)[p]( ) = {a, b} ≠ {a} = J(attr, →)[p]( ). However, the type J will prevail later at the ≪-minimization stage. So, adding (22) not only does not help r to inherit attr → a but also invalidates this inheritance for q.

The computational explanation here is as follows. Originally q inherits attr → a. However, when (22) is applied, a ≐ b is derived, modifying the prototype method p[attr → …] in the superclass p. Deriving a ≐ b is viewed as a modification because originally p[attr → b] was not a consequence of the program but, after the inheritance took place, a ≐ b and hence p[attr → b] became true. Such modification invalidates this inheritance step, causing it, computationally speaking, to be rolled back.

Now, suppose that the above equality a ≐ b does not depend on the inheritance of attr → a but may depend on inheritance of some other method. For instance, let in addition to (21) the following be in the program:

\begin{matrix}s : p \\ p[attr → a; attr′ @ c → h] \\ (a ≐ b) ← s[attr′ @ c → h]. \end{matrix}  (23)

Then inheritance of attr → a will take place anyway. Moreover, not only q will inherit attr → a but so will r and s!

The computational explanation here is that first s inherits attr′ → h and then a ≐ b is derived. After that, q inherits attr → a from p. The equality a ≐ b does not cause this inheritance to be rolled back because attr → a is inherited after the computation of attr is finished for the superclass p. This equality does not affect the inheritance of attr′ → h either because it does not alter attr′ in any way. On the other hand, if attr → a were inherited before a ≐ b was derived, then the subsequent derivation of a ≐ b would have caused this inheritance to be rolled back. Note, however, that after a ≐ b is established, the inheritance of attr → a can be tried again and this time it will be successful.

It should be noted that Principles 1 and 2 prohibit changes made to the results returned by the methods; for any method, its arguments and even its name may be equated without problem after an inheritance step is performed, as long as this does not change the result returned by this method. For instance, in (23), deriving c ≐ c′ or even attr′ ≐ attr′′ is harmless. However, if (23) contained, say, p[attr′ @ c′ → u] then equating c and c′ would have rendered s[attr′ @ c′ → u] a true statement, which changes the inherited method and thus should cause the inheritance of attr′ @ c → h by s to be rolled back. It should also be clear that these subtleties concerning equality do not arise when the equality definition EQ is a separate part of the program and when ⊑^{eq}-minimization is applied (Section 4.4).

For another example, consider this program:

\begin{aligned}a : t & t[attr → c] \\ b : t & b[attr → d] ← a[attr → c] \\ & a[attr → f] ← b[attr → c], \end{aligned}  (24)

where, again, type-declarations are omitted. If a inherits attr → c before b, causing the first rule to fire, then b[attr → d] is derived, precluding the inheritance from t to b. Similarly, if b inherits first, then a[attr → f] is derived, precluding the inheritance from t to a. Therefore, we have two kinds of canonic models here, even though the program consists of Horn clauses only. Intuitively, multiple models may arise because even simple class-hierarchies combined with deductive rules can create situations that are akin to multiple inheritance (compare this with Nixon’s Diamond).

The clause-set (24) demonstrates that even simple negation-free programs may have multiple inequivalent canonic models. Presumably, some sort of stratification that takes inheritance hierarchies into account can guarantee uniqueness, but the exact details need be worked out.

Our final example shows that inheritance from b to a may cause a and b to become equal (i.e., to represent the same class):

a : b
b[attr → c]
b : a ← a[attr → c].

The two interesting classes of models are those where inheritance does take place and hence a ≐ b and those where inheritance does not occur (and a ≠ b). Let I be a model where a ≐ b holds and

I(attr, →)[a]( ) = I(attr, →)[b]( ) = {c}.  (25)

Let J be another model where J |̸= (a ≐ b). Since a : b must hold everywhere, it follows that J |̸= b : a. Suppose J ⊧ ¬a[attr → c]. Then, although J(attr, →)[b]( ) = {c}, the set J(attr, →)[a]( ) does not contain c and may even be undefined. Therefore, because of (25), I ⊑^{inh} J. Computationally speaking, first a inherits attr → c, then b : a is derived, and finally a ≐ b is concluded.

C Perfect Models in the Presense of Inheritance

When inheritance is taken into account, atoms may become implicitly dependent on negation, even though no negative cycles may exist in D_{L}(P). Consider the following program:

\begin{matrix}a : b & b[attr → → \{X\}] ← ¬c[attr → → \{X\}] & d[attr → → \{X\}] \\ d[attr → → \{k, m, n\}] & c[attr → → \{X\}] ← a[attr → → \{X\}]. \end{matrix}

In the absence of inheritance, this program is stratified and the answer to the query ? − b[attr → → {X}] is X = k, m, n. However, with inheritance, c[attr → → {X}] becomes negatively dependent on itself. This invalidates the argument that earlier has led us to conclude b[attr → → {k, m, n}], since now a must inherit attr → → {k, m, n}, which in turn enables the fourth clause to derive c[attr → → {k, m, n}], rendering the derivation of b[attr → → {k, m, n}] unfounded.

To accommodate inheritance, we slightly amend the definition of D_{L}(P): If a : b occurs in the head of a ground instance of a rule in P then add a positive arc a[m @ b_{1}, ..., b_{n} → c] ⟵^{⊕} b[m @ b_{1}, ..., b_{n} → c] for all n ≥ 0 and m, b_{1}, ..., b_{n}, c ∈ F^{∗}. The resulting graph is denoted D_{L}^{+}(P). A program P is strongly locally stratified if:

• D_{L}^{+}(P) has neither negative cycles;

• nor negative paths leading into is-a, signature, or equality atoms.

The preference quasi-order ≪^{+} is defined as before, except that the graph D_{L}^{+}(P) is used instead of D_{L}(P). A strongly perfect untyped model of P is any semantic structure that is ≪^{+}-minimal within the class of ⊑^{inh}-models of P.

Proposition C.1 Every strongly locally stratified program has a strongly perfect untyped model.^{20}

20As (24) of Appendix B shows, this model may not be unique, even in the Herbrand case.

Proof: (Sketch) Take an ordinary perfect untyped model I of Appendix A, which exists by Proposition A.1. To get a strongly perfect untyped model, we expand I by performing inheritance whenever possible. Since there are no negative cycles through inheritance, we can construct a perfect model by firing rules in a stratum-by-stratum fashion, undoing inheritance steps when they lead to a conflict. According to Principles 1 and 2 of Appendix B, a conflict arises when subsequent applications of deductive rules cause changes in a method that was previously inherited by a subclass or if changes occur in a superclassowned method whose behaviour was earlier copied by a subclass. (This proof is non-constructive, as are the proofs of the corresponding results for classic logic programs.) □

It should be clear that Propositions A.1 and C.1 do not hold in the presense of ⊑^{eq}-minimization by the obvious reason that D_{L}(P) and D_{L}^{+}(P) do not take into account the equality-definitions found in P.

D An Algorithm for F-term Unification

This appendix presents an algorithm for finding a complete set of mgu’s for a pair of F-terms. We remind (Section 6.1) that any two complete sets of mgu’s are equivalent to each other and therefore it suffices to find just one such set. Recall that an F-term can be represented as a conjunction of its atoms. For a pair of F-terms T_{1} and T_{2}, an mgu of T_{1} into T_{2} is a most general substitution that makes every atom of T_{1} a subterm of some atom of T_{2}. Different correspondences between the atoms of T_{1} and T_{2} may lead to different mgu’s. To find a complete set of mgu’s, we must take all such correspondences into account. Let φ be an atom of either of the following forms:

1. P [Method @ Q_{1}, ..., Q_{k} → R], P [Method @ Q_{1}, ..., Q_{k} → → {R}], P [Method @ Q_{1}, ..., Q_{k} ⇒ {R}], P [Method @ Q_{1}, ..., Q_{k} ⇒ ⇒ {R}];

2. P [Method @ Q_{1}, ..., Q_{k} → → { }], P [Method @ Q_{1}, ..., Q_{k} ⇒ { }], P [Method @ Q_{1}, ..., Q_{k} ⇒ ⇒ { }].

The following notation will be used in the algorithm in Figure 10:

id(φ) = P,
method(φ) = Method,
arg_{i}(φ) = Q_{i}, for i = 1...k,
val(φ) = \{ \begin{matrix}R & if φ is of the form (1) above \\ ∅ & if φ is of the form (2) above. \end{matrix}

In addition, if T is an F-term then atoms(T) will denote the set of atoms of T. If T_{1} and T_{2} are F-terms then Maps(T_{1}, T_{2}) denotes the collection of mappings {λ : atoms(T_{1}) ⟼ atoms(T_{2})}, such that for each λ ∈ Maps(T_{1}, T_{2}) and φ ∈ atoms(T_{1}) the functionality and the arity of the methods in φ and λ(φ) are the same.

Input : Pair of data (or signature) F-terms T_{1} and T_{2}. Output : A complete set Ω of mgu’s of T_{1} into T_{2}.

1. If id(T_{1}) and id(T_{2}) are unifiable, then set θ := UNIF Y (< id(T_{1}) >, < id(T_{2}) >). Otherwise, stop: T_{1} and T_{2} are not unifiable.

2. If T_{1} is of the form S[ ] (a degenerated F-term), then stop: θ is the only mgu.

3. Set Ω := { }.

For each mapping λ ∈ Maps(T_{1}, T_{2}) do: Set σ_{λ} := θ. For each atom φ in atoms(T_{1}) do:

Let ψ =^{def} λ(φ).

If val(φ) = ∅ then Unify the tuples σ_{λ}(S⃗_{1}) and σ_{λ}(S⃗_{2}), where

S⃗_{1} =^{def} < method(φ), arg_{1}(φ), ..., arg_{n}(φ) >

S⃗_{2} =^{def} < method(ψ), arg_{1}(ψ), ..., arg_{n}(ψ) >.

If σ_{λ}(S⃗_{1}) and σ_{λ}(S⃗_{2}) are unifiable then set σ_{λ} := UNIF Y (σ_{λ}(S⃗_{1}), σ_{λ}(S⃗_{2})) ∘ σ_{λ}. else discard this σ_{λ} and jump out of the inner loop to select another λ.

else

Unify the tuples σ_{λ}(S⃗_{1}) and σ_{λ}(S⃗_{2}), where

S⃗_{1} =^{def} < method(φ), arg_{1}(φ), ..., arg_{n}(φ), val(φ) >

S⃗_{2} =^{def} < method(ψ), arg_{1}(ψ), ..., arg_{n}(ψ), val(ψ) >.

If σ_{λ}(S⃗_{1}) and σ_{λ}(S⃗_{2}) are unifiable then set σ_{λ} := UNIF Y (σ_{λ}(S⃗_{1}), σ_{λ}(S⃗_{2})) ∘ σ_{λ}. else discard this σ_{λ} and jump out of the inner loop to select another λ.

fi

Set Ω := Ω ∪ {σ_{λ}}. od

od

4. Return Ω, a complete set of mgu’s of T_{1} into T_{2}.

Figure 10: Computing a Complete Set of MGU’s

As noted in Section 6.1, the mgu of a pair of tuples of id-terms, ⟨P_{1}, ..., P_{n}⟩ and ⟨Q_{1}, ..., Q_{n}⟩, coincides with the mgu of the terms f(P_{1}, ..., P_{n}) and f(Q_{1}, ..., Q_{n}), where f is an arbitrary n-ary function symbol. So, we can use any standard unification procedure to unify tuples of id-terms. Given a pair of tuples of id-terms S⃗_{1} and S⃗_{2}, we use UNIF Y (S⃗_{1}, S⃗_{2}) to denote a procedure that returns the mgu of S⃗_{1} and S⃗_{2}, if one exists.

Lemma D.1 The algorithm in Figure 10 correctly finds a complete set of mgu’s of T_{1} into T_{2}.

Proof: Clearly, all elements of Ω are mgu’s of T_{1} into T_{2}, so we will only show that Ω is complete. Consider a unifier θ of T_{1} into T_{2}. By definition, there is a mapping λ ∈ Maps(T_{1}, T_{2}) from atoms(T_{1}) to atoms(T_{2}), such that θ maps every φ in atoms(T_{1}) into the corresponding atom λ(φ) in atoms(T_{2}). Clearly, substitution σ_{λ} constructed in the inner for-loop in Step 3 of the above algorithm is a most general unifier that maps every φ ∈ atoms(T_{1}) to λ(φ) ∈ atoms(T_{2}). So, θ is an instance of σ_{λ}.

Summarizing, we have shown that (1) each element of Ω is an mgu; and (2) if θ is a unifier of T_{1} into T_{2}, then θ is an instance of an element σ_{λ} of Ω. Hence, Ω is a complete set of mgu’s of T_{1} into T_{2}. □

In the worst-case, the algorithm of Figure 10 may yield an exponential number of unifiers, which may happen due to the following two factors:

1. Unification of sets:

This is not a problem with F-logic, but rather a manifestation of the way this world is arranged. Every language that allows the use of sets in any essential way has to put up with such worst-case complexity of unification;

2. Permutation of methods inside F-terms: Since methods may be denoted by nonground id-terms, they can match each other in many different ways. For instance, in unifying P [X → V; Y → W] and P [X′ → V′; Y′ → W′], the method denoted by X can match either X′ or Y′; similarly for Y. Thus, an extra complexity is expected due to the higher-order syntax of F-logic.

The key factor in estimating the complexity of unification in “practical” cases is the number of atoms comprising each term in rule bodies. For, if n_{1} is the number of atoms in T_{1} and n_{2} is the same for T_{2}, then the number of unifiers of T_{1} into T_{2} is bounded by n_{2}^{n_{1}}. Now, to resolve a pair of rules … ← …, T_{1}, … and T_{2} ← …, where T_{1} and T_{2} are data or signature F-terms, we need to unify T_{1} into T_{2} and, therefore, the above parameter n_{1} that denotes the number of atoms in T_{1} is most crucial. However, our experience with F-logic and all the examples in this paper show that this number is usually very small (≤ 2) and so, we believe, combinatorial explosion is unlikely to happen in practice.