SWRL first-order logic
The folks who brought us RDF, OWL, RuleML, and SWRL,
have now given us a version of first-order logic
called SWRL FOL:
http://www.daml.org/2004/11/fol/proposal
A Proposal for a SWRL Extension to First-Order Logic
Following is an example of "a simple, nonsensical assertion"
in that report expressed in the XML notation for SWRL FOL:
<Assertion owlx:name="Example">
<owlx:Annotation>
<owlx:Label>Example Rule for Expository Purposes</owlx:Label>
</owlx:Annotation>
<Forall>
<ruleml:Var type="Person">x1</ruleml:Var>
<ruleml:Var type="Parent">x2</ruleml:Var>
<ruleml:Var type="Person">x3</ruleml:Var>
<ruleml:Var type="xsd:int">x4</ruleml:Var>
<And>
<swrlx:individualPropertyAtom swrlx:property="hasParent">
<ruleml:Var>x1</ruleml:Var>
<ruleml:Var>x2</ruleml:Var>
</swrlx:individualPropertyAtom>
<swrlx:individualPropertyAtom swrlx:property="hasBrother">
<ruleml:Var>x2</ruleml:Var>
<ruleml:Var>x3</ruleml:Var>
</swrlx:individualPropertyAtom>
<swrlx:datatypePropertyAtom swrlx:property="hasAge">
<ruleml:Var>x2</ruleml:Var>
<ruleml:Var>x4</ruleml:Var>
</swrlx:datatypePropertyAtom>
</And>
</Forall>
</Assertion>
Following is a translation of that assertion into four
other notations for FOL:
1. Controlled English:
For every person x1, parent x2, person x3, integer x4,
the person x1 has the parent x2 as parent,
the parent x2 has the person x3 as brother,
and the parent x2 has the integer x4 as age.
2. Typed predicate calculus, limited to ASCII character set:
(A x1:person)(A x2:parent)(A x3:person)(A x4:integer)
(hasParent(x1,x2) & hasBrother(x2,x3) & hasAge(x2,x4))
3. Knowledge Interchange Format (KIF):
(forall ((?x1 person) (?x2 parent) (?x3 person) (x4 integer))
(and (hasParent ?x1 ?x2) (hasBrother ?x2 ?x3) (hasAge ?x2 ?x4)))
4. Conceptual Graph Interchange Format (CGIF):
[Person: @every*x1] [Parent: @every*x2] [Person: @every*x3]
[Integer: @every*x4] (hasParent ?x1 ?x2) (hasBrother ?x2 ?x3)
(hasAge ?x2 ?x4)
I agree with the authors that the example is nonsensical.
John Sowa