diff --git a/collects/datalog/parse.rkt b/collects/datalog/parse.rkt
index 83e524991d..316ea79bdd 100644
--- a/collects/datalog/parse.rkt
+++ b/collects/datalog/parse.rkt
@@ -46,6 +46,7 @@
      (literal [(predicate-sym LPAREN RPAREN) (make-literal (make-srcloc $1-start-pos $3-end-pos) $1 empty)]
               [(predicate-sym LPAREN terms RPAREN) (make-literal (make-srcloc $1-start-pos $4-end-pos) $1 $3)]
               [(predicate-sym) (make-literal (make-srcloc $1-start-pos $1-end-pos) $1 empty)]
+              [(term NEQUAL term) (make-literal (make-srcloc $1-start-pos $3-end-pos) '!= (list $1 $3))]
               [(term EQUAL term) (make-literal (make-srcloc $1-start-pos $3-end-pos) '= (list $1 $3))])
      (predicate-sym [(IDENTIFIER) (string->symbol $1)]
                     [(STRING) $1])
diff --git a/collects/datalog/private/lex.rkt b/collects/datalog/private/lex.rkt
index 58b9f498eb..e2ca602fed 100644
--- a/collects/datalog/private/lex.rkt
+++ b/collects/datalog/private/lex.rkt
@@ -3,7 +3,7 @@
          (prefix-in : parser-tools/lex-sre))
 
 (define-tokens dtokens (VARIABLE IDENTIFIER STRING))
-(define-empty-tokens dpunct (LPAREN COMMA RPAREN TSTILE DOT EQUAL TILDE QMARK EOF))
+(define-empty-tokens dpunct (LPAREN COMMA RPAREN TSTILE DOT EQUAL NEQUAL TILDE QMARK EOF))
 (define-lex-abbrev line-break #\newline)
 (define-lex-abbrev id-chars (char-complement (char-set "(,)=:.~?\"% \n")))
 (define-lex-abbrev variable-re (:: upper-case (:* (:or upper-case lower-case (char-set "0123456789_")))))
@@ -38,6 +38,7 @@
    [#\~ (token-TILDE)]
    [#\? (token-QMARK)]
    [#\= (token-EQUAL)]
+   ["!=" (token-NEQUAL)]
    [(eof) (token-EOF)]))
 
 (provide dtokens dpunct 
diff --git a/collects/datalog/runtime.rkt b/collects/datalog/runtime.rkt
index 481d1c8786..4bf5b5f679 100644
--- a/collects/datalog/runtime.rkt
+++ b/collects/datalog/runtime.rkt
@@ -128,6 +128,14 @@
          [(unify-term (empty-env) a b)
           => (lambda (env) (equal-test (subst-term env a) (subst-term env b)))]
          [else (equal-test a b)])]
+      [(struct literal (srcloc '!= (list a b)))
+       (define (equal-test a b)
+         (unless (term-equal? a b)
+           (fact! sg (make-literal srcloc '!= (list a b)))))
+       (cond
+         [(unify-term (empty-env) a b)
+          => (lambda (env) (equal-test (subst-term env a) (subst-term env b)))]
+         [else (equal-test a b)])]
       [_
        (search-theory! sg)]))
   (define sg (make-subgoal q empty empty))
diff --git a/collects/datalog/scribblings/datalog.scrbl b/collects/datalog/scribblings/datalog.scrbl
index 6942712205..79d741441b 100644
--- a/collects/datalog/scribblings/datalog.scrbl
+++ b/collects/datalog/scribblings/datalog.scrbl
@@ -43,7 +43,7 @@ included in a string. The remaining characters may be specified using escape cha
 
 A literal, is a predicate symbol followed by an optional parenthesized list of comma separated terms. A predicate symbol is either an identifier
 or a string. A term is either a variable or a constant. As with predicate symbols, a constant is either an identifier or a string. As a special case,
-two terms separated by @litchar["="] is a literal for the equality predicate.
+two terms separated by @litchar["="] (@litchar["!="]) is a literal for the equality (inequality) predicate.
 The following are literals:
 @verbatim[#:indent 4 #<<END
 parent(john, douglas)
@@ -96,7 +96,8 @@ The following BNF describes the syntax of Datalog.
        (BNF-seq (nonterm "predicate-sym") (litchar "(") (litchar ")"))
        (BNF-seq (nonterm "predicate-sym") (litchar "(") (nonterm "terms") (litchar ")"))
        (nonterm "predicate-sym")
-       (BNF-seq (nonterm "term") (litchar "=") (nonterm "term")))
+       (BNF-seq (nonterm "term") (litchar "=") (nonterm "term"))
+       (BNF-seq (nonterm "term") (litchar "!=") (nonterm "term")))
  (list (nonterm "predicate-sym")
        (nonterm "IDENTIFIER")
        (nonterm "STRING"))
diff --git a/collects/datalog/tool/syntax-color.rkt b/collects/datalog/tool/syntax-color.rkt
index 5966b2ef4f..7974d22948 100644
--- a/collects/datalog/tool/syntax-color.rkt
+++ b/collects/datalog/tool/syntax-color.rkt
@@ -30,7 +30,7 @@
    [identifier-re
     (syn-val lexeme 'identifier #f start-pos end-pos)]
    [(:or #\) #\() (syn-val lexeme 'parenthesis #f start-pos end-pos)]
-   [(:or #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'parenthesis #f start-pos end-pos)]
+   [(:or "!=" #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'parenthesis #f start-pos end-pos)]
    [(eof) (syn-val lexeme 'eof #f start-pos end-pos)]
    [#\" ((colorize-string start-pos) input-port)]
    [any-char (syn-val lexeme 'error #f start-pos end-pos)]))
\ No newline at end of file
diff --git a/collects/tests/datalog/examples/sym.rkt b/collects/tests/datalog/examples/sym.rkt
new file mode 100644
index 0000000000..1fd63687f1
--- /dev/null
+++ b/collects/tests/datalog/examples/sym.rkt
@@ -0,0 +1,8 @@
+#lang datalog
+
+sym(a).
+sym(b).
+sym(c).
+perm(X,Y) :- sym(X), sym(Y), X != Y.
+
+perm(X,Y)?
\ No newline at end of file
diff --git a/collects/tests/datalog/examples/sym.txt b/collects/tests/datalog/examples/sym.txt
new file mode 100644
index 0000000000..15bc15f6a4
--- /dev/null
+++ b/collects/tests/datalog/examples/sym.txt
@@ -0,0 +1,8 @@
+perm(a, c).
+perm(a, b).
+perm(c, a).
+perm(b, a).
+perm(b, c).
+perm(c, b).
+
+
diff --git a/collects/tests/datalog/paren-examples/sym.rkt b/collects/tests/datalog/paren-examples/sym.rkt
new file mode 100644
index 0000000000..9d05e6b6eb
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/sym.rkt
@@ -0,0 +1,11 @@
+#lang datalog/sexp
+
+(! (sym a))
+(! (sym b))
+(! (sym c))
+(! (:- (perm X Y)
+       (sym X)
+       (sym Y)
+       (!= X Y)))
+
+(? (perm X Y))
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/sym.txt b/collects/tests/datalog/paren-examples/sym.txt
new file mode 100644
index 0000000000..15bc15f6a4
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/sym.txt
@@ -0,0 +1,8 @@
+perm(a, c).
+perm(a, b).
+perm(c, a).
+perm(b, a).
+perm(b, c).
+perm(c, b).
+
+
diff --git a/collects/tests/datalog/parse.rkt b/collects/tests/datalog/parse.rkt
index db86b57ecc..293aff4ae1 100644
--- a/collects/tests/datalog/parse.rkt
+++ b/collects/tests/datalog/parse.rkt
@@ -21,6 +21,8 @@
                         (make-literal #f 'parent (list (make-constant #f 'john) (make-constant #f 'douglas))))
     (test-literal-parse "1 = 2"
                         (make-literal #f '= (list (make-constant #f '|1|) (make-constant #f '|2|))))
+    (test-literal-parse "1 != 2"
+                        (make-literal #f '!= (list (make-constant #f '|1|) (make-constant #f '|2|))))
     (test-literal-parse "zero-arity-literal"
                         (make-literal #f 'zero-arity-literal empty))
     (test-literal-parse "zero-arity-literal()"
diff --git a/collects/tests/datalog/private/lex.rkt b/collects/tests/datalog/private/lex.rkt
index 6648cfd378..f4efacdf6b 100644
--- a/collects/tests/datalog/private/lex.rkt
+++ b/collects/tests/datalog/private/lex.rkt
@@ -17,6 +17,7 @@
    "lex"
    
    (test-lexer "=" 'EQUAL #f)
+   (test-lexer "!=" 'NEQUAL #f)
    (test-lexer "?" 'QMARK #f)
    (test-lexer "~" 'TILDE #f)
    (test-lexer "." 'DOT #f)
diff --git a/collects/tests/datalog/tool/syntax-color.rkt b/collects/tests/datalog/tool/syntax-color.rkt
index 6b48bb8e4e..5103300c42 100644
--- a/collects/tests/datalog/tool/syntax-color.rkt
+++ b/collects/tests/datalog/tool/syntax-color.rkt
@@ -24,6 +24,7 @@
    (test-color "123var" 'identifier)
    (test-color "(" 'parenthesis)
    (test-color ")" 'parenthesis)
+   (test-color "!=" 'parenthesis)
    (test-color "=" 'parenthesis)
    (test-color "?" 'parenthesis)
    (test-color "~" 'parenthesis)