Removed unnecessary to_prolog methods from the codebase

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.

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,

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})",
 )