Does the Prolog symbol :- mean Implies, Entails or Proves?

Question

In Prolog we can write very simple programs like this:

mammal(dog).
mammal(cat).

animal(X) :- mammal(X).

The last line uses the symbol :- which informally lets us read the final fact as: if X is a mammal then it is also an animal.

I am beginning to learn Prolog and trying to establish which of the following is meant by the symbol :-

• Implies (⇒)
• Entails (⊨)
• Provable (⊢)

In addition, I am not clear on the difference between these three. I am trying to read threads like this one, but the discussion is at a level above my capability, https://math.stackexchange.com/questions/286077/implies-rightarrow-vs-entails-models-vs-provable-vdash.

My thinking:

• Prolog works by pattern-matching symbols (unification and search) and so we might be tempted to say the symbol :- means 'syntactic entailment'. However this would only be true of queries that are proven to be true as a result of that syntactic process.
• The symbol :- is used to create a database of facts, and therefore is semantic in nature. That means it could be one of Implies (⇒) or Entails (⊨) but I don't know which.

Hintz

Answer 1

Neither. Or, rather if at all, then it's the implication. The other symbols are above, that is meta-language. The Mathematics Stack Exchange answers explain this quite nicely.

So why :- is not that much of an implication, consider:

p :- p.

In logic, both truth values make this a valid sentence. But in Prolog we stick to the minimal model. So p is false. Prolog uses a subset of predicate logic such that there actually is only one minimal model. And worse, Prolog's actual default execution strategy makes this an infinite loop.

Nevertheless, the most intuitive way to read LHS :- RHS. is to see it as a way to generate new knowledge. Provided RHS is true it follows that also LHS is true. This way one avoids all the paradoxa related to implication.

The direction right-to-left is a bit counter intuitive. This direction is motivated by Prolog's actual execution strategy (which goes left-to-right in this representation).

Thoraco

Answer 2

:- is usually read as if, so something like:

a :- b, c .

reads as

| a is true if b and c are true.

In formal logic, the above would be written as

| a ← b ∧ c

Or

| b and c imply a

Inmate

Why the | before some lines? If it is separate sections then why not --- – Cubbyhole

hi Nicholas, are you able to explain the different terminology; imply vs entail vs proves ? – Hintz

@PrologByExample Entailment is a higher-level form of implication: If B is entailed by A, then it logically follows A, for all models where A is true. "All models" is the distinction. – Lanthanum