[imglorp]

I was just pondering if the Prolog universal quantifier would be applicable to reasoning about Cyc frames. Does your comment imply it's not?

[nl]

I'm somewhat familiar with Cyc but I'd never heard of this development of "micro-theories". It makes perfect sense though - to generalize hugely structured ontologies break as soon as the second person tries to use them or they are used on a slightly different domain.

Anyway, Prolog should be suitable for reasoning over them, but it is only grounded in the "micro-theory" part.