Using ACL2 with Semantic Web Data

Status: Withdrawn. was: in preparation for OWL: Experiences and Directions 2006 Athens, Georgia, USA, November 10-11 2006

The first section is an attempt to fit this in one page.

The later sections are the unabridged material.

Dan Connolly, CSAIL Decentralized Information Group, Massachusetts Institute of Technology

RDF, the core Semantic Web technology, is designed to facilitate interoperability between databases and logical systems much like HTML provides interoperability between document management systems.

A Computational Logic for Applicative Common Lisp, ACL2[ACL2] is a logical system with a number of industrial applications in hardware design and reliable software systems.

RDF, OWL, and ACL2

We integrate ACL2 with the Semantic Web as follows:

Symbols
We map URIs to ACL2 by choosing a package with (defpkg "URI") and writing the URI http://www.w3.org/1999/02/22-rdf-syntax-ns#type as the symbol |URI::http://www.w3.org/1999/02/22-rdf-syntax-ns#type|.
Atomic Formulas
The correspondence between sets of triples in RDF and conjuctions in ACL2 is straightforward, but there are a few things to note:
  • Each URI used in an RDF formula becomes a 0-ary function symbol in ACL2. We declare them a la 
    (defstub |URI::http://www.w3.org/2000/01/rdf-schema#Class| () t)
  • While a triple resembles application of a two-place predicate, the semantics of RDF treats the property (fullname, mailbox) more like a constant than a relation symbol. Hence we introduce a holds predicate: (defstub holds (s p o) t)
  • RDF also has existentially quantified variables. We plan to represent these using DEFCHOOSE
Namespaces
The xmlns mechanism in RDF's XML syntax provides short forms a la contact:fullName for longer URIs. We provide a similar mechanism using Common Lisp macros. This allows us to write 
(namespace "ex"
           "http://example/vocab#"
           ("socrates" "Man" "Mortal") )

which is short for a defstub and defmacro for each name in the namespace.

Generalization and Specialization: RDFS
We express the RDFS Entailment Rules as ACL2 axioms; for example, for rdfs9, we write: 
(defaxiom subclass-gen
  (implies (and (holds (rdf-type) x c1)
                (holds (rdfs-subclassof) c1 c2) )
           (holds (rdf-type) x c2) ) )
Equality Reasoning and Ontologies
We are exploring the use of the OWL pD* rules[OWLPD] as ACL2 axioms.
Universal Quantification and Horn Rules
We have implemented a translation from a subset of Notation 3[N3] to ACL2. The translation is intended to inform the standardization effort for rule interchange in the Semantic Web[RIF].

Related Work

Surnia[surnia] is a similar mapping of OWL Full to Otter during the testing phase of the OWL standardization. During the same timeframe, others developed mapping of the OWL DL subset to Vampire[vowl] using classes as unary predicates, rather than a holds predicate.

The Semantic Web is a technology for sharing data, just as the hypertext Web is for sharing documents. RDF is designed to facilitate interoperability between databases and logical systems much like HTML provides interoperability between document management systems.

ACL2[ACL2] is A Computational Logic for Applicative Common Lisp; it is both a programming language in which to model computer systems and a tool to help prove properties of those models. It has a number of industrial applications in hardware design and reliable software systems.

This is a report on experience using ACL2 with the standard Semantic Web technologies, URIs, RDF, RDFS, and OWL; as well as emerging Semantic Web standards for rules and query.

Symbols in the Semantic Web: URIs

The difference between Common Lisp syntax used for symbols in ACL2 and URIs used in the Semantic Web are minor, though not completely trivial. URIs are case-sensitive where Common Lisp symbols are typically not, for one thing. But in a 1996 design note on Web Architecture, Tim Berners-Lee writes:

URIs and the Test of Independent Invention

For example, it would be possible to map all international telephone numbers into URI space very easily, by inventing a new URI "phone:" after which was the phone number. It would in fact also conversely be possible to map URIs into international phone numbers by allocating a special phone number not used by anyone else, perhaps a special country code for URI space, and then converting all URIs into a decimal representation. In that case, both URIs and phone numbers would be universal spaces.

Following that pattern, we map URIs to ACL2 by choosing a package with (defpkg "URI") and writing the URI http://www.w3.org/1999/02/22-rdf-syntax-ns#type as the symbol |URI::http://www.w3.org/1999/02/22-rdf-syntax-ns#type|.

Atomic Formulas: RDF Triples

An RDF document is a conjunction of so-called triples. This is the first example from the RDF primer:

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
             xmlns:contact="http://www.w3.org/2000/10/swap/pim/contact#">

  <contact:Person rdf:about="http://www.w3.org/People/EM/contact#me">
    <contact:fullName>Eric Miller</contact:fullName>
    <contact:mailbox rdf:resource="mailto:em@w3.org"/>
    <contact:personalTitle>Dr.</contact:personalTitle>
  </contact:Person>

</rdf:RDF>

We represent this in ACL2 as:

(and (holds (URI::|http://www.w3.org/1999/02/22-rdf-syntax-ns#type|)
	    (URI::|http://www.w3.org/People/EM/contact#me|)
	    (URI::|http://www.w3.org/2000/10/swap/pim/contact#Person|)
	    )
     (holds (URI::|http://www.w3.org/2000/10/swap/pim/contact#fullName|)
	    (URI::|http://www.w3.org/People/EM/contact#me|)
	    "Eric Miller" )
     (holds (URI::|http://www.w3.org/2000/10/swap/pim/contact#mailbox|)
	    (URI::|http://www.w3.org/People/EM/contact#me|)
	    (URI::|mailto:em@w3.org|)
	    )
     (holds (URI::|http://www.w3.org/2000/10/swap/pim/contact#personalTitle|)
	    (URI::|http://www.w3.org/People/EM/contact#me|)
	    "Dr." )
     )

The correspondence is straightforward, but there are a few things to note:

Namespaces and Macros

Note the xmlns mechanism in RDF's XML syntax, which provides short forms a la contact:fullName for longer URIs. In rdf.lisp, we provide a similar mechanism using macros. This allows us to write

(namespace "ex"
           "http://example/vocab#"
           ("socrates" "Man" "Mortal") )

which is short for a defstub and defmacro for each name in the namespace:

  (defstub URI::|http://example/vocab#socrates| () t)
  (defmacro ex-socrates () '(URI::|http://example/vocab#socrates|) )

Following section 5.1 The RDF Namespace and Vocabulary, we have:

(namespace "rdf"
	   "http://www.w3.org/1999/02/22-rdf-syntax-ns#"
	   (
	    "type"
	    "Property"
	    "XMLLiteral"
	    "List" "first" "rest" "nil"
	    "value"

	    ;; plus a few others
	    ) )

Generalization and Specialization: RDFS

The next layer in the Semantic Web technology stack is RDFS, which provides support for generalization and specialization of classes and properties.

(namespace "rdfs"
	   "http://www.w3.org/2000/01/rdf-schema#"
	   ("domain" "range"
	    "Resource"
	    "Literal" "Datatype"
	    "Class"
	    "subClassOf" "subPropertyOf"
	    "member" "Container" "ContainerMembershipProperty" ; ugh.
	    "comment" "seeAlso" "isDefinedBy"
	    "label"
	    ) )

We can then express the RDFS Entailment Rules as ACL2 axioms; for example, for rdfs9, we write:

(defaxiom subclass-gen
  (implies (and (holds (rdf-type) x c1)
                (holds (rdfs-subclassof) c1 c2) )
           (holds (rdf-type) x c2) ) )

We can then use rdfs-subClassOf to relate Man to the more general Mortal and get ACL2 to verify the classical syllogism:

(namespace "ex"
	   "http://example/vocab#"
	   ("socrates" "Man" "Mortal") )

(defaxiom socrates1
  (holds (rdf-type) (ex-socrates) (ex-Man))
  )
(defaxiom socrates2
  (holds (rdfs-subclassof) (ex-Man) (ex-Mortal)))

(defthm socrates3
  (holds (rdf-type) (ex-socrates) (ex-Mortal))
  :rule-classes nil
  )

Equality Reasoning and Ontologies

OWL adds a number of facilities including support for equality reasoning. For example, the premise of I5.1-Uniform-treatment-of-literal-data-values from the OWL test cases looks something like this in ACL2: 

(exists (g4 g3 )
        (and (holds (URI::|http://example.org/vocab#stateCode|)
                    g3 "KS" )
             (holds (URI::|http://example.org/vocab#population|)
                    g3 "2688418" )
             (holds (URI::|http://www.w3.org/1999/02/22-rdf-syntax-ns#type|)
                    (URI::|http://example.org/vocab#stateCode|)
                    (URI::|http://www.w3.org/2002/07/owl#InverseFunctionalProperty|)
                    )
             (holds (URI::|http://example.org/vocab#stateCode|)
                    g4 "KS" )
             (holds (URI::|http://example.org/vocab#stateBird|)
                    g4 (URI::|http://example.org/vocab#WesternMeadowlark|)
                    )
             )
        )

The details of representing existentials in ACL2 are in progress. See, for example, statecode.lisp.

Meanwhile, in order to get ACL2 to come to the relevant conclusion, we need some axioms about owl:InverseFunctionalProperty.

We are exploring the OWL pD* treatment by ter Horst[OWLPD] by ter Horst, which suggests axioms such as:

(implies (and (holds (URI::|http://www.w3.org/1999/02/22-rdf-syntax-ns#type|)
		     p
		     (URI::|http://www.w3.org/2002/07/owl#InverseFunctionalProperty|)
		     )
	      (holds p u w )
	      (holds p v w )
	      )
	 (holds (URI::|http://www.w3.org/2002/07/owl#sameAs|)
		u v )
	 )

This axiom, combined with the premise of the I5.1 test, should lead ACL2 to consider the conclusion of the I5.1 test a theorem.

Universal Quantification and Horn Rules

The above axiom for owl:InverseFunctionalProperty is actually generated from a rule syntax called Notation 3[N3]: 

# rdfp2
{ ?p a owl:InverseFunctionalProperty.
  ?u ?p ?w.
  ?v ?p ?w.
} => { ?u = ?v }.

Our exploration of interchange between this N3 syntax and ACL2 is intended to inform the standardization effort for rule interchange in the Semantic Web[RIF].

As another example, consider

@forAll :y.

{  :Joe :likes :y } log:implies { :y :madeof :chocolate }.

:Joe :likes :easterEggs .

and when I use that as input thusly:

(forall (y )
        (and (implies (holds (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#likes|)
                             (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#Joe|)
                             y )
                      (holds (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#madeof|)
                             y (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#chocolate|)
                             )
                      )
             (holds (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#likes|)
                    (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#Joe|)
                    (URI::|file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/rules-simple.n3#easterEggs|)
                    )
             )
        )

Related and Future Work

Sandro Hawke did a mapping of OWL to Otter during the testing phase of the OWL standardization. See surnia among a list of OWL implementations. Sean Bechhofer integrated OWL with the Vampire theorem prover in a somewhat similar way.

Source Code

The ACL2 files discussed above are:

Also, n3absyn.py converts between N3, ACL2, MathML, and some RIF design syntaxes. It relies on the development version of SWAP, a Semantic Web platform written in python.

References