The X-Logic Workplan
Overview
The closest thing we have to a plan, more like a wish list really.
Excuses
Sorry, this is all a bit vague for a workplan, but its better than nothing surely? No chance of milestones, I don't work that way!
The first activity, pre-design, is to devise a way to build an OpenSource website from XML literate scripts.
A bit of philosophy is crucial, not just so that we have a clue what we are doing, but also because this kind of philosophy delivers formal models which are part of the design of X-Logic.
The whole point of X-Logic is inference (interpreted in the broadest possible way). This is what I expect to be doing about proof tools.
X-Logic hangs around semantics. Work on semantics will follow on once some
The Rest
I don't know what this is but I thought I'd mention it so you know that the stuff mentioned here is just the preliminaries!
Site Building
The first activity, pre-design, is to devise a way to build an OpenSource website from XML literate scripts.
OpenSource
Since part of the objective of X-Logic is to provide for delivery of formal specifications over the web, and the design of X-Logic will be partly formal, the X-Logic web site is not just the web site for an opensource project, it is an opensource website. The site build technologies are supposed to be reusable and are part of the X-Logic deliverables.
Stages
The first stage of this is just to support the needs of the "OpenMind" site which will provide philosophical foundations and formal models for X-Logic. This already works up to a point, and I havn't thought much about what else is needed on this front. So I don't have a staged plan for future work in this area, just one objective worth mentioning.
Reusability
The web site process is intended to be reusable, and I intend to re-use it on the OpenBrand.org website. OpenBrand will also have an OpenSource project in it (Open Portal) which will build on top of the X-Logic technologies. So the only next stage in the site building technology which I know about is tidying up the capabilities I curently have so that I can re-use them on the OpenBrand site (and also at RBJones.com).
Keeping Up
However, this doesn't mean the site build technology will be stable. Almost all the other aspects of X-Logic will result in new kinds of things which can be done on the Web and which I will want to demonstrate on the X-Logic web site, so this stuff will be constantly evolving.
Meta-Modelling
A bit of philosophy is crucial, not just so that we have a clue what we are doing, but also because this kind of philosophy delivers formal models which are part of the design of X-Logic.
Stage 1
In the first stage of modelling we create a model in which documents are asserted as true in some language, and, and in which programs transforming documents are asserted to satisfy some specifications couched in terms of the langauges of the documents which they transform. This yeilds a metacalculus in which the inferences performed by programs in various languages can be combined. This calculus is of the same order of expressiveness and complexity as propositional calculi. The modelling will give proof support by embedding, but a dedicated lightwieght meta-inference tool should be easy to implement.
Signatures
The next stage is to allow differentiation of confidence levels by adding digital signatures to the Stage 1 model. This is expected to add little complexity, and to give full control over the trade-off between assurance and functionality.
Models of Semantics
The first two stages of modelling can be accomplished with almost no information about how the semantics of languages is to be defined, but supports only discrete fixed languages. To allow for mixing of languages and for extensible languages we need more sophisticated modelling of semantis, identifying a general generic framework for semantics which supports modular semantic specifications. It is probably necessary also to muddy the distinction between a document and a semantics (kept separate till now).
Inference Tools
The whole point of X-Logic is inference (interpreted in the broadest possible way). This is what I expect to be doing about proof tools.
All Programs Infer
A key feature of X-Logic, which will come out in the earliest formal models, is that all programs do inferences, its not just about that special class of programs which we think of as proof tools. So X-Logic does not major on the implementation of proof tools, or even on the integration of existing proof tools into X-Logic (though both of these figure).
XL-Glue
Sometimes called XL-Glue, sometimes a meta-inference tool. The meta-inference tool is there to sew together arguments from pieces implemented in different languages, and to keep track of the resulting level of confidence (depending on the confidence with which the pieces were demonstrated. The early stages of meta-modelling will provide the basis for a simple meta-inference tool, which should not be greatly impacted by the later stages. So a first XL-Glue prover should follow on fairly rapidly from the first meta-models.
Proof Tool Integration
Apart from a very simple meta-inferrer there is no intention to build proof tools under X-Logic. Integration of existing tools into the framework is more likely. The first one is ProofPower, which is the one best supported (so far as literate scripts are concerned) at present. What integration involves is not so clear at present. The first desideratum is that tools should deliver signed claims about the truth of documents in certain languages, but it is probably that this could be realised by another bit of XL-Glue providing a wrapper which does packages up and signs the results from a proof tool. The next stage of integration would involve proof tools accepting and inferring from signed X-Logic claims.
Semantic Mappings
X-Logic hangs around semantics. Work on semantics will follow on once some
Default XML semantics
One of the earliest activities on the semantic front is likely to be development of a default semantics for XML documents. This will probably turn out to be like a formalisation of the XML infoset, and provides a semantics for XML documents independent of any DTDs, XML-schemas or XL-schemas. As well as allowing certain kinds of reasoning about XML documents without the need for any further work on semantics, it could be used as a staging point for application specific semantic specifications. See below for hints on what this means.
Semantic Domains
It is not intended that any single target be specified for the targets of semantic mappings, but in the initial stages definition of semantics targetted on semantic domains defined in Galactic Set Theory will be explored. Such mappings could provide the basis for proof support in tools such as ProofPower (or other similar tools) by semantic embedding.
Two Embedding Routes
For semantics intended to yield semantic embeddings there are two possible routes which are on the table for investigation. In the first route the definition is written in XSLT and maps to an XML version of GST (built on a more general XML for HOL). In the second route the mapping is written in Higher Order Logic, and maps from the GST model of the XML infoset to the appropriate semantic domains also defined in GST. The difference is analogous to the shallow/deep distinction for semantic embeddings (GST is intended to be a suitable environment for deep embeddings of almost anything).
Extensible Languages
Though all the above is written thinking of discrete languages, ultimately it is essential to come to grips with extensibility. This will require another round of meta-modelling before starting on methods for defining the semantics of extensible languages.

up quick index © RBJ

$Id: workplan.xml,v 1.1.1.1 2000/12/04 17:22:13 rbjones Exp $