KNOWLEDGE ENGINEERING, PART A: Knowledge Representation 

Let p and q be any propositions.
Conjunction (and) p ^ q
Disjunction (or) p v q
Negation (not) ~p
Implication (if  then) p > q
Biconditional (ifandonlyif) p <> q
Disjunction (or) p v q ~(~p ^ ~q)
Implication (if  then) p > q ~(p ^ ~(q))
Biconditional (ifandonlyif) p <> q ~(p^~q)^~(~p^q)
Negation (not) ~p (p NAND p)
Negation (not) ~p (p NOR p)
Conjunction (and) p ^ q (p NAND q) NAND (p NAND q)
Conjunction (and) p ^ q (p NOR p) NOR (q NOR q)
Let symbols p, q and
r represent any formulas whatever:
Modus Ponens.  From p and p > q,  derive q. 
Modus Tollens.  From ~q and p > q, .  derive ~p 
Hypothetical Syllogism.  From p > q and q > r,  derive p > r. 
Disjunctive Syllogism.  From p v q and ~p,  derive q. 
Conjunction.  From p and q,  derive p ^ q. 
Addition.  From p,  derive p v q . 


Subtraction.  From p ^ q,  derive p. 

Idempotency. p ^ p is identical to p
p v p is identical to p
Commutativity. p ^ q is identical to q ^ p
p v q is identical to q v p
Associativity. p ^ (q ^ r) is identical to (p ^ q) ^ r
p v (q v r) is identical to (p v q) v r
Distributivity. p ^ (q v r) is identical to (p ^ q) v (p ^ r)
p v (q ^ r) is identical to (p v q) ^ (p v r)
Absorption. p ^ (p v q) is identical to p
p v (p ^ q) is identical to p
Double Negation. p is identical to ~~p
De Morgan's Law. ~(p ^ q) is identical to ~p v ~q
~(p v q) is identical to ~p ^ ~q
Universal Instantiation.  From "xF(x), derive F(c), where c is any constant. 
Existential Generalisation.  From F(c), where c is any constant, derive $xF(x), provided that every occurrence of x in F(x) must be free. 
Dropping Quantifiers.  If the variable x does not occur free in F, then from $xF derive F, and from "xF derive F. 
Adding Quantifiers.  From F derive "xF or derive $xF, where x is any variable whatever. 
Substituting equals for equals.  From F(t) and t=u, derive F(u), provided that all free occurrence of variable in u remain free in F(u). 
"x(PEACH(x) > FUZZY(x)) ~$x(PEACH(x) ^ ~FUZZY(x))
"x(PEACH(x) > FUZZY(x)) => ~$x~(PEACH(x) > FUZZY(x)) => ~$x~~(PEACH(x) ^ ~FUZZY(x)) => ~$x(PEACH(x) ^ ~FUZZY(x))
Since the dyadic predicate MARRIED is symmetric, MARRIED(Ike, Mamie) is equivalent to MARRIED(Mamie, Ike).
Interchanging arguments of that predicate makes no difference, but interchanging the two quantifiers lead to the formula:
$y"x ((MAN(x) ^ DEPT(x, C99)) > (WOMAN(y) ^ HOMETOWN(y, BOSTON) ^ MARRIED(x, y))).
This formula says that there exists a y such that for every x, if x is a man and x works in department C99, then y is a woman, the home town of y is Boston, and x married y.
In English, that would be the same as saying, A woman who came from Boston married every man in department C99.
If there are more than one man in department C99, this sentence has implication that are very different from the preceding one.
Standard Notation  Graphical Form  Linear Form 
p ^ q ^ r  p q r  
~(p ^ q ^ r)  (p q r)  
~~(p ^ q ^ r)  ((p q r)) 

Equivalent Standard Notation  Graphical Form  Linear Form 
p v q v r  ~(~p ^ ~q ^ ~r)  ((p) (q) (r))  
p > q  ~(p ^ ~q)  (p (q))  
p > (q v r)  ~(p ^ ~q ^ ~r)  (p (q) (r))  
(p ^ q) > (r ^ s)  ~( p ^ q ~(r ^ s))  (p q (r s))  
(p <> q)  ~(p ^ ~q) ^ ~(~p ^ q)  (p (q)) ((p) q) 
Erasure  Any evenly enclosed graph may be erased. 
Insertion  Any graph may be inserted in any oddly enclosed context. 
Iteration  A copy of any graph u may be inserted into the same context in which u occurs or into any context dominated by u. 
Deiteration  Any graph whose occurrence could be the result of iteration may be erased (i.e., if it is identical to another graph in the same context or in a dominating context). 
Double
Negation 
A double negation may be drawn around or removed from any graph or set of graphs in any context. 
4.3.3 Theorem. For any set S of conceptual graphs, the following three statements are equivalent:
(a) Prove: (p v p) > p Graph Notation: (p v p) > p => ~(~p ^ ~p)  > p => ~(~(~p ^ ~p) ^ ~p) => (((p) (p)) (p)) Constriction: {} => (()) => (() (p)) => (((p)) (p)) => (((p) (p)) (p))
(b) Prove: q > (p v q) Graph Notation: (q (p) (q)) Construction: {} (())  double negation (q ())  insertion of q (q (q) )  iteration of q (q (q) (p)) insertion of (p)
(c) Prove: (p v q) > (q v p) Graph Notation: (((p) (q)) (p) (q)) Construction: <exercise>
(d) Prove: (q > r) > ((p v q) > (p v r)) Construction: <exercise>
Erasure.  A collection of graphs in a positive context is asserted to be true. Erasing any of them leaves the remaining graphs just as true as they were before. If all the graphs are erased, the empty sheet that is left says nothing false: silence is golden. 
Insertion  A collection of graphs in a negative context is asserted to be false or at best hypothetical. Adding more graphs can never make the collection true. Therefore, the negative context remains false, and the negation of falsehood is true. 
Iteration  Copying a subgraph in the same context makes a redundant copy that has no effect on the truth value. If a subgraph is copied into a nested context, its main contribution to the truth value was made in the outer context, and the copy has no effect on the truth value. 
Deiteration  A copy of a subgraph in the same context or a nested context adds nothing new to the truth value of the entire graph, and the nested copy may be erased without changing the truth value. 
Double
Negation 
Two negations with nothing between the inner and outer oval cancel each other out, and they may be added or erased without having any effect on the overall truth value. 
Erasure  In an evenly enclosed context, any graph may be erased, any coreference link from a dominating concept to an evenly enclosed concept may be erased, any referent may be erased, and any type label may be replaced with a supertype. 
Insertion  In an oddly enclosed context, any graph may be inserted, a coreference link may be drawn between any two identical concepts, and restriction may be performed on any concept. 
Iteration  A copy of any graph u may be inserted into the same context in which u occurs or into any context dominated by u. A coreference link may be drawn from any concept of u to the corresponding concept in the copy of u. If concepts a and b in some context c are both dominated by a concept d on some line of identity, then a coreference link may be drawn from a to b. 
Deiteration  Any graph or coreference link whose occurrence could be the result of iteration may be erased. Duplicate conceptual relations may be erased from any graph. 
Double
Negation 
A double negation may be drawn around or removed from any graph in any context. 
Coreferent
Join 
Two identical, coreferent concepts in the same context may be joined, and the coreference link between them may then be erased. 
Individuals  If any individual concept a dominates a generic concept b where a and b are coreferent, the referent(a) may be copied to b, and then coreference link may be erased. 
Given the following law defining citizenship in the Land of Oz.
( [person:*x]<(obj)<[born]>(loc)>[country:oz] r1 ([citizen:*x]<(memb)<[country:oz]) ) ( [person:*x]<(chld)<[citizen]<(memb)<[country:oz] r2 ([citizen:*x]<(memb)<[country:oz]) ) ( [person:*x]<(rcpt)<[naturalise]>(loc)>[country:oz] r3 ([citizen:*x]<(memb)<[country:oz]) ) ( [citizen:*x]<(memb)<[country:oz] r4 ( [person:*x]<(obj)<[born]>(loc)>[country:oz] ) ( [person:*x]<(chld)<[citizen]<(memb)<[country:oz] ) ( [person:*x]<(rcpt)<[naturalise]>(loc)>[country:oz] ) )Suppose that the outermost context contain the above four graphs together with the following graph:
[person:tinman]<(rcpt)<[naturalise]>(loc)>[country:oz]By iteration, a copy of this graphs may be inserted into the r3 to produce a graph as shown below:
( [person:tinman]<(rcpt)<[naturalise]>(loc)>[country:oz] [person:*x]<(rcpt)<[naturalise]>(loc)>[country:oz] ([citizen:*x]<(memb)<[country:oz]) )The two oddly enclosed graphs may be joined: first [person] is restricted to [person:tinman]; then a coreference link is drawn between them; finally, they are joined.
Similar joins of [naturalise] to [naturalise] and [country:oz] to [country:oz] may be made.
The duplicate copies of (rcpt) and (loc) may be erased by deiteration.
Next, the referent Tinman may be copied to the coreferent concept [citizen] in the innermost context and the coreference link erased.
The resulting graph is shown below:
( [person:tinman]<(rcpt)<[naturalise]>(loc)>[country:oz] ([citizen:tinman]<(memb)<[country:oz]) )By deiteration, the oddly enclosed graph may be erases because it is an exact copy of the graph that says the Tinman was naturalised in Oz.
The result is the following graph:
( ([citizen:tinman]<(memb)<[country:oz]) )Removal of double negation results in the following graph:
[citizen:tinman]<(memb)<[country:oz]
Dickson Lukose & Rob Kremer. KNOWLEDGE ENGINEERING, PART A: Knowledge Representation. July 1996. 
