The Automation of Reason
Introduction
My interest here is in the automation of deductive reason, and is mainly philosophical but includes some discussion of high level design.
Leibniz dreamed of a universal language and a calculus of reason which would reduce all problems to numerical computation. Unrealisable in his time, it is still today a dream, but one which (subject to qualifications) advances in mathematics, logic and information technology may have brought within our grasp.
The X-Logic project has two sides. It is Part IV of an "Evolution Rationality and Deduction" book project, and as such provides an informal exposition of an information architecture designed to capture the results of diverse methods of analysis, applicable both to philosophical and to other problem domains. Its other side is formal, and is represented by an open source project hosted on Google code under which formal models of this architecture are to be developed. These models, as well as furthering the philosophical analysis, are intended as an input to a process of formulating standards for some future generation of "The Semantic Web".
The Automation of Reason - Some History
Leibniz dreamed of a universal language and a calculus of reason which would reduce all problems to numerical computation. Unrealisable in his time, it is still today a dream, but one which (subject to qualifications) advances in mathematics, logic and information technology may have brought within our grasp.
Leibniz dreamed of a universal language and a calculus of reason which would reduce all problems to numerical computation. Unrealisable in his time, it is still today a dream, but one which (subject to qualifications) advances in mathematics, logic and information technology may have brought within our grasp.
From Calculators to Global Networks
The calculator which Leibnxiz designed and built was nowhere near adequate for doing anything worthwhile with the calculus ratiocinator which he envisaged. Todays global networks of electronic computers are more like what is needed. It took a long history of innovation to get from the one to the other.
The Logicisation of Analysis
The "calculus", independently invented by Isaac Newton and Leibniz, was the beginning of a new branch of mathematics called "analysis". Analysis developed rapidly over the next hundred years, providing the mathematical techniques necessary for the growth of science and engineering. Success in application made continued development possible despite reservations about the coherence and rigour of the methods which had been adopted. Rigourisation, leading eventually to logicisation began only in the nineteenth century.
The Automation of Analysis
X-Logic
The X-Logic project has two sides. It is Part IV of an "Evolution Rationality and Deduction" book project, and as such provides an informal exposition of an information architecture designed to capture the results of diverse methods of analysis, applicable both to philosophical and to other problem domains. Its other side is formal, and is represented by an open source project hosted on Google code under which formal models of this architecture are to be developed. These models, as well as furthering the philosophical analysis, are intended as an input to a process of formulating standards for some future generation of "The Semantic Web".
Philosophical Preliminaries
X-Logic is the confluence of ideas for the semantic web (from a previous incarnation of the project), with ideas offering a Carneadean resolution of "the problem" of radical scepticism, involving methodological pluralism and a technique which we call "epistemic retreat".
Desiderata
This is an informal statement of requirements for X-Logic.
Formal Models
Some aspects of the architecture are explored using formal models, usually models written in languages supported by ProofPower (HOL or Z or set theory in HOL).
Some earlier ideas about X-Logic (previously at X-Logic.org).

up quick index © RBJ

privacy policy

Created:2005-12-30

$Id: x002.xml,v 1.3 2007/04/25 19:10:22 rbj01 Exp $

V