First-Order Logic with Quotation (FOLQ) on the Semantic Web

Status

EARLY NOTES (NOT EVEN A DRAFT) $Revision: 1.4 $ $Date: 2002/10/02 21:34:53 $

Text by Sandro Hawke. Ideas and work by W3C SWAD. Thanks to Bijan Parsia, Lynn Andrea Stein, Jim Hendler, and many others.

Outline

Introduction

The Semantic Web (Documents expressing relations)
Why Triples? (Simple model for humans, metadata)
Why Logic? (Abstractions; Computers do it well; Documents=Programs)
Why Quotation? (Reasoning about documents; Trust, Belief, Closing the World)

Theory

Extension By External Constraints (RDF Layering) -- the meaning depends on what the terms mean
Reification Vocabularies -- strings, lists, sentences; dangers of RDF inference
Truth Predicates -- how to avoid paradox
Web Reference Predicates -- the simple and the complete
First-Order Axioms -- map FOLQ to FOL; interative web-reference handling

Practice

Document Syntax, Tranlation Tools -- N3, FOL+{} [history], KIF, infix KIF, ...
Inference Tools -- Using Otter, XSB, cwm, CLIPS
Applications -- Meeting Records

Conclusions

or maybe just:

         intro
	 serial syntaxes    [ cover layering HERE ]
	 graph syntax
	 layering axioms
	 inference tools
	 application example

Introduction

To be part of the Semantic Web, a document must convey its content as machine-readable statements of relationships which exist between things. This is an abstract view of knowledge, rooted in formal logic, which is flexible, well-understood by experts, and suitable for processing by computers. Documents like this have an underlying similarity, despite possible differences in surface syntax, which allows software to reason about collections of the documents and their contents.

The basic techniques of processing documents in formal languages have been understood since at least 1970, but they have perhaps not yet really met the Web. Traditionally, reasoners have operated on a specific knowledge base, maintained by a centralized authority. The web has no central authority, and documents are always appearing and disappearing. Reasoning with such a knowledge base presents new challenges.

In our work, we have considered two areas which seem crucial to the function of the Semantic Web: shared naming and reasoning about documents. Shared naming addresses the problem of using logic formulas as messages, considering the degree to which sender and receiver share an interpretation of various vocabulary terms. Reasoning about documents involves putting documents into the domain of discourse (reifying them), so that we can ... ugh.

To date, most Semantic Work seems to use RDF/XML. While we understand the need for a common language, it was never designed to be manipulated by hand. For reading and writing, we need languages that are easier for people to read and write; we've experimented with some of these (primarily an evolving language called N3). In some cases these language appear to have a greater expressive power than RDF, but we'll show how that's a false comparison since RDF itself has a variable expressive power depending on the which vocabulary terms are considered to be part of the language.

older stuff

Abstract

We suggest that RDF's limited expressive power can be extended safely to the level of classical first-order logic by using a combination of reification and a stratified truth predicate. First we formalize RDF in terms of classical logic. Then, we survey prior work on reification vocabularies and suggest a new candidate (called LX), and define it and the truth predicate with axioms. We show how to use a resolution theorem prover (Otter) and a tabled prolog compiler (XSB) to work with reified-and-asserted knowledge on sample problems. Finally, we suggest that adoption of LX reasoners could allow other logics (such as RDFS and OWL) to be trivially deployed for applications needing only moderate performance.

1. Introduction

As a knowledge representation language, RDF has very little expressive power. Without an extension to its vocabulary, an RDF document can do no more than state the values of properties of things. RDF critics have argued that more expressivity is needed [@]. RDF advocates have replied that this is enough because (1) it is all we need for most important applications [@], and (2) more expressive power can be added at a "higher layer" [@].

The mechanism and even the feasibility of adding expressive power has been debated. While the RDFS vocabulary appears to succesfully extend RDF from being a minimalist frame system to being a weak description logic [@], attempts to define a vocabulary for a stronger description logic, DAML+OIL, have run into controversy [@]. In general, the prospect of adding expressive power at higher layers has been brought into question [Patel-Shneider02].

People have already defined RDF vocabularies for logical systems close to classical first-order logic [Berners-Lee00, McDermott01, Hawke01, McDermott02], but they have failed to address precisely how such systems might productively interact with the underlying RDF. It has been suggested that doing so would lead to catastrophic failures due to paradoxes of self-reference, but we believe these problems can be avoided.

@@ talk about classical logic

2. RDF as a Predicate Logic

RDF follows the traditions of semantic networks [@], which are well known to be equalivalent to classical logic or some subset of classical logic [@].

At its simplest, and RDF graph is equivalent to a conjunction of ground binary atomic sentences, but there are few twists:

Some node and arc labels are document scope; these are equivalent to using existentially quantified variables as labels, so we must allow this quantification over entire RDF sentences.
Common inferences, such as used in RDFS, quantify over predicates, which is not a first-order operation, so we'll use a super-predicate to wrap the binary atomic sentences, like rdf(subject, predicate, object).
RDF has several kinds of strings (called "literals" in the RDF literature, but not to be confused with "literals" in automated theorem proving literature, which are possibly-negated atomic formulas), which are immediately known to be pairwise equal or distinct. This is addressed below in section 2.1.
The text of universal-scope labels on RDF nodes and arcs may be available to processing software and should not, in our opinion, simply be discarded or held to be entirely opaque. We suggest that if true opacity were desired, UUIDs would server as far better labels than URIRefs. We make this "microstructure" information available by using a "webDenotation" function, which maps many-to-one from character strings (which are URIRefs according to RDF) to objects in the domain of discourse.

By viewing RDF as a sublanguage of first-order logic, our mechanism for reifying first-order logic (section 3) can be used for reifying RDF graphs.

2.1 RDF Strings

We consider basic strings to be sequences of unicode characters. These can be assembled using four primitive terms: first, rest, nil, and unicode. "unicode" is itself a list of the unicode characters, in code sequence order. @@more details @@unicode versioning

@@@ RDF String also have the is-XML bit, and the language attribute.

3. Vocabularies for Reification

Berners-Lee suggested that first-order formula could be conveyed in RDF with a quoting operator, but did not precisely define a mapping to triples.

McDermott showed that one could describe first-order formulas using RDF triples, and with only a number of triples proportional to the complexity of the formula.

We find one flaw in McDermott's vocabulary design, which prompts us to consider some design decisions.

@@ handling of RDF inferences (spontaneous delabeling, relabing, and merging); distinguishing constants from variables at what level? Flaw in McDermott's.

@@ community of users, "and" vs "conjunction"

@@ binary vs n-ary

@@ in-line (log:implies, or "a and b")

@@ LX binary, Drews, Kif, Tim's ...?

4. Truth Predicates

A truth predicate lets us get from "There is a sentence which says there is a fire in this building" to "There is a fire in this building!". We do it by saying "There is a true sentence which says there is a fire in this building."

But we have to be careful: that same true might be used to say things like: "There is a sentence which says that it, the sentence itself, is not true." This is the classic liar paradox ("This is a lie!"). Is that sentence true? It's a touchy subject.

This is but the simplest paradox of self-reference; there are trickier ones, like Curry's, and many of them have been studied at great length

@@@@ Solutions: kif3, kif98 (truth predicate only at top level), stratification, stratification of negation

5. Application Experience

otter
xsb
translators
axioms
[cwm???]

what apps?

web-lookup of axioms

performance

6. Issues

why not just use java?     composibility, I think.

performance - open-ended badness!

too confusing

not rdf style

web-loop self reference; open world

7. Conclusions

this stuff is great, but can get slow, and is not likely to replace conventional programming any time soon.

Bibliograph

Drew

Peter

MT

M&S

Pat & Drew's old Semantic Networks stuff (AIMA)

RDF M&S revisited: From Reification to Nesting, from Containers to
Lists, from Dialect to pure XML; Conen, Klapsing, Koppen;
http://nestroy.wi-inf.uni-essen.de/rdf/SWWSBook.pdf

AIMA

http://www.xml.com/pub/a/2001/07/25/prologrdf.html
by Bijan Parsia
July 25, 2001

Sandro Hawke
First: 2002-03-29; This: $Id: paper200209.html,v 1.4 2002/10/02 21:34:53 sandro Exp $