A Topography for AI

"A" topography, not "the" topography. "Artificial" not "natural". A proposed architecture rather than a theory.

In human intelligence logic may play no large role. It is a higher level feature rather than a foundation on which intelligence is laid.

Computers, intelligent or otherwise, are much better at arithmetic than human beings. An intelligent computer may have an entirely different balance of mental aptitudes than a human, just as power tools and heavy machinery perform some kinds of physical tasks much better than humans and other tasks less well.

The white and blue region represents the purest and perhaps most easily realisable intelligence. Its subregion, "engineering logic", is mere brute force, implemented mainly by coding up in the right framework techniques already known. This region represents also the extent of functionality which we can hope to achieve with high levels of assurance and reliability. In this region our software might be infallible.

As we step out into the lush green of real life problems, our language becomes less clear, our criteria less precise, our methods less reliable and intelligence less trustworthy.

Topography for AI
Logic
At the core of our architecture is a formal logical "inference engine". A meld of compiler and proof technologies giving fast computation of logical truths rather than data values.
Formal Maths
Built on the logical core, the main body of applicable mathematics with just as much pure maths as helps to oil the wheels.
Engineering Logic
Beyond the theories into the applications, targeted at engineering applications. As much automated problem solving as we know how implement within the limits of energetic engineering rather than AI breakthroughs.
Intelligent Logic
We seek an environment in which, in an environment full of hard graft algorithmic problem solving, intelligent capabilities can evolve and emerge. Not by natural selection. Faster than that.
Judgement
Beyond logic and mathematics, beyond deduction, into empirical science. Judgement is called for here, and trusting machines may not be appropriate.
Values
One step further, from objective science to subjective values. This is part of what human intelligence is about, but do we need it in AI?
Emotions
One step further beyond the limits of machinery.

Logic
At the core of our architecture is a formal logical "inference engine". A meld of compiler and proof technologies giving fast computation of logical truths rather than data values.
Features
Classical set theory formalised in a polymorphic higher order logic based on the typed lambda calculus.
Rationale
Set theory gives clean semantics with logical strength, polymorphic higher order logic enables all operators to be in the domain of discourse, building on the lambda calculus gives open-ended uniform support for variable binding constructs.
Pedigree
Cantor, Zermelo and Fraenkel were the main sources of the set theory, Frege, Russell and Church contributed the predicate calculus, the type theory, and its realisation throught the lambda calculus. Robin Milner contributed the polymorphism, Mike Gordon first applied it to Church's logic.
Implementation
to adopt the LCF paradigm, with some further innovations, the most radical being the incorporation of a programming language in the logical kernel.

Formal Maths
Built on the logical core, the main body of applicable mathematics with just as much pure maths as helps to oil the wheels.
Background and Motivation
Leibniz dreamed of mechanising reason and mathematics but didn't have the wherewithall. Lots of people still want to do it, and think logic, computers and a bit of graft will do the trick.
Formal Foundations
This whole enterprise depends upon the fact that mathematics can be reduced to logic. So you need to know what a formal logical foundation system is.
Developing Formal Maths
A first goal is to be able to productively develop mathematical theories, in collusion with computers, with all theorems and proofs formal and machine checked.
Applying Formal Maths
A more ambitious (and maybe more profitable) goal is to exploit the formal methods to get computers which are good at applied mathematics.

Engineering Logic
Beyond the theories into the applications, targeted at engineering applications. As much automated problem solving as we know how implement within the limits of energetic engineering rather than AI breakthroughs.

Intelligent Logic
We seek an environment in which, in an environment full of hard graft algorithmic problem solving, intelligent capabilities can evolve and emerge. Not by natural selection. Faster than that.

Judgement
Beyond logic and mathematics, beyond deduction, into empirical science. Judgement is called for here, and trusting machines may not be appropriate.

Values
One step further, from objective science to subjective values. This is part of what human intelligence is about, but do we need it in AI?

Emotions:

One step further beyond the limits of machinery.


UP HOME © RBJ created 1996/5/10 modified 1998/8/28