LX is a small family of languages and language elements which outline the space between RDF and full, classical, first-order logic (FOL). In addition to formalizing RDF and FOL, LX formalizes their intersection and union, both as traditional character-sequence languages and as defined vocabulary terms which can be mixed just as other vocabulary terms are mixed in RDF to provide extensibility.
This work defines a separation of RDF into "primordial" elements which are shared with FOL and are probably more fundamental to Semantic Web languages and "chunky" elements which can, in principle, be added at a higher layer. (These whimsical names are intended to be distinctive and vaguely evocative while not too constraining. Primordial LX is a foundational language, but not necessarily the only one, as a name like "Layer 0" might suggest.)
More importantly, this work demonstrates that FOL ("vanilla") can be effectively layered on top of either primordial LX or chunky LX, and thus on RDF/XML. Doing so provides a language for FOL on the Semantic Web which improves on earlier designs.
The layering approach in Vanilla involves quotation, reification, and self-reference. As such, care must be taken to keep the system from being inherently inconsistent; we have taken an approach of partially segregating paradoxical sentences from true and false ones such that we obtain the necessary functionality in a sound system.
Although much effort in developing LX has been conceptual, there is associated software for language conversion and for encapsulating existing reasoners as LX reasoners.
There are two styles of applying LX: logic and metalogic. The logic applications are unsurprising: access control, database views and constraints, policies and preferences, ontology mapping, service coordination and planning, taxonomy, etc. These areas are sometimes better served by logics less expressive than FOL, such as RDFS or OWL. The less-expressive lanuages can be easier to understand and generally come with performance guarantees which are impossible with FOL. But sometimes FOL is necessary, sometimes it is more convenient, and often the performance costs are acceptable. LX provides FOL on the Semantic Web.
LX can also be used as a metalogic, defining the characteristics of other languages in a form usable by both humans and machines. An axiomatization of OWL, for instance, can help people understand its semantics. That same axiomatization in LX allows FOL reasoners to provide OWL inference. This approach may not make sense of OWL, which is expected to be standardized and widely implemented, but other experimental logics, if axiomatized in LX, can be used by LX reasoners on the Semantic Web without any additional software deployment.
In Progress. The paper is farther along.
The documents build on each other in this order:
Try our CVS Repository.
LX development work is being done as part of the MIT/LCS DAML Project under the MIT/AFRL cooperative agreement number F30602- 00-2-0593. This work is not on the W3C recommendation track and is not the product of a W3C working group or interest group.
First: 2002/08/20; This: $Date: 2002/11/13 21:52:36 $