Prolog Legend

loves(X,X).
  Everything loves itself.
  All variables are universally quantified 

loves(X,Y).
  Everything loves everything else including itself.

Special predicate 'diff'


~diff(X,X).
  Unique names.. This says that all things named the same are the same.

diff(X,X). diff(X,Y). ~diff(X,Y).
  None of these can be asserted 

same(X,Y):- ~diff(X,Y).
  Everything is the same unless known to be differnt and and diff/2 is ok in this context (this would be a logically absurd though)

~same(X,Y):- diff(X,Y).
   Nothing is same when known to be different.  (This is a good assertion)

Impossiblity operator  ~ 

~loves(X,Y).
   Nothing can love anything else or even itself
   Basically ~ effects the values of X and Y.. not the 'loves'

~loves(X,Y):-diff(X,Y).
   Nothing can love anything else.
   diff/2 makes sure this statement says nothing about not loving itself.

~loves(X,X).
     Nothing can love itself

~loves(X,Y):-diff(X,Y). ~loves(X,X).
   Nothing can love anything else or even itself Equivanent to ~loves(X,Y).

~A.  
   Is a negation by logical deduction and therefore no unifiable bindings against A which are true.
   In the consequent or fact base: the sentence A will add to that in which is known to not be true

Weakness predicates

true(A):- A, not(~A).
false(A):- ~A,not(A).
unsound(A):- A , ~A.
unknown(A):- not(A),not(~A).

consistent(A):- A ; not(~A).
unproveable(A):- ~A ; not(A).
known(A):- A ; ~A.
sound(A):- not(A) ; not(~A).

complete(A):- known(A), sound(A).


Entailment operator :- 

a(X,Y):- ~b(X).
   a(X,Y) unifies all possible requests that X is known impossible in b(X). 

~a(X,Y):- b(X).
   there is no a(X,Y) that X is known in b(X).

Starting with a 3 literal example

parentOf(P,C)  <=>  ( motherOf(P,C) V fatherOf(P,C) )
     All parents are mother or fathers.  It is a complete partitioning of parent

• Modus Tolens Entailment Rules in Prolog
  1) ~motherOf(P,C) :- ~parentOf(P,C).
  % disproved P is the mother of C when disproved P is the parent of C
  2) ~fatherOf(P,C) :- ~parentOf(P,C).
  % disproved P is the father of C when disproved P is the parent of C
  3) ~parentOf(P,C) :- ~fatherOf(P,C) , ~motherOf(P,C).
  % disproved P is parent of C when disproved that P is mother of C and disproved that P is father of C
• Modus Ponens Entailment Rules in Prolog
  4) motherOf(P,C) :- parentOf(P,C) , ~fatherOf(P,C). 
  % proved  P is the mother of C when proved P is the parent of C and disproved P as the father of C
  5)  fatherOf(P,C) :- parentOf(P,C) , ~motherOf(P,C).
  % proved  P is the father of C if proved P when the parent of C and disproved P as the father of C
  
• Consistency Rules
  6)  parentOf(P,C) :- motherOf(P,C),  not(fatherOf(P,C)).
  % proved  P is the parent of C when proved P is the mother of C and unkown that P is the father of C
  7)  parentOf(P,C) :- fatherOf(P,C), not(motherOf(P,C)).
  % proved  P is the parent of C when proved P is the father of C and unkown that P is the mother of C

later someone will assert:
 motherOf(P,C) => parentOf(P,C)
     All mothers are parents

• Modus Tolens Entailment Rules in Prolog
  1) ~motherOf(P,C) :- ~parentOf(P,C).
  % disproved P is the mother of C when disproved P is the parent of C
• Modus Ponens Entailment Rules in Prolog
  2) parentOf(P,C) :- motherOf(P,C).
  % proved  P is the parent of C when proved P is the mother of C

       Notice it will not have any side effect other then marking two of the 7 literals above as dependant on authorial form here

If someone asserts
 motherOf(P,C) => ~fatherOf(P,C)
     No mothers can be fathers and vice versa. They are disjoint.

• Modus Tolens Entailment Rules in Prolog
  1)  ~motherOf(P,C):-fatherOf(P,C)
  % disproved P is the mother of C when proved P is the father of C
• Modus Ponens Entailment Rules in Prolog
  2)  ~fatherOf(P,C):-motherOf(P,C)
  % disproved P is the father of C when proved P is the mother of C

 ~motherOf(P,C) => fatherOf(P,C)
     All P/C relations are mother or father. They are disjoint

• Modus Tolens Entailment Rules in Prolog
  1)  motherOf(P,C):- ~fatherOf(P,C)
  % proved P is the mother of C when disproved P is the father of C
• Modus Ponens Entailment Rules in Prolog
  2)  fatherOf(P,C):-~motherOf(P,C)
  % proved P is the father of C when disproved P is the mother of C