F-Logic Examples Related to RIF Use Case 2.7 for Testing the Condition Language Proposals

Editors: Adrian Giurca, Gerd Wagner (REWERSE Working Group I1)
Date: 01-Nov-2006

Consider the following F-Logic facts and rules:

R1. man::person.                                 // a man is a person
R2. person[father=>man].                         // the father of a person is a man
R3. person[ancestor=>person].                    // an ancestor of a person is a person
R4. man[son@(woman)=>>person].                   // a son of a man and a woman is a person
R5. isaac[father->abraham].                      // the father of isaac is abraham
R6. isaac[mother->sarah:woman].                  // the mother of isaac is sarah (who is a woman)
R7. abraham:man[son@(hagar:woman)->>ishmael].    // ishmael is a son of abraham (who is a man) 
                                                    and hagar (who is a woman)
// A person Y is an ancestor of a person X IF the father of X is a man Z that has Y as an ancestor
R8. X:person[ancestor->>Y:person] <- X:person[father->Z:man] AND Z:person[ancestor->>Y:person].

R1 to R4 are vocabulary facts about

• the classes man and person
• the properties father and ancestor
• the user-defined function/operation son@

Such vocabulary facts are called "signature facts" in F-Logic and "class axioms" resp. "property axioms" in OWL.

R5 to R7 are ordinary (ground) facts about Isaac and Abraham. A complex fact such as R7 is called "molecule" in F-Logic. Notice that F-Logic encodes the cardinality of the value of a property, using the symbol ->> for multivalued properties.

Observations

1. An expressive rule language such as F-Logic accommodates vocabulary facts in addition to rules and ordinary facts.
2. F-Logic rule conditions are based on the vocabulary elements classes, properties and operations (called "methods").
3. F-Logic does not require but allows typing information in rules.
4. F-Logic has three kinds of atoms:
   1. classification atoms such as Z:man
   2. property atoms such as isaac[father->abraham]
   3. object description atoms, such as X:person[father->Z:man], that conjunctively combine several classification atoms and property atoms

An Attempt to Go from F-Logic to Basis:Positive Conditions and back

According with the Basis: Positive Conditions a translator may translate the facts R1 to R7 from F-Logic to RIF as follows:

R1. person(man)
R2. father( person, man)
R3. ancestor( person person)
R4. son( man woman person)
R5. father( isaac abraham)
R6. mother( isaac woman(sarah))
R7. son( man(abraham) woman(hagar) ishmael)

The condition of rule R8 translates into

And( father( person(?X) man(?Z)) ancestor(person(?X) person(?Y)))

This attempt to translate from RIF to F-Logic raises the following questions:

1. Is ancestor( person person) an F-Logic signature fact (corresponding to an OWL property axiom) or is it an ordinary ground atom?
2. Is person(man) an ordinary ground atom or is it a generalization vocabulary fact (corresponding to an OWL subclassOf axiom)?
3. Is son( man(abraham) woman(hagar) ishmael) an F-Logic molecule or is it an ordinary ground atom with function terms as arguments?

Observations

• All typing information from the F-Logic sources is discarded in the translation. Basis:Positive Conditions do not offer the typing information needed.
• All kinds of atoms from F-Logic are translated into the standard atom construct such that it's impossible to reconstruct them when translasting back to F-Logic. We are not able to encode the F-Logic atoms in a loss-free manner using the proposed syntax.
• The syntax of Basic: Positive Conditions is too poor for allowing a loss-free F-Logic-to-RIF-to-F-Logic translation.

Going from F-Logic to REWERSE:Positive Conditions and back

Following the REWERSE proposal these F-Logic facts and rules translate into vocabulary facts, ordinary facts and rules. The F-Logic facts R1-R4) translate into the following vocabulary facts:

// vocabulary facts
Class( person)
Class( man superClass(person))
ReferenceProperty( father domain(person) range(man))
ReferenceProperty( ancestor domain(person) range(person))
ObjectOperation( son contextType(man) argType(woman) returnType(person))

The F-Logic facts R5 and R6 translate either into reference property atoms:

ReferencePropertyAtom( father OName(isaac) OName(abraham))
ReferencePropertyAtom( mother OName(isaac) OName(sarah woman))

or, alternatively, into corresponding equality atoms:

ReferencePropertyFTerm( father OName(isaac)) = OName(abraham) 
ReferencePropertyFTerm( mother OName(isaac)) = OName(sarah woman) 

Notice that properties can be used both as predicates and as functions.

The F-Logic fact R7 is translated into the equality atom:

ObjectOperationTerm( son contextArg(OName(abraham man)) argument(OName(hagar woman))) = OName( ishmael)

Finally the condition of rule R8 is translated into

Conjunction( ReferencePropertyAtom( father OVar(X person) OVar(Z man))
             ReferencePropertyAtom( ancestor OVar(X person) OVar(Y person)))

Observations

• The mapping described here is reversible. All F-Logic terms and atoms can be faithfully encoded and translated back into F-Logic without loss.
• F-Logic does not distinguish between object types (classes) and dataypes.
• In the REWERSE proposal function terms and atoms conform with the Multisorted Extensions of the RIF Nucleus regarding well-formed sorted function terms and well formed atomic formulas.
• We see the open issue whether or not it is preferable for RIF to "display" the object-or-datavalue category of a term in its syntax? It seems that displaying this makes RIF processing easier for translators and other RIF-enabled tools at the cost of a more loaded syntax. Displaying supports the RIF goals "Low cost of implementation" and "Widescale adoption".