I am curious about what people here consider good terminology. Suppose we have the program:
human(socrates).
human(plato).
mortal(X):-human(X).
From my perspective i would be inclined to say that mortal(socrates) “is entailed”, “is provable”, or “holds”. I like “true” less because i (naively) interpret this as true in the sense of corresponding to states of affairs (i know that in Prolog true simply means “provable”). I think that “holds” is nice and short.
Cheers/Jean-Christophe
To sidestep the problem completely, when I talk (to myself) about Prolog programs that could be executed on a computer, I prefer the most operational vocabulary possible. I would say things like:
The query
?- mortal(socrates).succeeds.
The opposite is “The query fails”.
I understand that this view is a bit extremist but has helped me avoid thinking about what to say (to myself).
@Boris thanks for the tip. “Holds” and “entailed” have a more logical flavour, which i like, but it is strange to say things like writeln(socrates) is provable 
Is this free? I thought it required a paid subscription.
If it is free I plan to add it to Useful Prolog references
As far as I know, I haven’t paid for it, nor been asked for payment. (Although maybe I’m “grandfathered” in …)
Does that mean that I subscribe to the statement:
“Entails” is equivalent to “derives from”.
?
I browsed around the newsletter a little bit but I didn’t easily find a good explanation of the logo and eventually gave up.
My original answer above could be interpreted as:
I lack the formal education to deal with such terminology. Instead, I use terminology that I intuitively understand, based on my personal experience with a concrete Prolog implementation.
I understood about 50% of the difference between semantic entailment and syntactic entailment by reading this. Maybe i have to take a philosophy course at my uni 
If i understand this correctly, Prolog returns anything that is syntactically entailed as well semantically entailed?
Interesting. For me one of the fascinating things with Prolog is the intersection between logic and programming.
Since Hornclauses are a fragment of FOL, it also holds for pure Prolog.
Shouldn’t this be the opposite?
Horn clauses are a fragment, so they are pretty certain to not derive everything that is true in a Model (to speak not even about a conclusion being unreachable for practical reasons). Just let them be “don’t know” (or “pseudo-false” under Negation-as-Failure, what I like to call “no evidence for”)
(Completeness is overrated anyway. Who wants to derive everything that is considered true? What is important is soundness: Do not label statements as true using a proof mechanism when they are aren’t true in the model. That would be bad!)
Here is a good reference:
https://plato.stanford.edu/entries/reasoning-automated/
Soundness and completeness are two (metatheoretical) properties of a calculus that are particularly important for automated deduction. Soundness states that the rules of the calculus are truth-preserving. For a direct calculus this means that if Γ ⊢ α then Γ ⊨ α. For indirect calculi, soundness means that if Γ∪{~α} ⊢ ⊥ then Γ ⊨ α. Completeness in a direct calculus states that if Γ ⊨ α then Γ ⊢ α. For indirect calculi, the completeness property is expressed in terms of refutations since one establishes that Γ ⊨ α by showing the existence of a proof, not of α from Γ, but of ⊥ from Γ∪{~α}. Thus, an indirect calculus is refutation complete if Γ ⊨ α implies Γ∪{~α} ⊢ ⊥. Of the two properties, soundness is the most desirable. An incomplete calculus indicates that there are entailment relations that cannot be established within the calculus. For an automated reasoning program this means, informally, that there are true statements that the program cannot prove. Incompleteness may be an unfortunate affair but lack of soundness is a truly problematic situation since an unsound reasoning program would be able to generate false conclusions from perfectly true information.
And a bit further:
Last but not least, in order to improve their efficiency, many implementations of Prolog do not implement unification fully and bypass a time-consuming yet critical test—the so-called occurs-check —responsible for checking the suitability of the unifiers being computed. This results in an unsound calculus and may cause a goal to be entailed by a Prolog program (from a computational point of view) when in fact it should not (from a logical point of view).
There are variations of Prolog intended to extend its scope. By implementing a model elimination procedure, the Prolog Technology Theorem Prover (PTTP) (Stickel 1992) extends Prolog into full first-order logic. The implementation achieves both soundness and completeness. Moving beyond first-order logic, λProlog (Miller & Nadathur 1988) bases the language on higher-order constructive logic.
Thanks for the tip!
/JC
if T ⊆ Horn_1, if s ∈ Horn_2, then if T ⊧ s then T ⊢ s.
If this is in Prolog and s is a Horn goal, then what is entailed by T should be the negation of s, no? So this should be:
if T ⊆ Horn_1, if s ∈ Horn_2, then if T ⊧ ¬s then T ∪ s ⊢ ⊥ .
Else I’m a bit confused.
Edit: how do you get syntax highlighting in comments that aren’t obviously Prolog?
6 posts were split to a new topic: How do you get syntax highlighting in comments that aren’t obviously Prolog?
Thanks. I was confused because I thought you were talking about Prolog. To be honest though it took me a while to get my head around refutation by resolution and now I can’t really think in terms of classical logic. It looks all wrong to me, that a conjunction of negative literals is entailed by a definite program.
Thank you Eric. I do have a question, though only out of curiosity and not out of any specific need to do something particular. On github, if I want to highlight a bit of code as Prolog I use a backtick fence and add “prolog” after the first three backticks, like this:
```prolog
% my prolog code here
```
I’m guessing that on discourse like this forum you can choose a default language for code blocks so that syntax highlighting for Prolog is automatically applied to all code blocks. But, is there a way to change the syntax highlighting to another language, e.g. by doing something like:
def my_func(bla):
stuff(bla)
Edit: oh. I guess it does work. Sorry for using the comments as a sandbox…