zardosht
zardosht

Reputation: 3581

What does soundness of a semantic reasoner mean?

Many articles about semantic reasoner, refer to soundness as a characteristic of the reasoner or a reasoning algorithm. However from definition of soundness from Wikipedia (http://en.wikipedia.org/wiki/Soundness) I understand that soundness is a property of my model and independent from reasoning algorithm that I apply to it. For example the model:

All organisms with wings can fly. 
Penguins have wings.

Leads to the following valid (provable?) but unsound result:

Penguins can fly.

So when I give this model to a for example Tableaux-based algorithm, or the KAON2 reasoner, that are both said to be sound, they would still give me this unsound result. So can you please describe to me what is the soundness exactly? and if it is a characteristic of model or modeling language or reasoning method or just the inference result?

Upvotes: 2

Views: 320

Answers (2)

Michael
Michael

Reputation: 4886

It basically means correct. Sound means the reasoner will return only correct results, that is, results that are either explicit in the knowledge base, or entailed from its contents. Unsound would mean that the reasoner returns a result that is both not explicit in your KB, and not entailed by any axiom(s), ie, an incorrect result.

Complete means it returns all the answers. You can be sound without being complete, that is, returning a subset of all correct answers. This can be desirable in some use cases.

You can also be complete, but unsound; you return all the correct answers, and some incorrect ones as well.

In your example, the result is only unsound to you because you have information that the KB does not, namely, that penguins cannot fly. From the reasoner's point of view, that's a sound result. It cannot confirm the veracity of the facts it's given, it just uses them to entail new ones.

Upvotes: 3

Eric Petroelje
Eric Petroelje

Reputation: 60528

The argument is valid, but one of the premises is not true. Therefore the argument is not sound.

I don't think the reasoner can decide if your premises are true - if it could, then that would be quite revolutionary :)

Upvotes: 1

Related Questions