NotEquivalent

src/interpreter/Preprocessor.kt

@@ -75,6 +75,7 @@ open class Preprocessor {
                     term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
                     term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
                     term.functor == "\\+/1" -> Not(args[0] as Goal)
+                    term.functor == "\\==/2" -> NotEquivalent(args[0], args[1])
                     term.functor == "==/2" -> Equivalent(args[0], args[1])
 
                     term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)

src/parser/grammars/TermsGrammar.kt

@@ -87,7 +87,7 @@ open class TermsGrammar : Tokens() {
         t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
     }
 
-    protected val op700: Parser<String> by (equivalent or equals or notEquals or isOp) use { text }
+    protected val op700: Parser<String> by (equivalent or notEquivalent or equals or notEquals or isOp) use { text }
     protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
         if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
     }

src/parser/grammars/Tokens.kt

@@ -20,6 +20,7 @@ abstract class Tokens : Grammar<Any>() {
     // 1000
     protected val comma: Token by literalToken(",")
     // 700
+    protected val notEquivalent: Token by literalToken("\\==")
     protected val equivalent: Token by literalToken("==")
     protected val equals: Token by literalToken("=")
     protected val isOp: Token by literalToken("is")

src/prolog/builtins/unificationOperators.kt

@@ -55,3 +55,12 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
         applySubstitution(term2, subs)
     )
 }
+
+class NotEquivalent(private val term1: Term, private val term2: Term) : Operator(Atom("\\=="), term1, term2) {
+    private val not = Not(Equivalent(term1, term2))
+    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+    override fun applySubstitution(subs: Substitutions): NotEquivalent = NotEquivalent(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
+}