Re: Starting a prover project for the semantic web

Welcome to rdf-logic -- your work sounds interesting, hope you'll 
keep us posted.  IN particular, as part of the Working Group process 
for OWL we need to show it can actually be implemented.  The Working 
Group has produced a TEST document that specifies the entailments 
expected in various cases - if your system was tried on these and you 
could provide feedback on either the Tests or the language to 
public-webont-comments@w3.org, that would be really great and help us 
in bringing OWL to a Web recommendation.
  The test cases document is available at
http://www.w3.org/TR/owl-test/
  and as I mentioned, we'd love your feedback on the mailing list above.
  -Jim Hendler


At 11:36 PM +0200 11/10/02, Tanel Tammet wrote:
>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


-- 
Professor James Hendler				  hendler@cs.umd.edu
Director, Semantic Web and Agent Technologies	  301-405-2696
Maryland Information and Network Dynamics Lab.	  301-405-6707 (Fax)
Univ of Maryland, College Park, MD 20742	  240-731-3822 (Cell)
http://www.cs.umd.edu/users/hendler

Received on Thursday, 14 November 2002 09:56:03 UTC