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?