Checkpoint

src/prolog/Program.kt

@@ -2,12 +2,10 @@ package prolog
 
 import prolog.logic.Substituted
 import prolog.ast.logic.Clause
-import prolog.ast.logic.Fact
 import prolog.ast.logic.Predicate
 import prolog.ast.logic.Resolvent
 import prolog.ast.terms.Functor
 import prolog.ast.terms.Goal
-import prolog.builtins.True
 
 typealias Database = Program
 
@@ -24,7 +22,6 @@ object Program: Resolvent {
     private fun setup() {
         // Initialize the program with built-in predicates
         load(listOf(
-            Fact(True())
         ))
     }
 

src/prolog/ast/arithmetic/ArithmeticOperator.kt

@@ -0,0 +1,12 @@
+package prolog.ast.arithmetic
+
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Operator
+import prolog.ast.terms.Term
+import prolog.logic.Substituted
+
+abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) :
+    Operator(symbol, leftOperand, rightOperand), Expression {
+    // Operators should overload the evaluate method to perform the operation
+    abstract override fun evaluate(subs: Substituted): Pair<Term, Substituted>
+}

src/prolog/ast/arithmetic/Expression.kt

@@ -0,0 +1,5 @@
+package prolog.ast.arithmetic
+
+import prolog.ast.terms.Term
+
+interface Expression : Term

src/prolog/ast/logic/Clause.kt

@@ -37,7 +37,7 @@ abstract class Clause(private val head: Head, private val body: Body) : Resolven
 
     override fun toString(): String {
         return when {
-            body == True() -> head.toString()
+            body is True -> head.toString()
             else         -> "$head :- $body"
         }
     }

src/prolog/ast/logic/Fact.kt

@@ -3,4 +3,4 @@ package prolog.ast.logic
 import prolog.ast.terms.Head
 import prolog.builtins.True
 
-class Fact(head: Head) : Clause(head, True())
+class Fact(head: Head) : Clause(head, True)

src/prolog/ast/logic/LogicOperand.kt

@@ -0,0 +1,5 @@
+package prolog.ast.logic
+
+import prolog.ast.terms.Operand
+
+abstract class LogicOperand : Operand, Provable

src/prolog/ast/logic/LogicOperator.kt

@@ -0,0 +1,13 @@
+package prolog.ast.logic
+
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Operator
+import prolog.logic.Substituted
+
+abstract class LogicOperator(
+    symbol: Atom,
+    leftOperand: LogicOperand? = null,
+    rightOperand: LogicOperand
+) : Operator(symbol, leftOperand, rightOperand), Provable {
+    abstract override fun prove(subs: Substituted): Sequence<Substituted>
+}

src/prolog/ast/terms/Atom.kt

@@ -9,6 +9,11 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
 
     override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> = unifyLazy(goal, this, subs)
 
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> = Pair(this, emptyMap())
+
+    /**
+     * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
+     */
     override fun compareTo(other: Term): Int {
         return when (other) {
             is Variable -> 1

src/prolog/ast/terms/Goal.kt

@@ -1,7 +1,7 @@
 package prolog.ast.terms
 
 import prolog.Program
-import prolog.ast.logic.Provable
+import prolog.ast.logic.LogicOperand
 import prolog.logic.Substituted
 
 /**
@@ -11,7 +11,7 @@ import prolog.logic.Substituted
  * A goal either [succeeds][prolog.builtins.True], in which case the variables in the compound terms have a binding,
  * or it fails if Prolog fails to prove it.
  */
-abstract class Goal : Term, Provable {
+abstract class Goal : LogicOperand(), Term {
     abstract val functor: Functor
 
     override fun prove(subs: Substituted): Sequence<Substituted> = Program.solve(this, subs)

src/prolog/ast/terms/Integer.kt

@@ -0,0 +1,32 @@
+package prolog.ast.terms
+
+import prolog.ast.arithmetic.Expression
+import prolog.logic.Substituted
+
+data class Integer(val value: Int): Term, Expression {
+    /**
+     * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
+     */
+    override fun compareTo(other: Term): Int {
+        return when (other) {
+            is Variable -> 1
+            is Integer -> value.compareTo(other.value)
+            else -> -1
+        }
+    }
+
+    // Integers are already evaluated
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> = Pair(this, emptyMap())
+
+    override fun toString(): String {
+        return value.toString()
+    }
+
+    operator fun plus(other: Integer): Integer {
+        return Integer(value + other.value)
+    }
+
+    operator fun minus(other: Integer): Integer {
+        return Integer(value - other.value)
+    }
+}

src/prolog/ast/terms/Operator.kt

@@ -1,21 +1,16 @@
 package prolog.ast.terms
 
-import prolog.ast.logic.Provable
+typealias Operand = Term
-import prolog.logic.Substituted
 
 abstract class Operator(
     private val symbol: Atom,
-    val leftOperand: Operand? = null,
+    private val leftOperand: Operand? = null,
-    val rightOperand: Operand
+    private val rightOperand: Operand
-) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Provable {
+) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)) {
-    abstract override fun prove(subs: Substituted): Sequence<Substituted>
-
     override fun toString(): String {
         return when (leftOperand) {
             null -> "${symbol.name} $rightOperand"
-            else -> "$leftOperand ${symbol.name} $rightOperand"
+            else -> "($leftOperand ${symbol.name} $rightOperand)"
         }
     }
 }
-
-typealias Operand = Goal

src/prolog/ast/terms/Structure.kt

@@ -1,7 +1,7 @@
 package prolog.ast.terms
 
 import prolog.ast.logic.Resolvent
-import prolog.builtins.equivalent
+import prolog.logic.equivalent
 import prolog.logic.Substituted
 import prolog.logic.unifyLazy
 
@@ -9,13 +9,19 @@ typealias Argument = Term
 
 typealias CompoundTerm = Structure
 
-open class Structure(val name: Atom, val arguments: List<Argument>) : Goal(), Head, Body, Resolvent {
+open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), Head, Body, Resolvent {
     override val functor: Functor = "${name.name}/${arguments.size}"
 
     override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> {
         return unifyLazy(goal, this, subs)
     }
 
+    // A structure does not need to be evaluated, so return an empty sequence.
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> = Pair(this, emptyMap())
+
+    /**
+     * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
+     */
     override fun compareTo(other: Term): Int {
         when (other) {
             is Structure -> {

src/prolog/ast/terms/Term.kt

@@ -1,9 +1,16 @@
 package prolog.ast.terms
 
+import prolog.logic.Substituted
+
 /**
  * Value in Prolog.
  *
  * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type string.
  */
-interface Term : Comparable<Term>
+interface Term : Comparable<Term> {
+    /**
+     * Returns the term that this expression evaluates to. (All the way down.)
+     */
+    fun evaluate(subs: Substituted): Pair<Term, Substituted>
+}

src/prolog/ast/terms/Variable.kt

@@ -1,8 +1,10 @@
 package prolog.ast.terms
 
+import prolog.ast.arithmetic.Expression
+import prolog.logic.Substituted
 import java.util.*
 
-data class Variable(val name: String) : Term {
+data class Variable(val name: String) : Term, Expression {
     private var alias: Optional<Term> = Optional.empty()
 
     fun alias(): Optional<Term> {
@@ -21,6 +23,16 @@ data class Variable(val name: String) : Term {
         alias = Optional.empty()
     }
 
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+        // If the variable is bound, return the value of the binding
+        // If the variable is not bound, return the variable itself
+        return if (alias.isPresent) {
+            alias.get().evaluate(subs)
+        } else {
+            Pair(this, emptyMap())
+        }
+    }
+
     override fun compareTo(other: Term): Int {
         return when (other) {
             is Variable -> name.compareTo(other.name)

src/prolog/builtins/arithmetic.kt

@@ -1 +0,0 @@
-package prolog.builtins

src/prolog/builtins/arithmeticOperators.kt

@@ -0,0 +1,152 @@
+package prolog.builtins
+
+import prolog.ast.arithmetic.ArithmeticOperator
+import prolog.ast.arithmetic.Expression
+import prolog.ast.logic.LogicOperand
+import prolog.ast.logic.LogicOperator
+import prolog.ast.logic.Provable
+import prolog.ast.terms.*
+import prolog.logic.*
+
+// TODO >
+
+// TODO <
+
+// TODO =<
+
+// TODO >=
+
+/**
+ * True if expression Expr1 evaluates to a number non-equal to Expr2.
+ */
+class EvaluatesToDifferent(private val left: Expression, private val right: Expression) :
+    ArithmeticOperator(Atom("=\\="), left, right) {
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+        val t1 = left.evaluate(subs)
+        val t2 = right.evaluate(subs)
+
+        // Should both be instantiated
+        if (!atomic(t1.first) || !atomic(t2.first)) {
+            throw IllegalArgumentException("Both operands must be instantiated")
+        }
+
+        return if (equivalent(t1.first, t2.first)) {
+            Pair(False, emptyMap())
+        } else {
+            Pair(True, t1.second + t2.second)
+        }
+    }
+
+}
+
+/**
+ * True if Expr1 evaluates to a number equal to Expr2.
+ */
+class EvaluatesTo(private val left: Expression, private val right: Expression) :
+    ArithmeticOperator(Atom("=:="), left, right) {
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+        val t1 = left.evaluate(subs)
+        val t2 = right.evaluate(subs)
+
+        // Should both be instantiated
+        if (!atomic(t1.first) || !atomic(t2.first)) {
+            throw IllegalArgumentException("Both operands must be instantiated")
+        }
+
+        return if (equivalent(t1.first, t2.first)) {
+            Pair(True, t1.second + t2.second)
+        } else {
+            Pair(False, emptyMap())
+        }
+    }
+}
+
+/**
+ * True when Number is the value to which Expr evaluates.
+ */
+class Is(private val left: Expression, private val right: Expression) :
+    Operator(Atom("is"), left, right), Provable {
+    override fun prove(subs: Substituted): Sequence<Substituted> {
+        val t1 = left.evaluate(subs)
+        val t2 = right.evaluate(subs)
+
+        if (!atomic(t2.first)) {
+            throw IllegalArgumentException("Arguments are not sufficiently instantiated")
+        }
+
+        return unifyLazy(t1.first, t2.first, subs).map{ it + t1.second + t2.second }
+    }
+}
+
+/**
+ * Result = -Expr
+ */
+class Negate(operand: Expression) : Subtract(Integer(0), operand)
+
+/**
+ * Result = Expr
+ */
+class Positive(operand: Expression) : Add(Integer(0), operand)
+
+/**
+ * Result = Expr1 + Expr2
+ */
+open class Add(private val expr1: Expression, private val expr2: Expression) :
+    ArithmeticOperator(Atom("+"), expr1, expr2) {
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+        val result = Variable("Result")
+        val map = plus(expr1, expr2, result, subs)
+        return result.evaluate(map.first())
+    }
+}
+
+/**
+ * Result = Expr1 - Expr2
+ */
+open class Subtract(private val expr1: Expression, private val expr2: Expression) :
+    ArithmeticOperator(Atom("-"), expr1, expr2) {
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+        val result = Variable("Result")
+        val map = plus(expr2, result, expr1, subs)
+        return result.evaluate(map.first())
+    }
+}
+
+// TODO Expr * Expr
+/**
+ * Result = Expr1 * Expr2
+ */
+class Multiply(private val expr1: Expression, private val expr2: Expression) :
+    ArithmeticOperator(Atom("*"), expr1, expr2) {
+    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+        val result = Variable("Result")
+        val map = mul(expr1, expr2, result, subs)
+        return result.evaluate(map.first())
+    }
+}
+
+// TODO Expr / Expr
+
+// TODO Expr mod Expr
+
+// TODO Expr rem Expr
+
+class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) :
+    Operator(Atom("between"), expr1, expr2) {
+    override fun prove(subs: Substituted): Sequence<Substituted> {
+        val e1 = expr1.evaluate(subs)
+        val e2 = expr2.evaluate(subs)
+        val e3 = expr3.evaluate(subs)
+
+        require(e1.first is Integer && e2.first is Integer) { "Arguments must be integers" }
+
+        val v1 = e1.first as Integer
+        val v2 = e2.first as Integer
+
+        return if (variable(e3.first)) {
+            between(v1, v2, e3.first as Variable).map { it + e1.second + e2.second }
+        } else {
+            between(v1, v2, e3.first as Integer).map { it + e1.second + e2.second }
+        }
+    }
+}

src/prolog/builtins/controlOperators.kt

@@ -1,12 +1,16 @@
 package prolog.builtins
 
-import prolog.ast.terms.*
+import prolog.ast.logic.LogicOperand
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Body
+import prolog.ast.terms.Goal
+import prolog.ast.logic.LogicOperator
 import prolog.logic.Substituted
 
 /**
  * Always fail.
  */
-class Fail : Atom("fail"), Body {
+object Fail : Atom("fail"), Body {
     override fun prove(subs: Substituted): Sequence<Substituted> = emptySequence()
 }
 
@@ -18,7 +22,7 @@ typealias False = Fail
 /**
  * Always succeed.
  */
-class True : Atom("true"), Body {
+object True : Atom("true"), Body {
     override fun prove(subs: Substituted): Sequence<Substituted> = sequenceOf(emptyMap())
 }
 
@@ -29,34 +33,29 @@ class True : Atom("true"), Body {
 /**
  * Conjunction (and). True if both Goal1 and Goal2 are true.
  */
-class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand) {
+class Conjunction(private val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) {
     override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
-        if (leftOperand != null) {
+        left.prove(subs).forEach { left ->
-            leftOperand.prove(subs).forEach { left ->
+            right.prove(subs + left).forEach { right ->
-                rightOperand.prove(subs + left).forEach { right ->
                 yield(left + right)
             }
         }
-        } else {
-            yieldAll(rightOperand.prove(subs))
-        }
     }
 }
 
 /**
  * Disjunction (or). True if either Goal1 or Goal2 succeeds.
  */
-open class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) {
+open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) :
+    LogicOperator(Atom(";"), left, right) {
     override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
-        if (leftOperand != null) {
+        yieldAll(left.prove(subs))
-            yieldAll(leftOperand.prove(subs))
+        yieldAll(right.prove(subs))
-        }
-        yieldAll(rightOperand.prove(subs))
     }
 }
 
 @Deprecated("Use Disjunction instead")
-class Bar(leftOperand: Operand, rightOperand: Operand) : Disjunction(leftOperand, rightOperand)
+class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(leftOperand, rightOperand)
 
 // TODO ->
 
@@ -65,10 +64,10 @@ class Bar(leftOperand: Operand, rightOperand: Operand) : Disjunction(leftOperand
 /**
  * True if 'Goal' cannot be proven.
  */
-class Not(goal: Goal) : Operator(Atom("\\+"), rightOperand = goal) {
+class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) {
     override fun prove(subs: Substituted): Sequence<Substituted> {
         // If the goal can be proven, return an empty sequence
-        if (rightOperand.prove(subs).toList().isNotEmpty()) {
+        if (goal.prove(subs).toList().isNotEmpty()) {
             return emptySequence()
         }
         // If the goal cannot be proven, return a sequence with an empty map

src/prolog/builtins/meta.kt

@@ -1 +0,0 @@
-package prolog.builtins

src/prolog/builtins/other.kt

@@ -1,10 +1,10 @@
 package prolog.builtins
 
+import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.Atom
-import prolog.ast.terms.Operand
+import prolog.ast.logic.LogicOperator
-import prolog.ast.terms.Operator
 import prolog.logic.Substituted
 
-class Query(rightOperand: Operand) : Operator(Atom("?-"), null, rightOperand) {
+class Query(private val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
-    override fun prove(subs: Substituted): Sequence<Substituted> = rightOperand.prove(subs)
+    override fun prove(subs: Substituted): Sequence<Substituted> = query.prove(subs)
 }

src/prolog/builtins/unification.kt

@@ -1,24 +1,24 @@
+/**
+ * Comparison and Unification of Terms
+ *
+ * [SWI Prolog Documentation](https://www.swi-prolog.org/pldoc/man?section=compare)
+ */
 package prolog.builtins
 
 import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
+import prolog.ast.terms.Operator
 import prolog.ast.terms.Term
-import prolog.ast.terms.Variable
+import prolog.logic.Substituted
+import prolog.logic.applySubstitution
+import prolog.logic.equivalent
 
-/**
+class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
- * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable.
+    override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
- */
+        val t1 = applySubstitution(term1, subs)
-fun equivalent(term1: Term, term2: Term): Boolean {
+        val t2 = applySubstitution(term2, subs)
-    return when {
+
-        term1 is Variable && term2 is Variable -> term1 == term2
+        if (equivalent(t1, t2)) {
-        term1 is Variable -> term1.alias().isPresent && equivalent(term1.alias().get(), term2)
+            yield(emptyMap())
-        term2 is Variable -> term2.alias().isPresent && equivalent(term2.alias().get(), term1)
+        }
-        term1 is Atom && term2 is Atom -> term1.compareTo(term2) == 0
-        term1 is Structure && term2 is Structure -> term1.compareTo(term2) == 0
-        else -> false
     }
 }
-
-/**
- *
- */

src/prolog/logic/arithmetic.kt

@@ -0,0 +1,150 @@
+package prolog.logic
+
+import prolog.ast.arithmetic.Expression
+import prolog.ast.terms.Integer
+import prolog.ast.terms.Variable
+import prolog.builtins.Is
+import java.util.*
+
+/**
+ * Low and High are integers, High ≥Low.
+ *
+ * 1. If Value is an integer, Low ≤ Value ≤ High.
+ * 2. When Value is a variable it is successively bound to all integers between Low and High.
+ *    If High is inf or infinite between/3 is true iff Value ≥ Low, a feature that is particularly interesting for
+ *    generating integers from a certain value.
+ */
+fun between(
+    low: Integer,
+    high: Integer,
+    value: Integer
+): Sequence<Substituted> {
+    return if (value.value in low.value..high.value) {
+        sequenceOf(emptyMap())
+    } else {
+        emptySequence()
+    }
+}
+
+fun between(
+    low: Integer,
+    high: Integer,
+    variable: Variable
+): Sequence<Substituted> {
+    return sequence {
+        for (i in low.value..high.value) {
+            yield(mapOf(variable to Integer(i)))
+        }
+    }
+}
+
+/**
+ * True if Int2 = Int1 + 1 and Int1 ≥ 0.
+ *
+ * At least one of the arguments must be instantiated to a natural number.
+ *
+ * @throws IllegalArgumentException the domain error not_less_than_zero if called with a negative integer.
+ * E.g. succ(X, 0) fails silently and succ(X, -1) raises a domain error.125
+ */
+fun succ(term1: Expression, term2: Expression, subs: Substituted): Sequence<Substituted> {
+    if (term2 is Integer) {
+        require(term2.value >= 0) { "Domain error: not_less_than_zero" }
+    }
+    val result = plus(term1, Integer(1), term2, subs)
+    // If term1 is a variable, we need to check if it is bound to a negative integer
+    return sequence { result.forEach { newSubs ->
+        val t1 = applySubstitution(term1, newSubs)
+        if (t1 is Variable && t1.alias().isPresent) {
+            val e1 = t1.evaluate(subs)
+            if(e1.first is Integer && (e1.first as Integer).value < 0) {
+                return@sequence
+            }
+        }
+        yield(newSubs)
+    }}
+}
+
+/**
+ * True if Int3 = Int1 + Int2.
+ *
+ * At least two of the three arguments must be instantiated to integers.
+ */
+fun plus(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence<Substituted> = sequence {
+    val t1 = applySubstitution(term1, subs)
+    val t2 = applySubstitution(term2, subs)
+    val t3 = applySubstitution(term3, subs)
+
+    // At least two arguments must be Integers
+    when {
+        nonvariable(t1) && nonvariable(t2) && nonvariable(t3) -> {
+            val e1 = t1.evaluate(subs)
+            val e2 = t2.evaluate(subs)
+            val e3 = t3.evaluate(subs)
+
+            val int3Value = e1.first as Integer + e2.first as Integer
+            if (int3Value == e3.first as Integer) {
+                yield(e1.second + e2.second + e3.second)
+            }
+        }
+        nonvariable(t1) && nonvariable(t2) && variable(t3) -> {
+            val e1 = t1.evaluate(subs)
+            val e2 = t2.evaluate(subs)
+
+            val int3Value = e1.first as Integer + e2.first as Integer
+            val int3 = t3 as Variable
+            int3.bind(int3Value)
+            yield(mapOf(int3 to int3Value) + e1.second + e2.second)
+        }
+        nonvariable(t1) && variable(t2) && nonvariable(t3) -> {
+            val e1 = t1.evaluate(subs)
+            val e3 = t3.evaluate(subs)
+
+            val int2Value = e3.first as Integer - e1.first as Integer
+            val int2 = t2 as Variable
+            int2.bind(int2Value)
+            yield(mapOf(int2 to int2Value) + e1.second + e3.second)
+        }
+        variable(t1) && nonvariable(t2) && nonvariable(t3) -> {
+            val e2 = t2.evaluate(subs)
+            val e3 = t3.evaluate(subs)
+
+            val int1Value = e3.first as Integer - e2.first as Integer
+            val int1 = t1 as Variable
+            int1.bind(int1Value)
+            yield(mapOf(int1 to int1Value) + e2.second + e3.second)
+        }
+        else -> {
+            throw IllegalArgumentException("At least two arguments must be instantiated to integers")
+        }
+    }
+}
+
+/**
+ * Recursive implementation of the multiply operator, logical programming-wise.
+ */
+fun mul(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence<Substituted> = sequence {
+    val t1 = applySubstitution(term1, subs)
+    val t2 = applySubstitution(term2, subs)
+    val t3 = applySubstitution(term3, subs)
+
+    // Base case
+    if (equivalent(t2, Integer(0))) {
+        yieldAll(Is(t3, Integer(0)).prove(subs))
+    }
+
+    // Recursive case
+    try {
+        val decremented = Variable("Decremented")
+        succ(decremented, t2, subs).forEach { decrementMap ->
+            val multiplied = Variable("Multiplied")
+            mul(t1, decremented, multiplied, subs + decrementMap).forEach { multipliedMap ->
+                yieldAll(plus(t1, multiplied, t3, subs + decrementMap + multipliedMap))
+            }
+        }
+    } catch(_: Exception) {
+    }
+}
+
+// TODO divmod
+
+// TODO nth_integer_root_and_remainder

src/prolog/logic/unification.kt

@@ -1,27 +1,33 @@
 package prolog.logic
 
-import prolog.ast.terms.Structure
+import prolog.ast.arithmetic.Expression
-import prolog.ast.terms.Term
+import prolog.ast.logic.LogicOperator
-import prolog.ast.terms.Variable
+import prolog.ast.terms.*
-import prolog.builtins.atomic
-import prolog.builtins.compound
-import prolog.builtins.equivalent
-import prolog.builtins.variable
 import java.util.*
 
 typealias Substituted = Map<Variable, Term>
 
 // Apply substitutions to a term
-private fun applySubstitution(term: Term, substitution: Substituted): Term = when {
+fun applySubstitution(term: Term, subs: Substituted): Term = when {
-    variable(term) -> substitution[(term as Variable)] ?: term
+    variable(term) -> subs[(term as Variable)] ?: term
     atomic(term)   -> term
     compound(term) -> {
         val structure = term as Structure
-        Structure(structure.name, structure.arguments.map { applySubstitution(it, substitution) })
+        Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
     }
     else -> term
 }
 
+fun applySubstitution(expr: Expression, subs: Substituted): Expression = when {
+    variable(expr) -> applySubstitution(expr as Term, subs) as Expression
+    atomic(expr)   -> expr
+    expr is LogicOperator -> {
+        expr.arguments = expr.arguments.map { applySubstitution(it, subs) }
+        expr
+    }
+    else -> expr
+}
+
 // Check if a variable occurs in a term
 private fun occurs(variable: Variable, term: Term): Boolean = when {
     variable(term) -> term == variable
@@ -33,8 +39,8 @@ private fun occurs(variable: Variable, term: Term): Boolean = when {
     else -> false
 }
 
-// Generate possible substitutions
+// Unify two terms with backtracking and lazy evaluation
-private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted): Sequence<Substituted> = sequence {
+fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence<Substituted> = sequence {
     val t1 = applySubstitution(term1, subs)
     val t2 = applySubstitution(term2, subs)
 
@@ -59,7 +65,7 @@ private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted):
             val structure2 = t2 as Structure
             if (structure1.functor == structure2.functor) {
                 val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(subs) { acc, (arg1, arg2) ->
-                    generateSubstitutions(arg1, arg2, acc).firstOrNull() ?: return@sequence
+                    unifyLazy(arg1, arg2, acc).firstOrNull() ?: return@sequence
                 }
                 yield(newSubstitution)
             }
@@ -68,14 +74,6 @@ private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted):
     }
 }
 
-// Unify two terms with backtracking and lazy evaluation
-fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence<Substituted> = sequence {
-    generateSubstitutions(term1, term2, subs).forEach { newSubs ->
-        // Return the new substitution
-        yield(newSubs)
-    }
-}
-
 fun unify(term1: Term, term2: Term): Optional<Substituted> {
     val substitutions = unifyLazy(term1, term2, emptyMap()).toList()
     return if (substitutions.isNotEmpty()) {
@@ -84,3 +82,18 @@ fun unify(term1: Term, term2: Term): Optional<Substituted> {
         Optional.empty()
     }
 }
+
+/**
+ * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable.
+ */
+fun equivalent(term1: Term, term2: Term): Boolean {
+    return when {
+        term1 is Atom && term2 is Atom -> term1.compareTo(term2) == 0
+        term1 is Structure && term2 is Structure -> term1.compareTo(term2) == 0
+        term1 is Integer && term2 is Integer -> term1.compareTo(term2) == 0
+        term1 is Variable && term2 is Variable -> term1 == term2
+        term1 is Variable -> term1.alias().isPresent && equivalent(term1.alias().get(), term2)
+        term2 is Variable -> term2.alias().isPresent && equivalent(term2.alias().get(), term1)
+        else -> false
+    }
+}

src/prolog/logic/verification.kt

@@ -1,4 +1,4 @@
-package prolog.builtins
+package prolog.logic
 
 import prolog.ast.terms.CompoundTerm
 import prolog.ast.terms.Term
@@ -37,5 +37,5 @@ fun variable(term: Term): Boolean {
         return term.alias().isEmpty || term.alias().get() === term || variable(term.alias().get())
     }
 
-    return false;
+    return false
 }

tests/prolog/EvaluationTest.kt

@@ -8,7 +8,7 @@ import prolog.ast.logic.Rule
 import prolog.builtins.Conjunction
 import prolog.builtins.Disjunction
 import prolog.builtins.Query
-import prolog.builtins.equivalent
+import prolog.logic.equivalent
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable

tests/prolog/builtins/ArithmeticOperatorsTests.kt

@@ -0,0 +1,426 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.*
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.assertThrows
+import prolog.ast.terms.Integer
+import prolog.ast.terms.Variable
+import prolog.logic.between
+import prolog.logic.equivalent
+
+class ArithmeticOperatorsTests {
+    @Test
+    fun `1 evaluates to 1`() {
+        val op1 = EvaluatesTo(
+            Integer(1),
+            Integer(1)
+        )
+
+        var result = op1.evaluate(emptyMap()).first
+
+        assertEquals(True, result, "1 should be equal to 1")
+
+        val op2 = EvaluatesToDifferent(
+            Integer(1),
+            Integer(1)
+        )
+
+        result = op2.evaluate(emptyMap()).first
+
+        assertEquals(False, result, "1 should not be different from 1")
+    }
+
+    @Test
+    fun `1 does not evaluate to 2`() {
+        val op1 = EvaluatesTo(
+            Integer(1),
+            Integer(2)
+        )
+
+        var result = op1.evaluate(emptyMap()).first
+
+        assertEquals(False, result, "1 should not be equal to 2")
+        
+        val op2 = EvaluatesToDifferent(
+            Integer(1),
+            Integer(2)
+        )
+
+        result = op2.evaluate(emptyMap()).first
+
+        assertEquals(True, result, "1 should be different from 2")
+    }
+
+    @Test
+    fun `2 + 3 evaluates to 5`() {
+        val op = EvaluatesTo(
+            Add(Integer(2), Integer(3)),
+            Integer(5)
+        )
+
+        var result = op.evaluate(emptyMap()).first
+
+        assertEquals(True, result, "2 + 3 should be equal to 5")
+
+        val op2 = EvaluatesToDifferent(
+            Add(Integer(2), Integer(3)),
+            Integer(5)
+        )
+
+        result = op2.evaluate(emptyMap()).first
+
+        assertEquals(False, result, "2 + 3 should not be different from 5")
+    }
+
+    @Test
+    fun `2 + 3 evaluates to 4 + 1`() {
+        val op = EvaluatesTo(
+            Add(Integer(2), Integer(3)),
+            Add(Integer(4), Integer(1))
+        )
+
+        var result = op.evaluate(emptyMap()).first
+
+        assertEquals(True, result, "2 + 3 should be equal to 4 + 1")
+
+        val op2 = EvaluatesToDifferent(
+            Add(Integer(2), Integer(3)),
+            Add(Integer(4), Integer(1))
+        )
+
+        result = op2.evaluate(emptyMap()).first
+
+        assertEquals(False, result, "2 + 3 should not be different from 4 + 1")
+    }
+
+    @Test
+    fun `1 evaluates to variable not sufficiently instantiated`() {
+        val op = EvaluatesTo(
+            Integer(1),
+            Variable("X")
+        )
+
+        assertThrows<IllegalArgumentException> { op.evaluate(emptyMap()) }
+
+        val op2 = EvaluatesToDifferent(
+            Integer(1),
+            Variable("X")
+        )
+
+        assertThrows<IllegalArgumentException> { op2.evaluate(emptyMap()) }
+    }
+
+    @Test
+    fun `(1 + var) evaluates to 1 not sufficiently instantiated`() {
+        val op = EvaluatesTo(
+            Add(Integer(1), Variable("X")),
+            Integer(1)
+        )
+
+        assertThrows<IllegalArgumentException> { op.evaluate(emptyMap()) }
+
+        val op2 = EvaluatesToDifferent(
+            Add(Integer(1), Variable("X")),
+            Integer(1)
+        )
+
+        assertThrows<IllegalArgumentException> { op2.evaluate(emptyMap()) }
+    }
+
+    @Test
+    fun `1 is 1`() {
+        val op = Is(
+            Integer(1),
+            Integer(1)
+        )
+
+        val result = op.prove(emptyMap())
+
+        assertTrue(result.any(), "1 should be equal to 1")
+    }
+
+    @Test
+    fun `1 is not 2`() {
+        val op = Is(
+            Integer(1),
+            Integer(2)
+        )
+
+        val result = op.prove(emptyMap()).toList()
+
+        assertTrue(result.isEmpty(), "1 should not be equal to 2")
+    }
+
+    @Test
+    fun `bound-to-1-var is 1`() {
+        val t1 = Variable("X")
+        val op = Is(
+            t1,
+            Integer(1)
+        )
+
+        t1.bind(Integer(1))
+
+        val result = op.prove(emptyMap())
+
+        assertTrue(result.any(), "X should be equal to 1")
+        assertTrue(result.first().isEmpty(), "X should not be rebound")
+    }
+
+    @Test
+    fun `bound-to-2-var is not 1`() {
+        val t1 = Variable("X")
+        val op = Is(
+            t1,
+            Integer(1)
+        )
+
+        t1.bind(Integer(2))
+
+        val result = op.prove(emptyMap())
+
+        assertFalse(result.any(), "X should not be equal to 1")
+    }
+
+    @Test
+    fun `variable is 1`() {
+        val op = Is(
+            Variable("X"),
+            Integer(1)
+        )
+
+        val result = op.prove(emptyMap()).toList()
+
+        assertFalse(result.isEmpty(), "X should be equal to 1")
+        assertEquals(1, result[0].size, "X should be rebound")
+        assertTrue(equivalent(Integer(1), result[0][Variable("X")]!!), "X should be equal to 1")
+    }
+
+    @Test
+    fun `variable is 1 + 2`() {
+        val op = Is(
+            Variable("X"),
+            Add(Integer(1), Integer(2))
+        )
+
+        val result = op.prove(emptyMap()).toList()
+
+        assertFalse(result.isEmpty(), "X should be equal to 3")
+        assertEquals(1, result[0].size, "X should be rebound")
+        assertTrue(equivalent(Integer(3), result[0][Variable("X")]!!), "X should be equal to 3")
+    }
+
+    @Test
+    fun `var is var should throw`() {
+        val op = Is(
+            Variable("X"),
+            Variable("Y")
+        )
+
+        assertThrows<IllegalArgumentException> { op.prove(emptyMap()) }
+    }
+
+    @Test
+    fun `1 is var should throw`() {
+        val op = Is(
+            Integer(1),
+            Variable("X")
+        )
+
+        assertThrows<IllegalArgumentException> { op.prove(emptyMap()) }
+    }
+
+    @Test
+    fun `var is bound-to-sum-var`() {
+        val t1 = Variable("X")
+        val t2 = Variable("Y")
+
+        t2.bind(Add(Integer(1), Integer(2)))
+
+        val op = Is(t1, t2)
+
+        val result = op.prove(emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "X should be equal to 3")
+        assertEquals(1, result[0].size, "X should be rebound, Y should not")
+        assertTrue(equivalent(Integer(3), result[0][t1]!!), "X should be equal to 3")
+    }
+
+    /**
+     * ?- between(1, 2, X), Y is 1 + X.
+     * X = 1, Y = 2 ;
+     * X = 2, Y = 3 .
+     */
+    @Test
+    fun `between 1 and 2 plus 1 to get 2 and 3`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Variable("X")
+        val t4 = Variable("Y")
+
+        val op = Conjunction(
+            Between(t1, t2, t3),
+            Is(t4, Add(Integer(1), t3))
+        )
+    }
+
+    @Test
+    fun `negate 1 to get -1`() {
+        val t1 = Integer(1)
+
+        val result = Negate(t1).evaluate(emptyMap()).first
+
+        assertEquals(Integer(-1), result, "negate(1) should be equal to -1")
+    }
+
+    @Test
+    fun `negate 0 to get 0`() {
+        val t1 = Integer(0)
+
+        val result = Negate(t1).evaluate(emptyMap()).first
+
+        assertEquals(Integer(0), result, "negate(0) should be equal to 0")
+    }
+
+    @Test
+    fun `negate -1 to get 1`() {
+        val t1 = Integer(-1)
+
+        val result = Negate(t1).evaluate(emptyMap()).first
+
+        assertEquals(Integer(1), result, "negate(-1) should be equal to 1")
+    }
+
+    @Test
+    fun `negate bound-to-1-var to get -1`() {
+        val t1 = Variable("X")
+
+        t1.bind(Integer(1))
+
+        val result = Negate(t1).evaluate(emptyMap()).first
+
+        assertEquals(Integer(-1), result, "negate(1) should be equal to -1")
+    }
+
+    @Test
+    fun `negate bound-to-1-var to get -1 by map`() {
+        val t1 = Variable("X")
+
+        val result = Negate(t1).evaluate(mapOf(t1 to Integer(1))).first
+
+        assertEquals(Integer(-1), result, "negate(1) should be equal to -1")
+    }
+
+    @Test
+    fun `negate 1 + 3 to get -4`() {
+        val t1 = Integer(1)
+        val t2 = Integer(3)
+
+        val result = Negate(Add(t1, t2)).evaluate(emptyMap()).first
+
+        assertEquals(Integer(-4), result, "negate(1 + 3) should be equal to -4")
+    }
+
+    @Test
+    fun `Add 1 and 2 to get 3`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+
+        val result = Add(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(3), result, "1 + 2 should be equal to 3")
+    }
+
+    @Test
+    fun `Add 1 and bound-to-2-var to get 3`() {
+        val t1 = Integer(1)
+        val t2 = Variable("X")
+
+        t2.bind(Integer(2))
+
+        val result = Add(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(3), result, "1 + 2 should be equal to 3")
+    }
+
+    @Test
+    fun `Add 1 and bound-to-2-var to get 3 by map`() {
+        val t1 = Integer(1)
+        val t2 = Variable("X")
+
+        val result = Add(t1, t2).evaluate(mapOf(t2 to Integer(2))).first
+
+        assertEquals(Integer(3), result, "1 + 2 should be equal to 3")
+    }
+
+    @Test
+    fun `Subtract 1 and 2 to get -1`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+
+        val result = Subtract(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(-1), result, "1 - 2 should be equal to -1")
+    }
+
+    @Test
+    fun `Subtract 3 and 1 to get 2`() {
+        val t1 = Integer(3)
+        val t2 = Integer(1)
+
+        val result = Subtract(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(2), result, "3 - 1 should be equal to 2")
+    }
+
+    @Test
+    fun `Multiply 0 and 0 to get 0`() {
+        val t1 = Integer(0)
+        val t2 = Integer(0)
+
+        val result = Multiply(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(0), result, "0 * 0 should be equal to 0")
+    }
+
+    @Test
+    fun `Multiply 1 and 0 to get 0`() {
+        val t1 = Integer(1)
+        val t2 = Integer(0)
+
+        val result = Multiply(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(0), result, "1 * 0 should be equal to 0")
+    }
+
+    @Test
+    fun `Multiply 0 and 1 to get 0`() {
+        val t1 = Integer(0)
+        val t2 = Integer(1)
+
+        val result = Multiply(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(0), result, "0 * 1 should be equal to 0")
+    }
+
+    @Test
+    fun `Multiply 3 and 1 to get 3`() {
+        val t1 = Integer(3)
+        val t2 = Integer(1)
+
+        val result = Multiply(t1, t2).evaluate(emptyMap()).first
+
+        assertEquals(Integer(3), result, "3 * 1 should be equal to 3")
+    }
+
+    @Test
+    fun `Multiply 2 and 3 to get 6`() {
+        val t1 = Integer(2)
+        val t2 = Integer(3)
+
+        val result = Multiply(t1, t2).evaluate(emptyMap()).toList()
+
+        assertEquals(1, result.size, "There should only be one solution")
+        assertEquals(Integer(6), result, "2 * 3 should be equal to 6")
+    }
+}

tests/prolog/builtins/ControlTest.kt

@@ -8,7 +8,7 @@ import prolog.Program
 import prolog.ast.logic.Fact
 import prolog.ast.terms.Atom
 
-class ControlBuiltinsTest {
+class ControlTest {
     @BeforeEach
     fun setUp() {
         Program.clear()
@@ -55,7 +55,7 @@ class ControlBuiltinsTest {
         Program.load(listOf(success, failure))
 
         val goal = Atom("a")
-        val failGoal = Fail()
+        val failGoal = Fail
 
         val result1 = Program.query(goal)
         val result2 = Program.query(failGoal)

tests/prolog/builtins/TermAnalysisConstructionTest.kt

@@ -5,6 +5,8 @@ import org.junit.jupiter.api.Assertions.assertTrue
 import org.junit.jupiter.api.Test
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
+import prolog.logic.atomic
+import prolog.logic.compound
 
 /**
  * Based on [Predicates for analyzing/constructing terms](https://github.com/dtonhofer/prolog_notes/blob/master/swipl_notes/about_term_analysis_and_construction/term_analysis_construction.png)

tests/prolog/builtins/UnificationTest.kt

@@ -0,0 +1,52 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.*
+import org.junit.jupiter.api.Test
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Integer
+import prolog.ast.terms.Variable
+
+class UnificationTest {
+    /**
+     * ?- X == a.
+     * false.
+     */
+    @Test
+    fun equivalent_variable_and_atom() {
+        val variable = Variable("X")
+        val atom = Atom("a")
+
+        val result = Equivalent(variable, atom).prove(emptyMap())
+
+        assertFalse(result.any(), "Variable and atom should not be equivalent")
+    }
+
+    /**
+     * ?- a == a.
+     * true.
+     */
+    @Test
+    fun equivalent_atom_and_atom() {
+        val atom1 = Atom("a")
+        val atom2 = Atom("a")
+
+        val result = Equivalent(atom1, atom2).prove(emptyMap())
+
+        assertTrue(result.any(), "Identical atoms should be equivalent")
+        assertEquals(0, result.first().size, "No substitutions should be made")
+    }
+
+    /**
+     * ?- 1 + 2 == 3.
+     * false.
+     */
+    @Test
+    fun simple_addition_equivalence() {
+        val addition = Add(Integer(1), Integer(2))
+        val solution = Integer(3)
+
+        val result = Equivalent(addition, solution).prove(emptyMap())
+
+        assertFalse(result.any(), "Addition should be equivalent")
+    }
+}

tests/prolog/builtins/VerificationTest.kt

@@ -6,9 +6,12 @@ import org.junit.jupiter.api.Test
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
+import prolog.logic.compound
+import prolog.logic.nonvariable
+import prolog.logic.variable
 import kotlin.test.assertEquals
 
-class VerificationBuiltinsTest {
+class VerificationTest {
     @Test
     fun unbound_variable_is_var() {
         val variable = Variable("X")

tests/prolog/logic/ArithmeticTests.kt

@@ -0,0 +1,357 @@
+package prolog.logic
+
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.assertThrows
+import prolog.ast.terms.Integer
+import prolog.ast.terms.Term
+import prolog.ast.terms.Variable
+
+class ArithmeticTests {
+    @Test
+    fun `1_between_0_and_2`() {
+        val result = between(Integer(0), Integer(2), Integer(1))
+
+        assertTrue(result.any(), "Expected 1 to be between 0 and 2")
+        assertEquals(emptyMap<Variable, Term>(), result.first(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `3_not_between_0_and_2`() {
+        val result = between(Integer(0), Integer(2), Integer(3))
+
+        assertTrue(result.none(), "Expected 3 not to be between 0 and 2")
+    }
+
+    @Test
+    fun numbers_between_0_and_2() {
+        val result = between(Integer(0), Integer(2), Variable("X"))
+
+        val expectedResults = listOf(
+            mapOf(Variable("X") to Integer(0)),
+            mapOf(Variable("X") to Integer(1)),
+            mapOf(Variable("X") to Integer(2))
+        )
+
+        val actualResults = result.toList()
+        assertEquals(expectedResults.size, actualResults.size, "Expected 3 results")
+        for ((expected, actual) in expectedResults.zip(actualResults)) {
+            for ((key, value) in expected) {
+                assertTrue(actual.containsKey(key), "Expected key $key to be present")
+                assertTrue(
+                    equivalent(value, actual[key]!!),
+                    "Expected value $value for key $key, but got ${actual[key]}"
+                )
+            }
+        }
+    }
+
+    @Test
+    fun `succ(0) is 1`() {
+        val t1 = Integer(0)
+
+        val expected = Integer(1)
+
+        val result = succ(t1, expected, emptyMap())
+
+        assertTrue(result.any(), "Expected 0 + 1 to be equal to 1")
+        assertTrue(result.first().isEmpty(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `succ(1) is 2`() {
+        val t1 = Integer(1)
+
+        val expected = Integer(2)
+
+        val result = succ(t1, expected, emptyMap())
+
+        assertTrue(result.any(), "Expected 1 + 1 to be equal to 2")
+        assertTrue(result.first().isEmpty(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `succ(1) is var`() {
+        val t1 = Integer(1)
+        val t2 = Variable("X")
+
+        val expected = Integer(2)
+
+        val result = succ(t1, t2, emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "Expected 1 + 1 to be equal to X")
+        assertTrue(result[0][t2] == expected, "Expected X to be equal to 2")
+    }
+
+    @Test
+    fun `succ(bound-to-1-var) is 2`() {
+        val t1 = Variable("X")
+        val t2 = Integer(2)
+
+        t1.bind(Integer(1))
+
+        val result = succ(t1, t2, emptyMap())
+
+        assertTrue(result.any(), "Expected X + 1 to be equal to 2")
+        assertTrue(result.first().isEmpty(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `succ(bound-to-1-var) is 2 by map`() {
+        val t1 = Variable("X")
+        val t2 = Integer(2)
+
+        val result = succ(t1, t2, mapOf(t1 to Integer(1)))
+
+        assertTrue(result.any(), "Expected X + 1 to be equal to 2")
+        assertTrue(result.first().isEmpty(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `succ(bound-to-1-var) is var`() {
+        val t1 = Variable("X")
+        val t2 = Variable("Y")
+
+        t1.bind(Integer(1))
+
+        val result = succ(t1, t2, emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "Expected X + 1 to be equal to Y")
+        assertTrue(result[0][t2] == Integer(2), "Expected Y to be equal to 2")
+    }
+
+    @Test
+    fun `succ(bound-to-1-var) is var by map`() {
+        val t1 = Variable("X")
+        val t2 = Variable("Y")
+
+        val result = succ(t1, t2, mapOf(t1 to Integer(1))).toList()
+
+        assertTrue(result.isNotEmpty(), "Expected X + 1 to be equal to Y")
+        assertTrue(result[0][t2] == Integer(2), "Expected Y to be equal to 2")
+    }
+
+    @Test
+    fun `succ(var, 0) fails silently`() {
+        val t1 = Variable("X")
+        val t2 = Integer(0)
+
+        val result = succ(t1, t2, emptyMap()).toList()
+
+        assertTrue(result.isEmpty(), "Expected X + 1 to fail")
+    }
+
+    @Test
+    fun `1_plus_2_is_3`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Integer(3)
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.any(), "1 + 2 should be equal to 3")
+        assertTrue(result.first().isEmpty(), "1 + 2 should be equal to 3")
+    }
+
+    @Test
+    fun `1_plus_2_is_not_4`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Integer(4)
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.none(), "1 + 2 should not be equal to 4")
+    }
+
+    @Test
+    fun `1_plus_2_is_variable`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Variable("X")
+
+        val result = plus(t1, t2, t3, emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "1 + 2 should be equal to X")
+        assertTrue(equivalent(result[0][t3]!!, Integer(3)), "X should be equal to 3")
+    }
+
+    @Test
+    fun `1_plus_variable_is_3`() {
+        val t1 = Integer(1)
+        val t2 = Variable("X")
+        val t3 = Integer(3)
+
+        val result = plus(t1, t2, t3, emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "1 + X should be equal to 3")
+        assertTrue(equivalent(result[0][t2]!!, Integer(2)), "X should be equal to 2")
+    }
+
+    @Test
+    fun variable_plus_2_is_3() {
+        val t1 = Variable("X")
+        val t2 = Integer(2)
+        val t3 = Integer(3)
+
+        val result = plus(t1, t2, t3, emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "X + 2 should be equal to 3")
+        assertTrue(equivalent(result[0][t1]!!, Integer(1)), "X should be equal to 1")
+    }
+
+    @Test
+    fun `1 plus 2 is bound-to-3-var`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Variable("X")
+
+        t3.bind(Integer(3))
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.any(), "1 + 2 should be equal to X")
+        assertTrue(result.first().isEmpty(), "t3 should not be rebound")
+    }
+
+    @Test
+    fun `1 plus 2 is bound-to-3-var by map`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Variable("X")
+
+        val result = plus(t1, t2, t3, mapOf(Variable("X") to Integer(3)))
+
+        assertTrue(result.any(), "1 + 2 should be equal to X")
+        assertTrue(result.first().isEmpty(), "t3 should not be rebound")
+    }
+
+    @Test
+    fun `1 plus 2 is bound-to-4-var`() {
+        val t1 = Integer(1)
+        val t2 = Integer(2)
+        val t3 = Variable("X")
+
+        t3.bind(Integer(4))
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.none(), "1 + 2 should not be equal to X")
+    }
+
+    @Test
+    fun `1 plus bound-to-2-var is 3`() {
+        val t1 = Integer(1)
+        val t2 = Variable("X")
+        val t3 = Integer(3)
+
+        t2.bind(Integer(2))
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.any(), "1 + X should be equal to 3")
+        assertTrue(result.first().isEmpty(), "t2 should not be rebound")
+    }
+
+    @Test
+    fun `1 plus bound-to-2-var is not 4`() {
+        val t1 = Integer(1)
+        val t2 = Variable("X")
+        val t3 = Integer(4)
+
+        t2.bind(Integer(2))
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.none(), "1 + X should not be equal to 4")
+    }
+
+    @Test
+    fun `bound-to-1-var plus 2 is 3`() {
+        val t1 = Variable("X")
+        val t2 = Integer(2)
+        val t3 = Integer(3)
+
+        t1.bind(Integer(1))
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.any(), "X + 2 should be equal to 3")
+        assertTrue(result.first().none(), "t1 should not be rebound")
+    }
+
+    @Test
+    fun `bound-to-1-var plus 2 is not 4`() {
+        val t1 = Variable("X")
+        val t2 = Integer(2)
+        val t3 = Integer(4)
+
+        t1.bind(Integer(1))
+
+        val result = plus(t1, t2, t3, emptyMap())
+
+        assertTrue(result.none(), "X + 2 should not be equal to 4")
+    }
+
+    @Test
+    fun `two unbound vars plus should throw`() {
+        val t1 = Variable("X")
+        val t2 = Variable("Y")
+        val t3 = Integer(3)
+
+        assertThrows<IllegalArgumentException> {
+            plus(t1, t2, t3, emptyMap())
+        }
+    }
+
+    @Test
+    fun `bound-to-1-var plus bound-to-2-var is variable`() {
+        val t1 = Variable("X")
+        val t2 = Variable("Y")
+        val t3 = Variable("Z")
+
+        t1.bind(Integer(1))
+        t2.bind(Integer(2))
+
+        val result = plus(t1, t2, t3, emptyMap()).toList()
+
+        assertTrue(result.isNotEmpty(), "X + Y should be equal to Z")
+        assertTrue(equivalent(result[0][t3]!!, Integer(3)), "Z should be equal to 3")
+    }
+
+    @Test
+    fun `1 times 1 is 1`() {
+        val t1 = Integer(1)
+        val t2 = Integer(1)
+        val t3 = Integer(1)
+
+        val result = mul(t1, t2, t3, emptyMap()).toList()
+
+        assertEquals(1, result.size, "There should be one solution")
+        assertTrue(result[0].isEmpty(), "1 * 1 should already be equal to 1")
+    }
+
+    @Test
+    fun `2 times 3 is 6`() {
+        val t1 = Integer(2)
+        val t2 = Integer(3)
+        val t3 = Integer(6)
+
+        val result = mul(t1, t2, t3, emptyMap()).toList()
+
+        assertEquals(1, result.size, "There should be one solution")
+        assertTrue(result[0].isEmpty(), "2 * 3 should already be equal to 6")
+    }
+
+    @Test
+    fun `2 times 3 is not 4`() {
+        val t1 = Integer(2)
+        val t2 = Integer(3)
+        val t3 = Integer(4)
+
+        val result = mul(t1, t2, t3, emptyMap())
+
+        assertTrue(result.none(), "2 * 3 should not be equal to 4")
+    }
+}

tests/prolog/logic/UnifyTest.kt

@@ -3,10 +3,10 @@ package prolog.logic
 import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
+import prolog.ast.terms.Integer
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
-import prolog.builtins.equivalent
 
 /*
  * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
@@ -260,4 +260,25 @@ class UnifyTest {
 
         assertFalse(result.isPresent, "Atom with different arity should not unify")
     }
+
+    @Test
+    fun identical_integers_unify() {
+        val int1 = Integer(1)
+        val int2 = Integer(1)
+
+        val result = unify(int1, int2)
+
+        assertTrue(result.isPresent, "Identical integers should unify")
+        assertEquals(0, result.get().size, "No substitutions should be made")
+    }
+
+    @Test
+    fun different_integers_do_not_unify() {
+        val int1 = Integer(1)
+        val int2 = Integer(2)
+
+        val result = unify(int1, int2)
+
+        assertFalse(result.isPresent, "Different integers should not unify")
+    }
 }