That's a very good point re SAT/SMT. F* (https://www.fstar-lang.org/) has done truly amazing things by making use of them, and it's great to be able to get sophisticated correctness checks while doing basically non of the work.
I'm going to have to go away and think about how one could effectively leverage this in a data setting, but I'd love to hear ideas.
It doesn't have anything directly to do with SAT but I'd say the #1 deficiency in RDFS and OWL is this.
Somebody might write
:Today :tempF 32.0 .
or
:Today :tempC 0.0 .
The point of RDFS and OWL is not to force people into a straightjacket the way people think it is but rather make it possible to write a rulebox after the fact that merges data together. You might wish you could write
:tempC rdfs:subPropertyOf :tempF .
but you can't, what you really want is to write a rule like
?x :tempC ?y -> ?x :tempF ?y*1.8 + 32.0
but OWL doesn't let you do that. You can do it with SPIN but SPIN never got ratified and so far all the SPIN implementations are simple fixed point iterators and don't take advantage of the large advances that have happened with production rules systems since they fell out of fashion (e.g. systems in the 1980s broke down with 10,000 rules, in 2022 1,000,000 rules is often no problem.)
I'm going to have to go away and think about how one could effectively leverage this in a data setting, but I'd love to hear ideas.