Frame Logic

Origin. Kifer, Lausen, Wu (1995). Object-oriented knowledge representation. Frames with logic. Methods and inheritance. Foundation for F-logic systems.

Models. Objects with attributes. Class hierarchy. Method definitions. Nonmonotonic inheritance. Combines frames with first-order logic.

Formalism.

Objects and classes: o : c — object o is instance of class c c :: d — class c subclass of d o[m → v] — object o has method m with value v o[m →→ v] — inheritable method

Signatures and data: c[m ⇒ t] — instances of c have m of type t c[m ⇒⇒ t] — inheritable signature o[m → v] — actual data value

Rules: H :- B₁, ..., Bₙ Deductive rules. Logic programming style.

Inheritance: Nonmonotonic: overridable. Multiple inheritance with conflict resolution. ISA hierarchy.

Path expressions: o.m.n — chained access o[m → X][n → Y] — conjunctive

Molecules: Combine facts about one object: o[m₁ → v₁; m₂ → v₂; ... ; mₙ → vₙ]

Example: bob : person. person :: being. person[age ⇒ integer]. bob[age → 30].

Query: ?- X : person[age → Y], Y > 25.

Symbols.

Symbol	Unicode	Name	Meaning
:	U+003A	Colon / Membership	Object is an instance of a class
→	U+2192	Rightwards arrow / Data	Method of an object has this value
⇒	U+21D2	Double arrow / Signature	Declares the type of a method on a class
[	U+005B	Left square bracket	Opens a molecule of facts about one object
]	U+005D	Right square bracket	Closes a molecule
;	U+003B	Semicolon	Separates the components of a molecule
,	U+002C	Comma	Conjunction in a rule body or query
.	U+002E	Full stop	Path expression, chaining method access
>	U+003E	Greater-than sign	Comparison in a query
::	—	Subclass	Class is a subclass of another
→→	—	Inheritable data	Value inherited by instances
⇒⇒	—	Inheritable signature	Type declaration inherited by subclasses
:-	—	Rule arrow	Head holds if body holds
?-	—	Query prefix	Goal to be answered
o	—	Object	Individual in the domain
c	—	Class	Object used as a class
m	—	Method	Attribute or function on an object
v	—	Value	Result of a method

Metatheory. Kifer, Lausen and Wu (1995) gave F-logic a model-theoretic semantics in which objects, classes and methods all inhabit a single domain, and proved a resolution-based proof theory sound and complete for the monotonic fragment. That fragment is a syntactic variant of classical first-order logic with equality — the frame notation adds convenience rather than expressive power — so entailment there is recursively enumerable and undecidable. Variables may stand in class and method positions, which reads as second order but is given a first-order semantics by reification, as in HiLog. The subclass relation is axiomatized as a partial order, so a cycle in :: identifies the classes rather than being rejected. The difficulty is concentrated in the nonmonotonic part: the original inheritance semantics behaved badly when rules could themselves derive class membership, and Yang and Kifer (2003) replaced it with an account built on the well-founded semantics, in which inheritance and deduction are computed by one fixpoint instead of inheritance being a preprocessing step. Function-free programs inherit Datalog's polynomial data complexity.

Applies to. Deductive databases. Knowledge bases. Semantic Web (Flora-2). Object-oriented reasoning. Ontologies.

Limitations. Inheritance is nonmonotonic and entangled with deduction: a rule may derive the class membership that decides what is inherited, and the inherited value may in turn feed the rule, so the two cannot be separated into phases and the joint fixpoint can leave a value undefined rather than settling it. Conflicting multiple inheritance is not adjudicated by the logic — where two superclasses supply different values for the same method, the semantics declines to inherit, and any preference must be encoded by hand. The monotonic core is first-order logic with equality, so entailment is undecidable; the tractable fragments come from excluding function symbols, not from anything the frame syntax contributes. Signatures declare intended types but are not enforced: a violation is an ordinary derivable inconsistency, not a rejected input. There are no class constructors of the description-logic kind, so disjointness, cardinality bounds and negated classes have to be simulated by rules with no guarantee that the simulation is complete.