The conference started today. The first few days are workshops and tutorials. The actual conference comes later.
So, today I attend a tutorial on "Automated Reasoning in First-Order Logic". Professor Andrei Voronkov from the University of Manchester talked us through some of his Vampire theorem-prover (version 8). He's been working on this system for the past 10 years and it is by far the fastest 1st-order logic reasoning system in the world. It wins just about every category in a yearly theorem-proving competition. The competition is often as much as 100 times slower. Vampire devours other provers.
However, for specialized reasoning in OWL, dedicated tableaux algorithm-based reasoners are quicker than Vampire. For now. I learnt that there are many parameters by which Vampire can be tweaked. A small change in the parameters will often allow the prover to answer a problem that was taking 24 hours before in a couple of seconds. However, finding the optimal settings is very much a black-art. No one understand which combination of parameters will give a good result. Andrei himself is pretty good, but he doesn't have the time to investigate all possible things people want to do with Vampire.
Professor Voronkov is taking a sabbatical at Microsoft Research in Seattle for the next year. Microsoft wants to use Vampire to formally verify device drivers. Bad drivers are a frequent cause of Windows crashing, so Microsoft is very interested in translating the code into logic syntax and letting Vampire find the bugs. Intel has been verifying all their chips in a similar fashion after the embarrassing bug in the original Pentium processor that caused it to give the incorrect answer on a few simple division operations.
Relating to my research, I found out that Vampire, unlike the tableaux-based reasoners, doesn't have a problem when classifying large data structures. One major difference between description logic and FOL is that the later is undecidable. The prover can answer "don't know". A description logic reasoner will however always, in theory, be able answer conclusively. In practice it often answers "stack-overflow" when faced with the ontologies I throw at it.
Anyway, Vampire achieves it's slow memory usage by simply discarding inactive clauses it has generated by its resolution process. The most "young and heavy" clauses are going to be processed last anyway, so why not just throw them out? We're likely to find a solution (= empty clause) (= contradiction) before then. I wonder if I can do a similar thing in description logic. I'll loose some completeness, of course.