[Biojava-dev] reasoning

[Matthew Pocock]

Hi,

I have checked in new ontology code. It doesn't crash, but doesn't 
entirly work yet. Please add sablecc 3.* to your ant/lib directory to 
enable the new ontology parser code to be generated.

Good points:

* much more sane core ontology with a workable type-system - strictly 
typed higher-order predicate logic!

* a fairly nice text format for writing things down - I have yet to find 
anything that can't be represented

* the reasoner can execute proofs that require variable substitution e.g.

  axiom: instance_of(_x, ANY)
  proposition: instance_of(dog, ANY)
  proof: instance_of(_x, ANY)[_x = dog]

  proposition: sub_type_of(_x, mammal)
  proof: sub_type_of(_x, mammal)[_x = dog] ; axiom(dog, mammal)

Bad points:

* I haven't been able to get it to find proofs for things that require 
an inference step without manually pruning the search space e.g.

  axiom: sub_type_of(dog, mammal)
  axiom: sub_type_of(mammal, animal)
  axiom: implies( and(sub_type_of(_x, _y), sub_type_of(_y, _z)),
                             sub_type_of(_x, _z))

  proposition: sub_type_of(dog, animal)

Well, it can do this, but it gets stuck in an infinite recursion before 
it gets arround to using the right variable substitutions.

* It runs slowly - there is loads of scope for naive performance tuning, 
and once inference works propperly, it should be generating it's own 
interpreter in bytecode, but not today.

The code is in CVS, so if you are interested in any of this then please 
get involved. I am wondering which bits will survive - certainly, some 
of the code needs gutting for functional and aesthetic reasons. However, 
I'm not even sure if this is the correct approach.

Matthew