diff --git a/docs/source/frame/knowledge_base/demonstrations.rst b/docs/source/frame/knowledge_base/demonstrations.rst
index c500547..d03b974 100644
--- a/docs/source/frame/knowledge_base/demonstrations.rst
+++ b/docs/source/frame/knowledge_base/demonstrations.rst
@@ -13,7 +13,7 @@ It contains implementations of:
 Each concept is defined with:
 - Symbolic representation using the expression framework
 - Computational implementation for concrete evaluation
-- Translation rules for different target languages (Lean 4, Prolog, Z3)
+- Translation rules for different target languages (Lean 4, Z3)
 - Example management and testing infrastructure
 
 The module also includes comprehensive tests and demonstrations that can be run directly.
diff --git a/frame/environments/math_env.py b/frame/environments/math_env.py
index 4af8617..0b9c14f 100644
--- a/frame/environments/math_env.py
+++ b/frame/environments/math_env.py
@@ -379,7 +379,6 @@ def step(self, action: Union[int, ValidAction], is_simulation: bool = False) ->
                                     proof=cached_proof,
                                     example_structure=new_entity.examples.example_structure,
                                     lean4_translation=new_entity._lean4,
-                                    prolog_translation=new_entity._prolog,
                                     z3_translation=new_entity._z3,
                                     computational_implementation=new_entity._compute,
                                     can_add_examples=new_entity.can_add_examples,
@@ -409,7 +408,6 @@ def step(self, action: Union[int, ValidAction], is_simulation: bool = False) ->
                                         proof=proof,
                                         example_structure=new_entity.examples.example_structure,
                                         lean4_translation=new_entity._lean4,
-                                        prolog_translation=new_entity._prolog,
                                         z3_translation=new_entity._z3,
                                         computational_implementation=new_entity._compute,
                                         can_add_examples=new_entity.can_add_examples,
@@ -460,7 +458,6 @@ def step(self, action: Union[int, ValidAction], is_simulation: bool = False) ->
                                         proof=proof,
                                         example_structure=new_entity.examples.example_structure,
                                         lean4_translation=new_entity._lean4,
-                                        prolog_translation=new_entity._prolog,
                                         z3_translation=new_entity._z3,
                                         computational_implementation=new_entity._compute,
                                         can_add_examples=new_entity.can_add_examples,
diff --git a/frame/knowledge_base/demonstrations.py b/frame/knowledge_base/demonstrations.py
index 2446589..963879b 100644
--- a/frame/knowledge_base/demonstrations.py
+++ b/frame/knowledge_base/demonstrations.py
@@ -11,7 +11,7 @@
 Each concept is defined with:
 - Symbolic representation using the expression framework
 - Computational implementation for concrete evaluation
-- Translation rules for different target languages (Lean 4, Prolog, Z3)
+- Translation rules for different target languages (Lean 4, Z3)
 - Example management and testing infrastructure
 
 The module also includes comprehensive tests and demonstrations that can be run directly.
@@ -39,7 +39,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b: f"({a} + {b})",
-    prolog_translation=lambda a, b: f"plus({a}, {b}, Result)",
     z3_translation=lambda a, b: f"(+ {a} {b})",
 )
 
@@ -53,7 +52,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b: f"({a} * {b})",
-    prolog_translation=lambda a, b: f"times({a}, {b}, Result)",
     z3_translation=lambda a, b: f"(* {a} {b})",
 )
 
@@ -71,7 +69,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b: f"(∃ n : ℕ, {b} = {a} * n)",
-    prolog_translation=lambda a, b: f"(0 is {b} mod {a})",
     z3_translation=lambda a, b: f"(exists ((n Int)) (= {b} (* {a} n)))",
 )
 
@@ -85,7 +82,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b, ctx=None: f"({a} < {b})",
-    prolog_translation=lambda a, b: f"({a} < {b})",
     z3_translation=lambda a, b: f"(< {a} {b})",
 )
 
@@ -113,7 +109,6 @@
         input_arity=1,
     ),
     lean4_translation=lambda n: f"(Nat.Prime {n})",
-    prolog_translation=lambda n: f"is_prime({n})",
     z3_translation=lambda n: f"""
 n := Exec({n.to_z3()})
 x := NatVar();
@@ -164,7 +159,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b, ctx=None: f"({a} ≤ {b})",
-    prolog_translation=lambda a, b: f"({a} =< {b})",
     z3_translation=lambda a, b: f"(<= {a} {b})",
 )
 
@@ -178,7 +172,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b: f"({a} > {b})",
-    prolog_translation=lambda a, b: f"({a} > {b})",
     z3_translation=lambda a, b: f"(> {a} {b})",
 )
 
@@ -192,7 +185,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda a, b: f"({a} ≥ {b})",
-    prolog_translation=lambda a, b: f"({a} >= {b})",
     z3_translation=lambda a, b: f"(>= {a} {b})",
 )
 
@@ -269,7 +261,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda A, B: f"({A} ∪ {B})",
-    prolog_translation=lambda A, B: f"union({A}, {B}, Result)",
     z3_translation=lambda A, B: f"(union {A} {B})",
 )
 
@@ -284,7 +275,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda A, B: f"({A} ∩ {B})",
-    prolog_translation=lambda A, B: f"intersection({A}, {B}, Result)",
     z3_translation=lambda A, B: f"(inter {A} {B})",
 )
 
@@ -299,7 +289,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda A, B: f"({A} \\ {B})",
-    prolog_translation=lambda A, B: f"subtract({A}, {B}, Result)",
     z3_translation=lambda A, B: f"(setminus {A} {B})",
 )
 
@@ -314,7 +303,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda A, B: f"(({A} \\ {B}) ∪ ({B} \\ {A}))",
-    prolog_translation=lambda A, B: f"symmetric_difference({A}, {B}, Result)",
     z3_translation=lambda A, B: f"(union (setminus {A} {B}) (setminus {B} {A}))",
 )
 
@@ -329,7 +317,6 @@
         input_arity=2,
     ),
     lean4_translation=lambda A, B: f"({A} ⊆ {B})",
-    prolog_translation=lambda A, B: f"subset({A}, {B})",
     z3_translation=lambda A, B: f"(subset {A} {B})",
 )
 
@@ -378,7 +365,6 @@
         input_arity=1,
     ),
     lean4_translation=lambda grp: f"|{grp.carrier.to_lean4()}|",
-    prolog_translation=lambda grp: f"group_cardinality({grp.carrier.to_prolog()}, Result)",
     z3_translation=lambda grp: f"(cardinality {grp.carrier.to_z3()})",
 )
 
@@ -418,6 +404,5 @@
         input_arity=3,
     ),
     lean4_translation=lambda grp, g, x: f"({g} * {x} * {grp.inverse(g)})",
-    prolog_translation=lambda grp, g, x: f"conjugate({grp.to_prolog()}, {g}, {x}, Result)",
     z3_translation=lambda grp, g, x: f"(conjugate {grp.to_z3()} {g} {x})",
 )
diff --git a/frame/knowledge_base/entities.py b/frame/knowledge_base/entities.py
index d64941f..012d756 100644
--- a/frame/knowledge_base/entities.py
+++ b/frame/knowledge_base/entities.py
@@ -21,13 +21,12 @@
 
 Each expression type supports translation to multiple target languages:
 - Lean 4 theorem prover
-- Prolog logic programming
 - Z3 SMT solver
 
 Each mathematical entity supports:
 - Symbolic definitions using the expression framework
 - Computational implementations for concrete evaluation
-- Translation to multiple target languages (Lean 4, Prolog, Z3)
+- Translation to multiple target languages (Lean 4, Z3)
 - Example management with automatic validation
 - Metadata and documentation
 
@@ -84,11 +83,6 @@ def to_lean4(self) -> str:
         """Return a Lean 4 representation."""
         pass
 
-    @abstractmethod
-    def to_prolog(self) -> str:
-        """Return a Prolog representation."""
-        pass
-
     @abstractmethod
     def to_z3(self) -> Z3Template:
         """Return a Z3 (Python API or SMT-LIB) representation."""
@@ -104,10 +98,6 @@ def __init__(self, name: str):
     def to_lean4(self) -> str:
         return self.name
 
-    def to_prolog(self) -> str:
-        # In Prolog, atoms are lowercase
-        return self.name.lower()
-
     def to_z3(self) -> Z3Template:
         raise NotImplementedError("to_z3 is not yet implemented")
 
@@ -128,9 +118,6 @@ def _filter_example_type(self, arg: Any) -> Any:
     def to_lean4(self) -> str:
         raise NotImplementedError("to_lean4 is not yet implemented")
 
-    def to_prolog(self) -> str:
-        raise NotImplementedError("to_prolog is not yet implemented")
-
     def to_z3(self) -> Z3Template:
         raise NotImplementedError("to_z3 is not yet implemented")
 
@@ -149,10 +136,6 @@ def __init__(self, name: str):
     def to_lean4(self) -> str:
         return self.name
 
-    def to_prolog(self) -> str:
-        # In Prolog, atoms are lowercase
-        return self.name.lower()
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -164,9 +147,6 @@ def __init__(self, expr: Expression):
     def to_lean4(self) -> str:
         return f"(¬ {self.expr.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        return f"not({self.expr.to_prolog()})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -181,11 +161,6 @@ def to_lean4(self) -> str:
         right = self.right.to_lean4()
         return f"({left} ∧ {right})"
 
-    def to_prolog(self) -> str:
-        left = self.left.to_prolog()
-        right = self.right.to_prolog()
-        return f"({left}, {right})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -198,9 +173,6 @@ def __init__(self, left: Expression, right: Expression):
     def to_lean4(self) -> str:
         return f"({self.left.to_lean4()} ∨ {self.right.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        return f"({self.left.to_prolog()}; {self.right.to_prolog()})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -213,10 +185,6 @@ def __init__(self, antecedent: Expression, consequent: Expression):
     def to_lean4(self) -> str:
         return f"({self.antecedent.to_lean4()} → {self.consequent.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        # Note: Prolog does not have a direct "implies" operator.
-        return f"implies({self.antecedent.to_prolog()}, {self.consequent.to_prolog()})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -242,11 +210,6 @@ def to_lean4(self) -> str:
         body = self.body.to_lean4()
         return f"(∀ {self.var} : {iterable}, {body})"
 
-    def to_prolog(self) -> str:
-        iterable = self.iterable.to_prolog()
-        body = self.body.to_prolog()
-        return f"forall({self.var}, {iterable}, {body})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -262,11 +225,6 @@ def to_lean4(self) -> str:
         body = self.body.to_lean4()
         return f"(∃ {self.var} : {domain}, {body})"
 
-    def to_prolog(self) -> str:
-        domain = self.domain.to_prolog()
-        body = self.body.to_prolog()
-        return f"exists({self.var}, {domain}, {body})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -308,15 +266,6 @@ def to_lean4(self) -> str:
             body = self.predicate.body.to_lean4()
             return f"{{x : {self.domain.to_lean4()} | {body}}}"
 
-    def to_prolog(self) -> str:
-        if self.elements is not None:
-            elems = ", ".join(e.to_prolog() for e in self.elements)
-            return f"[{elems}]"
-        else:
-            var = self.predicate.var_name
-            body = self.predicate.body.to_prolog()
-            return f"findall(X, ({body}), Set)"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -348,9 +297,6 @@ class SetDomain(Expression):
     def to_lean4(self) -> str:
         return "Set"
 
-    def to_prolog(self) -> str:
-        return "set"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -367,9 +313,6 @@ def __init__(self, domains: Tuple["Entity", ...]):
     def to_lean4(self, ctx: Optional[Any] = None) -> str:
         return " × ".join(d.to_lean4() for d in self.domains)
 
-    def to_prolog(self, ctx: Optional[Any] = None) -> str:
-        return f"tuple_domain({', '.join(d.to_prolog() for d in self.domains)})"
-
     def to_z3(self, ctx: Optional[Any] = None) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -384,9 +327,6 @@ def __init__(self, element: Expression, set_expr: Expression):
     def to_lean4(self) -> str:
         return f"({self.element.to_lean4()} ∈ {self.set_expr.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        return f"member({self.element.to_prolog()}, {self.set_expr.to_prolog()})"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -405,10 +345,6 @@ def to_lean4(self) -> str:
         set_str = self.set.to_lean4()
         return f"(Finset.card {set_str})"
 
-    def to_prolog(self) -> str:
-        set_str = self.set.to_prolog()
-        return f"length({set_str}, Len)"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -449,10 +385,6 @@ def to_lean4(self) -> str:
         set_str = self.set_expr.to_lean4()
         return f"(Finset.sum {set_str} id)"
 
-    def to_prolog(self) -> str:
-        set_str = self.set_expr.to_prolog()
-        return f"sum_list({set_str}, Sum)"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -490,9 +422,6 @@ class Zero(Expression):
     def to_lean4(self) -> str:
         return "0"
 
-    def to_prolog(self) -> str:
-        return "zero"
-
     def to_z3(self) -> Z3Template:
         return "0"
 
@@ -504,9 +433,6 @@ def __init__(self, n: Expression):
     def to_lean4(self) -> str:
         return f"(succ {self.n.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        return f"succ({self.n.to_prolog()})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -522,9 +448,6 @@ def __init__(self, value: int):
     def to_lean4(self) -> str:
         return str(self.value)  # Direct number representation
 
-    def to_prolog(self) -> str:
-        return str(self.value)
-
     def to_z3(self) -> Z3Template:
         return f"{self.value}"
 
@@ -563,10 +486,6 @@ def to_lean4(self) -> str:
         # This is a placeholder; a proper representation might involve a specific library.
         return f"FiniteField {self.order}"
 
-    def to_prolog(self) -> str:
-        """Return a Prolog representation of the finite field type."""
-        return f"finite_field_{self.order}"
-
     def to_z3(self) -> str:
         """Return a Z3 representation of the finite field type."""
         # This would typically be a custom sort in Z3.
@@ -633,9 +552,6 @@ def __hash__(self) -> int:
     def to_lean4(self) -> str:
         return str(self.value)
 
-    def to_prolog(self) -> str:
-        return str(self.value)
-
     # TODO(tsoukalas): See what this should actually be in SMT-LIB
     def to_z3(self) -> str:
         return str(self.value)
@@ -651,9 +567,6 @@ class NatDomain(Expression):
     def to_lean4(self) -> str:
         return "ℕ"  # Unicode for natural numbers
 
-    def to_prolog(self) -> str:
-        return "nat"
-
     def to_z3(self) -> str:
         return "NatSet"  # Z3 doesn't have built-in naturals, we use integers
 
@@ -664,9 +577,6 @@ class GroupDomain(Expression):
     def to_lean4(self) -> str:
         return "Group"
 
-    def to_prolog(self) -> str:
-        return "Unimplemented"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -677,9 +587,6 @@ class GroupElementDomain(Expression):
     def to_lean4(self) -> str:
         return "G"  # In Lean, groups are typically defined over a type 'G'
 
-    def to_prolog(self) -> str:
-        return "group_element"  # A clear Prolog atom for group elements
-
     def to_z3(self) -> str:
         # In Z3, group elements can be modeled as an uninterpreted sort 'G'
         return NotImplementedError("to_z3 is not yet implemented")
@@ -698,9 +605,6 @@ def __init__(self, domains: "Union[List[Entity], Tuple[Entity, ...]]"):
     def to_lean4(self) -> str:
         return " × ".join(d.to_lean4() for d in self.domains)
 
-    def to_prolog(self) -> str:
-        return f"tuple_domain({', '.join(d.to_prolog() for d in self.domains)})"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -720,11 +624,6 @@ def to_lean4(self) -> str:
         elements_str = ", ".join(e.to_lean4() for e in self.elements)
         return f"({elements_str})"
 
-    def to_prolog(self) -> str:
-        # In Prolog, tuples are represented using parentheses and commas
-        elements_str = ", ".join(e.to_prolog() for e in self.elements)
-        return f"({elements_str})"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -745,10 +644,6 @@ def to_lean4(self) -> str:
         body = self.body.to_lean4()
         return f"(λ {self.var_name} => {body})"
 
-    def to_prolog(self) -> str:
-        body = self.body.to_prolog()
-        return f"lambda({self.var_name}, {body})"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -763,9 +658,6 @@ def __init__(self, fn: Expression, arg: Expression):
     def to_lean4(self) -> str:
         return f"({self.fn.to_lean4()} {self.arg.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        return f"apply({self.fn.to_prolog()}, {self.arg.to_prolog()})"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -782,11 +674,6 @@ def to_lean4(self) -> str:
         right = self.right.to_lean4()
         return f"({left} = {right})"
 
-    def to_prolog(self) -> str:
-        left = self.left.to_prolog()
-        right = self.right.to_prolog()
-        return f"equals({left}, {right})"
-
     def to_z3(self) -> Z3Template:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -839,9 +726,6 @@ def __init__(self, count: Expression, base: Expression, step_fn: Expression):
     def to_lean4(self) -> str:
         return f"(fold {self.count.to_lean4()} {self.base.to_lean4()} {self.step_fn.to_lean4()})"
 
-    def to_prolog(self) -> str:
-        return f"fold({self.count.to_prolog()}, {self.base.to_prolog()}, {self.step_fn.to_prolog()})"
-
     def to_z3(self) -> str:
         # Z3 doesn't have direct fold, we'd need to use recursion/quantifiers
         return NotImplementedError("to_z3 is not yet implemented")
@@ -874,12 +758,6 @@ def to_lean4(self) -> str:
             return self.value.to_lean4()
         return str(self.value)
 
-    def to_prolog(self) -> str:
-        """Convert the group element to Prolog syntax."""
-        if hasattr(self.value, "to_prolog"):
-            return self.value.to_prolog()
-        return str(self.value)
-
     def to_z3(self) -> str:
         """Convert the group element to Z3 syntax."""
         return NotImplementedError("to_z3 is not yet implemented")
@@ -901,9 +779,6 @@ class GroupElementDomain(Expression):
     def to_lean4(self) -> str:
         return "G"  # In Lean4, group elements are of type G
 
-    def to_prolog(self) -> str:
-        return "G"  # In Prolog, group elements are of type G
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -929,14 +804,6 @@ def to_lean4(self) -> str:
         else:
             return f"{{x : {self.domain.to_lean4()}}}"
 
-    def to_prolog(self) -> str:
-        if self.elements is not None:
-            return f"[{', '.join(e.to_prolog() for e in self.elements)}]"
-        elif self.predicate is not None:
-            return f"{{X : {self.domain.to_prolog()} | {self.predicate.to_prolog()}}}"
-        else:
-            return f"{{X : {self.domain.to_prolog()}}}"
-
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
@@ -1046,13 +913,7 @@ def to_lean4(self) -> str:
             f"{self.inverse.to_lean4() if hasattr(self.inverse, 'to_lean4') else self.inverse})"
         )
 
-    def to_prolog(self) -> str:
-        return (
-            f"group({self.carrier.to_prolog()}, "
-            f"{self.op.to_prolog() if hasattr(self.op, 'to_prolog') else self.op}, "
-            f"{self.identity.to_prolog() if hasattr(self.identity, 'to_prolog') else self.identity}, "
-            f"{self.inverse.to_prolog() if hasattr(self.inverse, 'to_prolog') else self.inverse})"
-        )
+
 
     def to_z3(self) -> str:
         return (
@@ -1250,9 +1111,6 @@ class GroupDomain(Expression):
     def to_lean4(self) -> str:
         return "Group"
 
-    def to_prolog(self) -> str:
-        return "Unimplemented"
-
     def to_z3(self) -> str:
         return "Unimplemented"
 
@@ -1267,9 +1125,6 @@ def __init__(self, domain: Expression, codomain: Expression):
     def to_lean4(self) -> str:
         return f"{self.domain.to_lean4()} → {self.codomain.to_lean4()}"
 
-    def to_prolog(self) -> str:
-        return f"function({self.domain.to_prolog()}, {self.codomain.to_prolog()})"
-
     def to_z3(self) -> str:
         return f"(Array {self.domain.to_z3()} {self.codomain.to_z3()})"
 
@@ -1804,7 +1659,6 @@ def __init__(
         computational_implementation: callable,
         example_structure: "Optional[ExampleStructure]" = None,
         lean4_translation: "Optional[callable]" = None,
-        prolog_translation: "Optional[callable]" = None,
         z3_translation: "Optional[callable]" = None,
         can_add_examples: bool = True,  # NOTE: These names are provisional and may change
         can_add_nonexamples: bool = True,  # NOTE: These names are provisional and may change
@@ -1817,7 +1671,6 @@ def __init__(
             computational_implementation is not None
         )
         self._lean4 = lean4_translation
-        self._prolog = prolog_translation
         self._z3 = z3_translation
         self._has_z3_translation = z3_translation is not None # Added flag
         self.examples = ExampleCollection(example_structure)
@@ -1986,13 +1839,6 @@ def to_lean4(
         """Returns Lean 4 translation."""
         raise NotImplementedError("to_lean4 is not yet implemented")
 
-    def to_prolog(
-        self,
-        *args,
-    ) -> str:
-        """Returns Prolog translation."""
-        raise NotImplementedError("to_prolog is not yet implemented")
-
     def to_z3(
         self,
         *args,
@@ -2095,7 +1941,6 @@ def __init__(
         computational_implementation: callable,
         example_structure: ExampleStructure,
         lean4_translation: "Optional[callable]" = None,
-        prolog_translation: "Optional[callable]" = None,
         z3_translation: "Optional[callable]" = None,
         can_add_examples: bool = True,
         can_add_nonexamples: bool = True,
@@ -2106,7 +1951,6 @@ def __init__(
             computational_implementation,
             example_structure,
             lean4_translation,
-            prolog_translation,
             z3_translation,
             can_add_examples,
             can_add_nonexamples,
@@ -2129,7 +1973,6 @@ def __init__(
         description: str,
         example_structure: "Optional[ExampleStructure]" = None,
         lean4_translation: "Optional[callable]" = None,
-        prolog_translation: "Optional[callable]" = None,
         z3_translation: "Optional[callable]" = None,
         computational_implementation: callable = None,
         can_add_examples: bool = True,
@@ -2145,7 +1988,6 @@ def __init__(
             computational_implementation,
             example_structure,
             lean4_translation,
-            prolog_translation,
             z3_translation,
             can_add_examples,
             can_add_nonexamples,
@@ -2179,7 +2021,6 @@ def __init__(
         proof: Proof,
         example_structure: "Optional[ExampleStructure]" = None,
         lean4_translation: "Optional[callable]" = None,
-        prolog_translation: "Optional[callable]" = None,
         z3_translation: "Optional[callable]" = None,
         computational_implementation: callable = None,
         can_add_examples: bool = True,
@@ -2191,7 +2032,6 @@ def __init__(
             computational_implementation=computational_implementation,
             example_structure=example_structure,
             lean4_translation=lean4_translation,
-            prolog_translation=prolog_translation,
             z3_translation=z3_translation,
             can_add_examples=can_add_examples,
             can_add_nonexamples=can_add_nonexamples,
diff --git a/frame/productions/base.py b/frame/productions/base.py
index c4040de..34dc850 100644
--- a/frame/productions/base.py
+++ b/frame/productions/base.py
@@ -6,7 +6,7 @@
 - Symbolic definitions
 - Computational implementations
 - Example sets
-- Target language translations (Lean4, Prolog, Z3)
+- Target language translations (Lean4, Z3)
 """
 
 from abc import ABC, abstractmethod
diff --git a/frame/productions/concepts/size.py b/frame/productions/concepts/size.py
index 821f290..9985a77 100644
--- a/frame/productions/concepts/size.py
+++ b/frame/productions/concepts/size.py
@@ -230,7 +230,6 @@ def size_compute(*args):
                     input_arity=input_arity,
                 ),
                 lean4_translation=lambda *args: "",
-                prolog_translation=lambda *args: "",
                 z3_translation=None,
                 can_add_examples=can_add_examples,
                 can_add_nonexamples=can_add_nonexamples,
@@ -262,7 +261,6 @@ def size_compute(*args):
                 input_arity=len(free_indices),
             ),
             lean4_translation=lambda *args: "",
-            prolog_translation=lambda *args: "",
             z3_translation=None,
             can_add_examples=can_add_examples,
             can_add_nonexamples=can_add_nonexamples,
diff --git a/frame/productions/conjectures/equivalence.py b/frame/productions/conjectures/equivalence.py
index 045a4b7..cc63272 100644
--- a/frame/productions/conjectures/equivalence.py
+++ b/frame/productions/conjectures/equivalence.py
@@ -386,7 +386,6 @@ def create_mersenne_form_concept():
             input_arity=1
         ),
         lean4_translation=lambda n: f"(∃ k : ℕ, is_prime(2^(k+1) - 1) ∧ {n} = 2^k * (2^(k+1) - 1))",
-        prolog_translation=lambda n: f"exists(k, nat, (is_prime(minus(power(2, plus(k, 1)), 1)), equals({n}, times(power(2, k), minus(power(2, plus(k, 1)), 1)))))",
         z3_translation=lambda n: f"(exists ((k Int)) (and (is_prime (- (^ 2 (+ k 1)) 1)) (= {n} (* (^ 2 k) (- (^ 2 (+ k 1)) 1)))))"
     )
     
diff --git a/tests/productions/conftest.py b/tests/productions/conftest.py
index 097769a..dc61c61 100644
--- a/tests/productions/conftest.py
+++ b/tests/productions/conftest.py
@@ -233,7 +233,6 @@ def greater_than():
             input_arity=2,
         ),
         lean4_translation=lambda a, b: f"({a} > {b})",
-        prolog_translation=lambda a, b: f"({a} > {b})",
         z3_translation=lambda a, b: Z3Template(
             f"""
             params 2;
@@ -397,7 +396,6 @@ def multiply():
             input_arity=2,
         ),
         lean4_translation=lambda a, b: f"({a} * {b})",
-        prolog_translation=lambda a, b: f"times({a}, {b}, Result)",
         z3_translation=lambda a, b: Z3Template(
             f"""
             params 2;
@@ -439,7 +437,6 @@ def multiply3():
             input_arity=3,
         ),
         lean4_translation=lambda a, b, c: f"({a} * {b} * {c})",
-        prolog_translation=lambda a, b, c: f"times3({a}, {b}, {c}, Result)",
         z3_translation=lambda a, b, c: f"(* {a} (* {b} {c}))",
     )