Starting a prover project for the semantic web

Hi,

Just wanted to advertise that I have started a
project together with a colleague to build a new
prover system suited for tasks like those we get
in reasoning for semantic web.

Since I have not been in touch with rdf or semantic web
communities (I am a hard-core first-order-theorem-prover
developer with some additional experience both in
verification and collaborative web systems)
I am basically looking for contacts.

The provers I have been working on are built for
full first order predicate logic and decidable
subclasses of these. I am not directly working
with description logic: instead I prefer to treat
description logic, datalog and such as subsets of
full first order for which we create specialised
strategies inside the full first order prover,
sometimes augmented with propositional solvers.

The main tool I have been developing for the last
six years is the automated theorem prover Gandalf
(see http://www.ttu.ee/it/gandalf/). Gandalf
is particularly strong at large problems, decidable
classes and model building (according to the
CASC competition http://www.math.miami.edu/~tptp/CASC/,
probably the best there is for these kinds of tasks).

I have convinced a colleague (who has a lot of successful
experience writing and deploying industrial-strength web-based
financial software) to start working with me on a new
reasoning tool which would be well-suited for both semantic web 
reasoning tasks and writing deployable and scalable
rule-based business logic systems.

The specific goal is to have a reasoning system which
would be usable for building distributed systems in the
somewhat similar manner as people have been using
SQL servers.

The main short-term tasks we have been working
with so far:

-  hack the Gandalf theorem prover, add suitable strategies etc
-  build a layer around Gandalf which would enable one
    to easily call and direct Gandalf from external systems.
-  write a server (similar to SQL servers) for the storage,
    modification and compilation of rule sets, plus
    dispatching queries to the Gandalf subsystem and
    handling the results.

I'd love to get in touch with people actively doing
(or planning to do) implementation work for using
first order provers for semantic web tasks: perhaps
we could coordinate our RD efforts and hopefully work
together to build useful semantic web reasoning
(sub)systems as a result.

Regards,
         Tanel Tammet
         tammet@staff.ttu.ee

Received on Sunday, 10 November 2002 16:37:46 UTC