The X-Logic.org Directory Structure
Overview
Since there are many ways of navigating the X-Logic site, it can sometimes be hard to find things. This document heads a comprehensive hierarchy which follows the directory structure, which will normally reach everything on the site.
The X-Logic project aims to build generic (i.e. not specific to particular languages or logics) support for deductive inference, with an emphasis on integration with the XML standards.
Formal analytic philosophy using X-Logic, rationality and deduction, X-Logic foundations.
This provides information about ProofPower and the various formal theories developed at X-Logic.org using ProofPower.
This provides information about ProofPower and the various formal theories developed at X-Logic.org using ProofPower.
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Some documents whose directories don't yet have an index.
directory arch
The X-Logic project aims to build generic (i.e. not specific to particular languages or logics) support for deductive inference, with an emphasis on integration with the XML standards.
Introduction
The ultimate content of X-Logic remains at this stage quite open. Nevertheless we have available a prospectus, some preliminary work on philosophical principles, a crude workplan and a first (pre-design!) alpha release.
The OpenMind web site is a testbed for X-Logic technologies and the source of philosophical foundations and high-level formal models for X-Logic.
An XML based framework supporting reasoning in the "semantic web". Generic support for defining the semantics of languages and for sound deductive reasoning in a multi-lingual context.
The closest thing we have to a plan, more like a wish list really.
This is just a few notes to explain what the currently available releases of X-Logic are.
The directory tree of X-Logic.org giving full access to work in progress.
directory OpenMind
Formal analytic philosophy using X-Logic, rationality and deduction, X-Logic foundations.
Introduction
OpenMind applies formal methods and tools to analytic philosophical problems, explores the relationship between logic and rationality, and provides both applications of and foundations for X-Logic.
To underpin an understanding of Rationality, and as a philosophical foundations for The Semantic Web, we propose develop a new "Theory of Knowledge".
Foundation systems for formal analysis play the same role as logical foundations for mathematics but are aimed at a broader range of applications.
directory pp
This provides information about ProofPower and the various formal theories developed at X-Logic.org using ProofPower.
ProofPower and its Logic
Links to some of the theories which come with ProofPower, with brief descriptions. These are the ones above "basic-hol" which is the point at which OpenMind hangs off the tree.
This document contains extra sml procedures for use with ProofPower to support the methods adopted at X-Logic.org.
The formalisation of ZFC in ProofPower HOL and its applications.
Galactic Set Theory and some applications.
directory isabelle
This provides information about ProofPower and the various formal theories developed at X-Logic.org using ProofPower.
Isabelle and its logics
Isabelle is a specification and proof development and checking tool developed by Larry Paulson and others initially at the University of Cambridge. It is an intellectual descendent of Edinburgh LCF. It is a generic proof tool, supporting multiple object logics, and provides strong interactive proof support and an extensive library of well developed object languages and applications.
Theory of Knowledge in Isabelle.
directory sml
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Introduction
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Two datatypes for representing XML documents (Fat and Lean) and a function for throwing away the fat.
Procedures for invoking the fxp XML parser to create a data structure (parse tree) for further processing.
Procedures for driving collections of "hooks" from fat or lean datatype representations of XML documents, primarily intended to support writing XML documents to files.
Wrappers for the Unicode decode and encode facilities provided in the fxp parser library to package these in ways which are convenient for X-Logic.
Singatures for state and exception monads, and an input stream monad, with an implementation of an input stream monad with exception handling.
Arrows which can be constructed from Monads using a Kleisli functor.
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Miscellaneous Documents
Some documents whose directories don't yet have an index.
A schema for the XML namespace used for the X-Logic site.

up quick index © RBJ

$Id: directories.xml,v 1.1.1.1 2000/12/04 17:24:46 rbjones Exp $