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 :slight_smile:

In other words, @Boris subscribes to the logo of the Association for Logic Programming newsletter. [image]

[image] peter.ludemann: Association for Logic Programming newsletter. Is this free? I thought it required a paid subscription. If it is free I plan to add it to Useful Prolog references

[image] EricGT: Is this free? I thought it required a paid subscription. As far as I know, I haven’t paid for it, nor been asked for payment. (Although maybe I’m “grandfathered” in …)

[image] peter.ludemann: In other words, @Boris subscribes to the logo of the Association for Logic Programming newsletter. 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 :smile:

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.

Terminology: "true", "entailed", "provable", "holds"

General

Topic		Replies	Views
Prolog: Declarative, Procedural vs. Imperative readings / languages Discussion discussion	8	1737	August 17, 2021
Sets of rules as conjunctions and/or disjunctions General	42	681	August 16, 2026
What is meant by "meta-level" in logic programming? General	16	521	August 24, 2024
Is the definition of "predicate" correct in the Glossary of Terms? General	34	3092	September 30, 2021
Hillel Wayne: "My Gripes with Prolog" General discussion	11	523	February 3, 2026

Terminology: "true", "entailed", "provable", "holds"

Related topics