Fix and improve kernel2code and asFront methods

Author: augustepoiroux

lisa-examples/src/main/scala/Kernel2Code.scala

@@ -209,63 +209,48 @@ object Kernel2Code extends lisa.Main {
     }
     val s_2 = have(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) subproof {
       val s_2_0 = have(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) by InstFunSchema(Map(x -> f(x)))(s_1)
+      val s_2_1 = have(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) by InstFunSchema(Map(x -> f(x)))(s_1)
     }
     val s_3 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))) subproof {
       val s_3_0 = have(() ⊢ (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x))))) by Restate.from(s_1)
       val s_3_1 = have(() ⊢ (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) by Restate.from(s_2)
       val s_3_2 = have((∀(x, (Q(x) ==> Q(f(x)))), (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) subproof {
         val s_3_2_0 = have(
-          Q(f(x)) ⊢ ¬(((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊤) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(⊤)))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x))))))
+          Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊤ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊤))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
         ) by Restate
         val s_3_2_1 = thenHave(
-          Q(f(x)) ⊢ ¬(
-            ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
-          )
-        ) by RightSubstIff(
+          Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
+        ) by RightSubstIff.withParametersSimple(
           List(((Q(f(x))), (⊤))),
           lambda(
             Seq(MaRvIn_1),
-            ¬(
-              ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ MaRvIn_1) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(MaRvIn_1)))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(
-                Q(f(f(x)))
-              ))
-            )
+            ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ MaRvIn_1 ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(MaRvIn_1))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
           )
         )
         val s_3_2_2 = have(
-          ¬(Q(f(x))) ⊢ ¬(
-            ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊥) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(⊥)))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
-          )
+          ¬(Q(f(x))) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊥ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊥))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
         ) by Restate
         val s_3_2_3 = thenHave(
           ¬(Q(f(x))) ⊢ ¬(
-            ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
+            (¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x)))))
           )
-        ) by RightSubstIff(
+        ) by RightSubstIff.withParametersSimple(
           List(((Q(f(x))), (⊥))),
           lambda(
             Seq(MaRvIn_1),
-            ¬(
-              ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ MaRvIn_1) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(MaRvIn_1)))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(
-                Q(f(f(x)))
-              ))
-            )
+            ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ MaRvIn_1 ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(MaRvIn_1))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
           )
         )
         val s_3_2_4 = thenHave(
           () ⊢ (Q(f(x)), ¬(
-            ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
+            (¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x)))))
           ))
         ) by Restate
         val s_3_2_5 = have(
-          () ⊢ ¬(
-            ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
-          )
+          () ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
         ) by Cut(s_3_2_4, s_3_2_1)
         val s_3_2_6 = thenHave(
-          () ⊢ ¬(
-            ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
-          )
+          () ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
         ) by Restate
         val s_3_2_7 =
           thenHave((∀(x, (Q(x) ==> Q(f(x)))), (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Restate
@@ -282,25 +267,21 @@ object Kernel2Code extends lisa.Main {
     val s_3 = have(() ⊢ (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x))))) by Restate.from(s_1)
     val s_4 = have(() ⊢ (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) by Restate.from(s_2)
     val s_5 = have(
-      Q(f(x)) ⊢ ¬(((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊤) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(⊤)))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x))))))
+      Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊤ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊤))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
     ) by Restate
     val s_6 = thenHave(
-      Q(f(x)) ⊢ ¬(
-        ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
-      )
+      Q(f(x)) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
     ) by Restate
     val s_7 = have(
-      ¬(Q(f(x))) ⊢ ¬(((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊥) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(⊥)))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x))))))
+      ¬(Q(f(x))) ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ ⊥ ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(⊥))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
     ) by Restate
     val s_8 = thenHave(
       () ⊢ (Q(f(x)), ¬(
-        ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
+        (¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x)))))
       ))
     ) by Restate
     val s_9 = have(
-      () ⊢ ¬(
-        ((((¬(((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x))) ∧ ¬(Q(f(f(x)))))) ∧ ¬(((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x)) ∧ ¬(Q(f(x)))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x))))))) ∧ Q(x)) ∧ ¬(Q(f(f(x)))))
-      )
+      () ⊢ ¬((¬((∀(x_1, ¬((Q(x_1) ∧ ¬(Q(f(x_1)))))) ∧ Q(f(x)) ∧ ¬(Q(f(f(x)))))) ∧ ¬((∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(x))))) ∧ ∀(x, ¬((Q(x) ∧ ¬(Q(f(x)))))) ∧ Q(x) ∧ ¬(Q(f(f(x))))))
     ) by Cut(s_8, s_6)
     val s_10 = thenHave((∀(x, (Q(x) ==> Q(f(x)))), (∀(x, (Q(x) ==> Q(f(x)))) ==> (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Restate
     val s_11 = have((∀(x, (Q(x) ==> Q(f(x)))), (∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ==> (Q(f(x)) ==> Q(f(f(x)))))) ⊢ (Q(x) ==> Q(f(f(x))))) by Cut(s_3, s_10)

lisa-utils/src/main/scala/lisa/fol/Common.scala

@@ -708,7 +708,11 @@ trait Common {
     def rename(newid: Identifier): ConstantConnectorLabel[N] = throw new Error("Can't rename a constant connector label")
     def freshRename(taken: Iterable[Identifier]): ConstantConnectorLabel[N] = rename(K.freshId(taken, id))
     override def toString(): String = id
-    def mkString(args: Seq[Formula]): String = if (args.length == 2) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")"
+    def mkString(args: Seq[Formula]): String = if (args.length == 1) {
+      underlyingLabel match
+        case K.Neg => toString() + "(" + args(0).toString() + ")"
+        case _ => args(0).toString()
+    } else "(" + args.mkString(" " + toString() + " ") + ")"
     override def mkStringSeparated(args: Seq[Formula]): String = if (args.length == 2) "(" + mkString(args) + ")" else mkString(args)
 
   }

lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala

@@ -118,10 +118,7 @@ object FOLHelpers {
   def asFront(pf: K.AtomicFormula): Formula =
     asFrontLabel(pf.label).applySeq(pf.args.map(asFront))
   def asFront(cf: K.ConnectorFormula): Formula =
-    cf.label match
-      case K.And | K.Or if cf.args.size == 1 => asFront(cf.args(0))
-      case K.And | K.Or => cf.args.map(asFront).reduceLeft((a, b) => asFrontLabel(cf.label)(Seq(a, b))) // TODO: handle this more gracefully
-      case _ => asFrontLabel(cf.label).applyUnsafe(cf.args.map(asFront))
+    asFrontLabel(cf.label).applyUnsafe(cf.args.map(asFront))
   def asFront(bf: K.BinderFormula): BinderFormula =
     asFrontLabel(bf.label).apply(asFrontLabel(bf.bound), asFront(bf.inner))
 

lisa-utils/src/main/scala/lisa/fol/Sequents.scala

@@ -168,9 +168,9 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
     infix def ++?(s1: Sequent): Sequent = this addAllIfNotExists s1
 
     override def toString =
-      (if left.size == 0 then "" else if left.size == 1 then left.head.toString else "( " + left.mkString(", ") + " )") +
+      (if left.size == 0 then "" else if left.size == 1 then left.head.toString else "(" + left.mkString(", ") + ")") +
         " ⊢ " +
-        (if right.size == 0 then "" else if right.size == 1 then right.head.toString else "( " + right.mkString(", ") + " )")
+        (if right.size == 0 then "" else if right.size == 1 then right.head.toString else "(" + right.mkString(", ") + ")")
 
   }
 

lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala

@@ -9,7 +9,6 @@ import lisa.utils.KernelHelpers.lambda
 
 object ProofsConverter {
 
-// TODO: fix printing of ∧ and ∨ with > 2 arguments, currently handled as recursive binary operators (see FOLHelpers.scala)
 // TODO: remove unnecessary variables "val s_..." in generated proofs -> need to keep track of which steps are used in other steps
 // TODO: generate more realistic variable names
 // TODO: handle automatic global variable declaration before theorems/proofs
@@ -65,14 +64,14 @@ object ProofsConverter {
             case LeftSubstEq(bot, t1, equals, lambdaPhi) => (bot, Seq(t1))
             case RightSubstEq(bot, t1, equals, lambdaPhi) => (bot, Seq(t1))
             case LeftSubstIff(bot, t1, equals, lambdaPhi) =>
-              tacticName = s"LeftSubstIff(List(${equals
-                  .map((a, b) => s"((${formula2code(a)}), (${formula2code(b)}))")
-                  .mkString(", ")}), lambda(Seq(${lambdaPhi.vars.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi.body)}))"
+              tacticName = s"LeftSubstIff.withParametersSimple(List(${equals
+                  .map((a, b) => s"((${formula2code(a.body)}), (${formula2code(b.body)}))")
+                  .mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi._2)}))"
               (bot, Seq(t1))
             case RightSubstIff(bot, t1, equals, lambdaPhi) =>
-              tacticName = s"RightSubstIff(List(${equals
-                  .map((a, b) => s"((${formula2code(a)}), (${formula2code(b)}))")
-                  .mkString(", ")}), lambda(Seq(${lambdaPhi.vars.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi.body)}))"
+              tacticName = s"RightSubstIff.withParametersSimple(List(${equals
+                  .map((a, b) => s"((${formula2code(a.body)}), (${formula2code(b.body)}))")
+                  .mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi._2)}))"
               (bot, Seq(t1))
             case InstSchema(bot, t1, mCon, mPred, mTerm) =>
               if mCon.isEmpty && mPred.isEmpty then

lisa-utils/src/main/scala/lisa/utils/tptp/ProblemGatherer.scala

@@ -4,8 +4,7 @@ import lisa.utils.tptp.KernelParser.*
 
 object ProblemGatherer {
   // Path to the TPTP problems directory
-  // val path = getClass.getResource("/TPTP/Problems/").getPath
-  val TPTPProblemPath = "/home/auguste/Documents/EPFL/PhD/Projects/TPTP-v8.2.0/Problems/"
+  val TPTPProblemPath: String = getClass.getResource("/TPTP/Problems/").getPath
 
   /**
    * @return sequence of tptp problems in the library lib with the tags in spc.