if I would support it or not.

I can understand the ideas behind an axiomatization of a formal theory.
How rigorous would this method be?

What kinds of inference would it support?

The highest levels of an ontology like Cyc are useful in static 
'syntactic' level constraints on relation signatures, etc.

What would the highest levels of this kind of ontology provide for
computation?

I assume we are still talking about using this as an information
source to a computer program, not a human, right?

How many