From b667d900d591c0e5ef87dbe025054b8bc9709e25 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Mon, 4 Aug 2025 14:13:44 +0200 Subject: [PATCH] Remove lisa-sets2 --- .../main/scala/lisa/automation/atp/Egg.scala | 133 ------------------ .../Functions/Examples/ConstantFunction.scala | 9 -- .../src/test/resources/goeland_test_1.p | 19 --- .../test/resources/level2_steps/instMult.p | 31 ---- lisa-sets2/src/test/resources/p9_test_1.p | 36 ----- lisa-sets2/src/test/resources/p9_test_2.p | 55 -------- lisa-sets2/src/test/resources/p9_test_3.p | 116 --------------- .../src/test/resources/steps_tests/cut.p | 21 --- .../src/test/resources/steps_tests/hyp.p | 13 -- .../src/test/resources/steps_tests/instFun.p | 30 ---- .../src/test/resources/steps_tests/instPred.p | 30 ---- .../src/test/resources/steps_tests/leftAnd.p | 21 --- .../test/resources/steps_tests/leftEpsilon.p | 22 --- .../test/resources/steps_tests/leftExists.p | 22 --- .../test/resources/steps_tests/leftForall.p | 22 --- .../src/test/resources/steps_tests/leftIff.p | 21 --- .../test/resources/steps_tests/leftImplies.p | 21 --- .../src/test/resources/steps_tests/leftNot.p | 20 --- .../src/test/resources/steps_tests/leftOr.p | 21 --- .../test/resources/steps_tests/leftSubst.p | 15 -- .../test/resources/steps_tests/leftSubstIff.p | 15 -- .../test/resources/steps_tests/leftWeaken.p | 12 -- .../src/test/resources/steps_tests/rightAnd.p | 21 --- .../test/resources/steps_tests/rightEpsilon.p | 0 .../test/resources/steps_tests/rightExists.p | 23 --- .../test/resources/steps_tests/rightForall.p | 22 --- .../src/test/resources/steps_tests/rightIff.p | 21 --- .../test/resources/steps_tests/rightImplies.p | 21 --- .../src/test/resources/steps_tests/rightNot.p | 20 --- .../src/test/resources/steps_tests/rightOr.p | 21 --- .../test/resources/steps_tests/rightRefl.p | 3 - .../test/resources/steps_tests/rightSubst.p | 15 -- .../resources/steps_tests/rightSubstIff.p | 15 -- .../test/resources/steps_tests/rightWeaken.p | 12 -- 34 files changed, 899 deletions(-) delete mode 100644 lisa-sets2/src/main/scala/lisa/automation/atp/Egg.scala delete mode 100644 lisa-sets2/src/main/scala/lisa/maths/SetTheory/Functions/Examples/ConstantFunction.scala delete mode 100644 lisa-sets2/src/test/resources/goeland_test_1.p delete mode 100644 lisa-sets2/src/test/resources/level2_steps/instMult.p delete mode 100644 lisa-sets2/src/test/resources/p9_test_1.p delete mode 100644 lisa-sets2/src/test/resources/p9_test_2.p delete mode 100644 lisa-sets2/src/test/resources/p9_test_3.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/cut.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/hyp.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/instFun.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/instPred.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftAnd.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftEpsilon.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftExists.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftForall.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftIff.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftImplies.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftNot.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftOr.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftSubst.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftSubstIff.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/leftWeaken.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightAnd.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightEpsilon.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightExists.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightForall.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightIff.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightImplies.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightNot.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightOr.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightRefl.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightSubst.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightSubstIff.p delete mode 100644 lisa-sets2/src/test/resources/steps_tests/rightWeaken.p diff --git a/lisa-sets2/src/main/scala/lisa/automation/atp/Egg.scala b/lisa-sets2/src/main/scala/lisa/automation/atp/Egg.scala deleted file mode 100644 index 47138fc82..000000000 --- a/lisa-sets2/src/main/scala/lisa/automation/atp/Egg.scala +++ /dev/null @@ -1,133 +0,0 @@ -package lisa.automation.atp -import lisa.utils.fol.FOL as F -import lisa.utils.prooflib.Library -import lisa.utils.prooflib.OutputManager -import lisa.utils.prooflib.ProofTacticLib.* -import lisa.utils.K - -import java.io.* -import scala.io.Source -import scala.util.Failure -import scala.util.Success -import scala.util.Try - -import sys.process._ -import lisa.tptp.ProofParser.* -import lisa.tptp.ProofPrinter.* -import lisa.tptp.KernelParser.* - -/** - * Goéland is an automated theorem prover. This tactic calls the Goéland prover to solve the current sequent. - * Goéland is only available on Linux yet, but proofs generated by Goéland should be kept in the library for future use. - * To ensure that proofs are published and can be replayed in any system, proofs from an ATPcan only be generated in draft mode. - * When in non-draft mode, the proof file should be given as an argument to the tactic (the exact file is provided by Lisa upon run without draft mode). - */ -object Egg extends ProofTactic with ProofSequentTactic { - private var i : Int = 0 - - var timeLimit = 5 - - val eggExec_linux = "../bin/egg-sc-tptp" - val eggExec_windows = "..\\bin\\egg-sc-tptp.exe" - - class OsNotSupportedException(msg: String) extends Exception(msg) - - val foldername = "egg/" - - /** - * Fetch a proof of a sequent that was previously proven by Goéland. - * The file must be in SC-TPTP format. - */ - def apply(using lib: Library, proof: lib.Proof)(file:String)(bot: F.Sequent): proof.ProofTacticJudgement = { - val outputname = proof.owningTheorem.fullName+"_sol" - try { - val scproof = reconstructProof(new File(foldername+outputname+".p"))(using mapAtom, mapTerm, mapVariable) - proof.ValidProofTactic(bot, scproof.steps, Seq()) - } catch { - case e: FileNotFoundException => - throw FileNotFoundException("The file "+foldername+outputname+".p was not found. To produce a proof, use `by Egg`. ") - case e => throw e - } - } - - - /** - * Solve a sequent using the Goéland automated theorem prover. - * At the moment, this option is only available on Linux system. - * The proof is generated and saved in a file in the `Egg` folder. - */ - def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = { - from(using lib, proof)()(bot) - } - - def from(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(bot: F.Sequent) = { - val axioms = premises.map(proof.getSequent) - solve(axioms, bot, proof.owningTheorem.fullName, lib.isDraft) match { - case Success(value) => proof.ValidProofTactic(bot, value.steps, premises) - case Failure(e) => e match - case e: FileNotFoundException => throw new Exception("For compatibility reasons, external provers can't be called in non-draft mode" + - " unless all proofs have already been generated and be available in static files. You can enable draft mode by adding `draft()` at the top of your working file.") - case e: OsNotSupportedException => throw e - case e => - throw e - } - } - - inline def solve(axioms: Seq[F.Sequent], sequent: F.Sequent, source: String, generateProofs : Boolean): Try[K.SCProof] = - solveK(axioms.map(_.underlying), sequent.underlying, source, generateProofs) - - - /** - * Solve a sequent using the Goéland automated theorem prover, and return the kernel proof. - * At the moment, this option is only available on Linux systems. - */ - def solveK(using line: sourcecode.Line, file: sourcecode.File)(axioms: Seq[K.Sequent], sequent: K.Sequent, source:String, generateProofs : Boolean): Try[K.SCProof] = { - val filename = source - val outputname = source+"_sol" - val directory = File(foldername) - if (directory != null) && !directory.exists() then directory.mkdirs() - - val freevars = (sequent.left.flatMap(_.freeVariables) ++ sequent.right.flatMap(_.freeVariables) ).toSet.map(x => x -> K.Variable(K.Identifier("X"+x.id.name, x.id.no), x.sort) ).toMap - - val backMap = freevars.map{ - case (x: K.Variable, xx: K.Variable) => xx -> x - } - val r = problemToFile(foldername, filename, "question"+i, axioms, sequent, source) - i += 1 - if generateProofs then - val OS = System.getProperty("os.name") - if OS.contains("nix") || OS.contains("nux") || OS.contains("aix") then - val ret = s"chmod u+x \"$eggExec_linux\"".! - val cmd = (s"$eggExec_linux $foldername$filename.p $foldername$outputname.p --level1") // TODO - val res = try { - cmd.!! - } catch { - case e: Exception => - throw e - } - val proof = reconstructProof(new File(foldername+outputname+".p"))(using mapAtom, mapTerm, mapVariable) - Success(proof) - else if OS.contains("win") || OS.contains("Win") then - val cmd = (s"$eggExec_windows $foldername$filename.p $foldername$outputname.p --level1") // TODO - val res = try { - cmd.!! - } catch { - case e: Exception => - throw e - } - val proof = reconstructProof(new File(foldername+outputname+".p"))(using mapAtom, mapTerm, mapVariable) - Success(proof) - else - Failure(OsNotSupportedException("The Egg automated theorem prover is only supported on Linux for now.")) - else - if File(foldername+outputname+".p").exists() then - val proof = reconstructProof(new File(foldername+outputname+".p"))(using mapAtom, mapTerm, mapVariable) - println(OutputManager.WARNING(s"WARNING: in ${file.value}:$line, For compatibility reasons, replace `by Egg` with `by Egg(\"$foldername$outputname\")`.")) - Success(proof) - - else Failure(Exception("For compatibility reasons, external provers can't be called in non-draft mode. You can enable draft mode by adding `draft()` at the top of your working file.")) - - - } - -} \ No newline at end of file diff --git a/lisa-sets2/src/main/scala/lisa/maths/SetTheory/Functions/Examples/ConstantFunction.scala b/lisa-sets2/src/main/scala/lisa/maths/SetTheory/Functions/Examples/ConstantFunction.scala deleted file mode 100644 index 23da98a1c..000000000 --- a/lisa-sets2/src/main/scala/lisa/maths/SetTheory/Functions/Examples/ConstantFunction.scala +++ /dev/null @@ -1,9 +0,0 @@ -package lisa.maths.SetTheory.Functions.Examples - -/** - * A constant function `f : A -> B` is a function such that `f(x) = c` - * for all `x ∈ A`, for some constant term `c`. - * - * TODO: Define it. - */ -object ConstantFunction {} diff --git a/lisa-sets2/src/test/resources/goeland_test_1.p b/lisa-sets2/src/test/resources/goeland_test_1.p deleted file mode 100644 index df6eddef1..000000000 --- a/lisa-sets2/src/test/resources/goeland_test_1.p +++ /dev/null @@ -1,19 +0,0 @@ -fof(c_simple_p, conjecture, ((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))). - -fof(f7, plain, [~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))), (! [X5] : (p_2(X5))), ~((p_2(a_3) & p_2(b_4))), ~(p_2(a_3)), p_2(a_3)] --> [], inference(leftHyp, [status(thm), 3], [])). - -fof(f5, plain, [~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))), (! [X5] : (p_2(X5))), ~((p_2(a_3) & p_2(b_4))), ~(p_2(a_3))] --> [], inference(leftForall, [status(thm), 1, $fot(a_3)], [f7])). - -fof(f8, plain, [~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))), (! [X5] : (p_2(X5))), ~((p_2(a_3) & p_2(b_4))), ~(p_2(b_4)), p_2(b_4)] --> [], inference(leftHyp, [status(thm), 3], [])). - -fof(f6, plain, [~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))), (! [X5] : (p_2(X5))), ~((p_2(a_3) & p_2(b_4))), ~(p_2(b_4))] --> [], inference(leftForall, [status(thm), 1, $fot(b_4)], [f8])). - -fof(f4, plain, [~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))), (! [X5] : (p_2(X5))), ~((p_2(a_3) & p_2(b_4)))] --> [], inference(leftNotAnd, [status(thm), 2], [f5, f6])). - -fof(f3, plain, [~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4))))] --> [], inference(leftNotImplies, [status(thm), 0], [f4])). - -fof(f2, plain, [((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))] --> [((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))], inference(hyp, [status(thm), 0], [])). - -fof(f1, plain, [] --> [((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4))), ~(((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4))))], inference(rightNot, [status(thm), 1], [f2])). - -fof(f0, plain, [] --> [((! [X5] : (p_2(X5))) => (p_2(a_3) & p_2(b_4)))], inference(cut, [status(thm), 1], [f1, f3])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/level2_steps/instMult.p b/lisa-sets2/src/test/resources/level2_steps/instMult.p deleted file mode 100644 index c08a33d7e..000000000 --- a/lisa-sets2/src/test/resources/level2_steps/instMult.p +++ /dev/null @@ -1,31 +0,0 @@ -fof(a1, axiom, [q(X)] --> []). -fof(f1, plain, [q(b)] --> [], inference(instMult, [status(thm), [tuple3('X', $fot(b), [])]], [a1])). - -fof(a2, axiom, [q(g(X, f(X)))] --> []). -fof(f2, plain, [q(g(f(c), f(f(c))))] --> [], inference(instMult, [status(thm), [tuple3('X', $fot(f(c)), [])]], [a2])). - -fof(a3, axiom, [q(X), q(g(X, f(X)))] --> [q(g(f(X, Y)))]). -fof(f3, plain, [q(f(b)), q(g(f(b), f(f(b))))] --> [q(g(f(f(b), Y)))], inference(instMult, [status(thm), [tuple3('X', $fot(f(b)), [])]], [a3])). - - -fof(a4, axiom, [![X] : q(g(X, f(Y)))] --> [q(g(f(X, Y)))]). -fof(f4, plain, [![Z] : q(g(Z, f(f(X))))] --> [q(g(f(X, f(X))))], inference(instMult, [status(thm), [tuple3('Y', $fot(f(X)), [])]], [a4])). - -fof(a5, axiom, [![X] : q(g(X, f(Y)))] --> [q(g(f(X, Y)))]). -fof(f5, plain, [![Y] : q(g(Y, f(f(X))))] --> [q(g(f(X, f(X))))], inference(instMult, [status(thm), [tuple3('Y', $fot(f(X)), [])]], [a5])). - - -fof(a6, axiom, [~(A | ~A)] --> []). -fof(f6, plain, [~(~p(b) | ~(~p(b)) )] --> [], inference(instMult, [status(thm), [tuple3('A', $fof(~p(b)), [])]], [a6])). - -fof(a7, axiom, [A, (A & ~p(b))] --> [(~A) => B]). -fof(f7, plain, [~p(B), (~p(B) & ~p(b))] --> [(~~p(B)) => B], inference(instMult, [status(thm), [tuple3('A', $fof(~p(B)), [])]], [a7])). - -fof(a8, axiom, [![X] : P(b, X)] --> []). -fof(f8, plain, [![A] : p(A, Z)] --> [], inference(instMult, [status(thm), [tuple3('P', $fof(p(Y, Z)), ['X', 'Y'])]], [a8])). - - -fof(a9, axiom, [![X] : P(Y, X)] --> []). -fof(f9, plain, [![A] : p(A, f(X))] --> [], inference(instMult, [status(thm), [tuple3('P', $fof(p(Y, X)), ['X', 'Y']), tuple3('Y', $fot(f(X)), [])]], [a9])). - - diff --git a/lisa-sets2/src/test/resources/p9_test_1.p b/lisa-sets2/src/test/resources/p9_test_1.p deleted file mode 100644 index babe13ef3..000000000 --- a/lisa-sets2/src/test/resources/p9_test_1.p +++ /dev/null @@ -1,36 +0,0 @@ -fof(test_minimaliste, conjecture, [] --> [(! [X]: p(X) => (p(a) & p(b)))]). -fof(phi, let, ~(! [X]: p(X) => (p(a) & p(b)))). -fof(negated_conjecture, assumption, [~(! [X]: p(X) => (p(a) & p(b)))] --> [~(! [X]: p(X) => (p(a) & p(b)))], inference(hyp, [status(thm), 0], [])). -fof(nnf_step, plain, [$phi] --> [(! [X]: p(X) & (~p(a) | ~p(b)))], inference(rightNnf, [status(thm), 0, 0], [negated_conjecture])). -fof(prenex_step, plain, [$phi] --> [! [X]: (p(X) & (~p(a) | ~p(b)))], inference(rightPrenex, [status(thm), 0, 0], [nnf_step])). -fof(i0, plain, [$phi] --> [(p(V0) & (~p(a) | ~p(b)))], inference(instForall, [status(thm), 0, $fot(V0)], [prenex_step])). -fof(tsStep0, let, (Ts3 <=> (~p(a) | ~p(b)))). -fof(tsStep1, let, ! [V0]: (Ts1(V0) <=> (p(V0) & Ts3))). -fof(tsStepExpl1, plain, [$phi,$tsStep0] --> [(p(V0) & Ts3)], inference(rightSubstIff, [status(thm), 1, $fof((p(V0) & A)), 'A'], [i0])). -fof(tsStepExpl2, plain, [$phi,$tsStep0,(Ts1(V0) <=> (p(V0) & Ts3))] --> [Ts1(V0)], inference(rightSubstIff, [status(thm), 2, $fof(A), 'A'], [tsStepExpl1])). -fof(4, plain, [$phi,$tsStep0,$tsStep1] --> [Ts1(V0)], inference(leftForall, [status(thm), 2, $fot(V0)], [tsStepExpl2])). -fof(a3, plain, [$phi,$tsStep0,(Ts1(V0) <=> (p(V0) & Ts3))] --> [~Ts1(V0),p(V0)], inference(clausify, [status(thm), 2], [])). -fof(3, plain, [$phi,$tsStep0,$tsStep1] --> [~Ts1(V0),p(V0)], inference(leftForall, [status(thm), 2, $fot(V0)], [a3])). -fof(a6, plain, [$phi,$tsStep0,(Ts1(V0) <=> (p(V0) & Ts3))] --> [~Ts1(V0),Ts3], inference(clausify, [status(thm), 2], [])). -fof(6, plain, [$phi,$tsStep0,$tsStep1] --> [~Ts1(V0),Ts3], inference(leftForall, [status(thm), 2, $fot(V0)], [a6])). -fof(7, plain, [$phi,$tsStep0,$tsStep1] --> [~Ts3,~p(a),~p(b)], inference(clausify, [status(thm), 1], [])). -fof(15, plain, [$phi,$tsStep0,$tsStep1] --> [~Ts1(V100),p(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [3])). -fof(16, plain, [$phi,$tsStep0,$tsStep1] --> [Ts1(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [4])). -fof(17, plain, [$phi,$tsStep0,$tsStep1] --> [p(V100)], inference(res, [status(thm), 0], [16, 15])). -fof(10, plain, [$phi,$tsStep0,$tsStep1] --> [p(V0)], inference(instMult, [status(thm), [tuple3('V100', $fot(V0), [])]], [17])). -fof(18, plain, [$phi,$tsStep0,$tsStep1] --> [~Ts1(V100),Ts3], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [6])). -fof(19, plain, [$phi,$tsStep0,$tsStep1] --> [Ts1(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [4])). -fof(11, plain, [$phi,$tsStep0,$tsStep1] --> [Ts3], inference(res, [status(thm), 0], [19, 18])). -fof(a012, plain, [$phi,$tsStep0,$tsStep1] --> [~p(a),~p(b)], inference(res, [status(thm), 0], [11, 7])). -fof(20, plain, [$phi,$tsStep0,$tsStep1] --> [p(a)], inference(instMult, [status(thm), [tuple3('V0', $fot(a), [])]], [10])). -fof(a112, plain, [$phi,$tsStep0,$tsStep1] --> [~p(b)], inference(res, [status(thm), 0], [20, a012])). -fof(21, plain, [$phi,$tsStep0,$tsStep1] --> [p(b)], inference(instMult, [status(thm), [tuple3('V0', $fot(b), [])]], [10])). -fof(12, plain, [$phi,$tsStep0,$tsStep1] --> [], inference(res, [status(thm), 0], [21, a112])). -fof(psi, let, (! [X]: p(X) => (p(a) & p(b)))). -fof(addPsi0, assumption, [$psi] --> [$psi], inference(hyp, [status(thm), 0], [])). -fof(addPsi1, plain, [] --> [$psi,$phi], inference(rightNot, [status(thm), 0], [addPsi0])). -fof(addPsi2, plain, [$tsStep0,$tsStep1] --> [$psi], inference(cut, [status(thm), 1], [addPsi1, 12])). -fof(removeTseitin0, plain, [$tsStep0,! [V0]: ((p(V0) & Ts3) <=> (p(V0) & Ts3))] --> [$psi], inference(instPred, [status(thm), 'Ts1', $fof((p(V0) & Ts3)), ['V0']], [addPsi2])). -fof(removeTseitin1, plain, [$tsStep0] --> [$psi], inference(elimIffRefl, [status(thm), 1], [removeTseitin0])). -fof(removeTseitin2, plain, [((~p(a) | ~p(b)) <=> (~p(a) | ~p(b)))] --> [$psi], inference(instPred, [status(thm), 'Ts3', $fof((~p(a) | ~p(b))), []], [removeTseitin1])). -fof(removeTseitin3, plain, [] --> [$psi], inference(elimIffRefl, [status(thm), 0], [removeTseitin2])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/p9_test_2.p b/lisa-sets2/src/test/resources/p9_test_2.p deleted file mode 100644 index 3d6f69333..000000000 --- a/lisa-sets2/src/test/resources/p9_test_2.p +++ /dev/null @@ -1,55 +0,0 @@ -fof(c1, conjecture, [] --> [((! [X]: p(X) | ! [Y]: q(Y)) => (p(c) | q(c)))]). -fof(phi, let, ~((! [X]: p(X) | ! [Y]: q(Y)) => (p(c) | q(c)))). -fof(negated_conjecture, assumption, [~((! [X]: p(X) | ! [Y]: q(Y)) => (p(c) | q(c)))] --> [~((! [X]: p(X) | ! [Y]: q(Y)) => (p(c) | q(c)))], inference(hyp, [status(thm), 0], [])). -fof(nnf_step, plain, [$phi] --> [((! [X]: p(X) | ! [Y]: q(Y)) & (~p(c) & ~q(c)))], inference(rightNnf, [status(thm), 0, 0], [negated_conjecture])). -fof(prenex_step, plain, [$phi] --> [! [X]: ! [Y]: ((p(X) | q(Y)) & (~p(c) & ~q(c)))], inference(rightPrenex, [status(thm), 0, 0], [nnf_step])). -fof(i0, plain, [$phi] --> [! [Y]: ((p(V0) | q(Y)) & (~p(c) & ~q(c)))], inference(instForall, [status(thm), 0, $fot(V0)], [prenex_step])). -fof(i1, plain, [$phi] --> [((p(V0) | q(V1)) & (~p(c) & ~q(c)))], inference(instForall, [status(thm), 0, $fot(V1)], [i0])). -fof(tsStep0, let, (Ts5 <=> (~p(c) & ~q(c)))). -fof(tsStep1, let, ! [V1]: ! [V0]: (Ts2(V0,V1) <=> (p(V0) | q(V1)))). -fof(tsStep2, let, ! [V1]: ! [V0]: (Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))). -fof(tsStepExpl0, plain, [$phi,$tsStep0] --> [((p(V0) | q(V1)) & Ts5)], inference(rightSubstIff, [status(thm), 1, 1, $fof(((p(V0) | q(V1)) & A)), 'A'], [i1])). -fof(tsStepExpl1, plain, [$phi,$tsStep0,(Ts2(V0,V1) <=> (p(V0) | q(V1)))] --> [(Ts2(V0,V1) & Ts5)], inference(rightSubstIff, [status(thm), 2, 1, $fof((A & Ts5)), 'A'], [tsStepExpl0])). -fof(tsStepExpl2, plain, [$phi,$tsStep0,! [V0]: (Ts2(V0,V1) <=> (p(V0) | q(V1)))] --> [(Ts2(V0,V1) & Ts5)], inference(leftForall, [status(thm), 2, $fot(V0)], [tsStepExpl1])). -fof(tsStepExpl3, plain, [$phi,$tsStep0,$tsStep1] --> [(Ts2(V0,V1) & Ts5)], inference(leftForall, [status(thm), 2, $fot(V1)], [tsStepExpl2])). -fof(tsStepExpl4, plain, [$phi,$tsStep0,$tsStep1,(Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))] --> [Ts3(V0,V1)], inference(rightSubstIff, [status(thm), 3, 1, $fof(A), 'A'], [tsStepExpl3])). -fof(tsStepExpl5, plain, [$phi,$tsStep0,$tsStep1,! [V0]: (Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))] --> [Ts3(V0,V1)], inference(leftForall, [status(thm), 3, $fot(V0)], [tsStepExpl4])). -fof(3, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts3(V0,V1)], inference(leftForall, [status(thm), 3, $fot(V1)], [tsStepExpl5])). -fof(a2s2, plain, [$phi,$tsStep0,$tsStep1,(Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))] --> [~Ts3(V0,V1),Ts2(V0,V1)], inference(clausify, [status(thm), 3], [])). -fof(a2s1, plain, [$phi,$tsStep0,$tsStep1,! [V0]: (Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))] --> [~Ts3(V0,V1),Ts2(V0,V1)], inference(leftForall, [status(thm), 3, $fot(V0)], [a2s2])). -fof(2, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts3(V0,V1),Ts2(V0,V1)], inference(leftForall, [status(thm), 3, $fot(V1)], [a2s1])). -fof(a5s2, plain, [$phi,$tsStep0,$tsStep1,(Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))] --> [~Ts3(V0,V1),Ts5], inference(clausify, [status(thm), 3], [])). -fof(a5s1, plain, [$phi,$tsStep0,$tsStep1,! [V0]: (Ts3(V0,V1) <=> (Ts2(V0,V1) & Ts5))] --> [~Ts3(V0,V1),Ts5], inference(leftForall, [status(thm), 3, $fot(V0)], [a5s2])). -fof(5, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts3(V0,V1),Ts5], inference(leftForall, [status(thm), 3, $fot(V1)], [a5s1])). -fof(a7s2, plain, [$phi,$tsStep0,$tsStep1,(Ts2(V0,V1) <=> (p(V0) | q(V1)))] --> [~Ts2(V0,V1),p(V0),q(V1)], inference(clausify, [status(thm), 3], [])). -fof(a7s1, plain, [$phi,$tsStep0,$tsStep1,! [V0]: (Ts2(V0,V1) <=> (p(V0) | q(V1)))] --> [~Ts2(V0,V1),p(V0),q(V1)], inference(leftForall, [status(thm), 3, $fot(V0)], [a7s2])). -fof(7, plain, [$phi,$tsStep0,! [V1]: ! [V0]: (Ts2(V0,V1) <=> (p(V0) | q(V1))),$tsStep2] --> [~Ts2(V0,V1),p(V0),q(V1)], inference(leftForall, [status(thm), 2, $fot(V1)], [a7s1])). -fof(19, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts3(V100,V101),Ts2(V100,V101)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), []), tuple3('V1', $fot(V101), [])]], [2])). -fof(20, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts3(V100,V101)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), []), tuple3('V1', $fot(V101), [])]], [3])). -fof(21, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts2(V100,V101)], inference(res, [status(thm), 0], [20, 19])). -fof(9, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts2(V0,V1)], inference(instMult, [status(thm), [tuple3('V100', $fot(V0), []), tuple3('V101', $fot(V1), [])]], [21])). -fof(10, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts5,~p(c)], inference(clausify, [status(thm), 1], [])). -fof(22, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts2(V100,V101)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), []), tuple3('V1', $fot(V101), [])]], [9])). -fof(23, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts2(V100,V101),p(V100),q(V101)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), []), tuple3('V1', $fot(V101), [])]], [7])). -fof(24, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [p(V100),q(V101)], inference(res, [status(thm), 0], [22, 23])). -fof(12, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [p(V0),q(V1)], inference(instMult, [status(thm), [tuple3('V100', $fot(V0), []), tuple3('V101', $fot(V1), [])]], [24])). -fof(25, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [p(c),q(V1)], inference(instMult, [status(thm), [tuple3('V0', $fot(c), [])]], [12])). -fof(26, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [q(V1),~Ts5], inference(res, [status(thm), 0], [25, 10])). -fof(13, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [q(V0),~Ts5], inference(instMult, [status(thm), [tuple3('V1', $fot(V0), [])]], [26])). -fof(14, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts5,~q(c)], inference(clausify, [status(thm), 1], [])). -fof(27, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts3(V100,V101),Ts5], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), []), tuple3('V1', $fot(V101), [])]], [5])). -fof(28, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts3(V100,V101)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), []), tuple3('V1', $fot(V101), [])]], [3])). -fof(15, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [Ts5], inference(res, [status(thm), 0], [28, 27])). -fof(29, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [q(c),~Ts5], inference(instMult, [status(thm), [tuple3('V0', $fot(c), [])]], [13])). -fof(16, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [~Ts5,~Ts5], inference(res, [status(thm), 0], [29, 14])). -fof(17, plain, [$phi,$tsStep0,$tsStep1,$tsStep2] --> [], inference(res, [status(thm), 0], [15, 16])). -fof(psi, let, ((! [X]: p(X) | ! [Y]: q(Y)) => (p(c) | q(c)))). -fof(addPsi0, assumption, [$psi] --> [$psi], inference(hyp, [status(thm), 0], [])). -fof(addPsi1, plain, [] --> [$psi,$phi], inference(rightNot, [status(thm), 0], [addPsi0])). -fof(addPsi2, plain, [$tsStep0,$tsStep1,$tsStep2] --> [$psi], inference(cut, [status(thm), 1], [addPsi1, 17])). -fof(removeTseitin0, plain, [$tsStep0,$tsStep1,! [V1]: ! [V0]: ((Ts2(V0,V1) & Ts5) <=> (Ts2(V0,V1) & Ts5))] --> [$psi], inference(instPred, [status(thm), 'Ts3', $fof((Ts2(V0,V1) & Ts5)), ['V0','V1']], [addPsi2])). -fof(removeTseitin1, plain, [$tsStep0,$tsStep1] --> [$psi], inference(elimIffRefl, [status(thm), 2], [removeTseitin0])). -fof(removeTseitin2, plain, [$tsStep0,! [V1]: ! [V0]: ((p(V0) | q(V1)) <=> (p(V0) | q(V1)))] --> [$psi], inference(instPred, [status(thm), 'Ts2', $fof((p(V0) | q(V1))), ['V0','V1']], [removeTseitin1])). -fof(removeTseitin3, plain, [$tsStep0] --> [$psi], inference(elimIffRefl, [status(thm), 1], [removeTseitin2])). -fof(removeTseitin4, plain, [((~p(c) & ~q(c)) <=> (~p(c) & ~q(c)))] --> [$psi], inference(instPred, [status(thm), 'Ts5', $fof((~p(c) & ~q(c))), []], [removeTseitin3])). -fof(removeTseitin5, plain, [] --> [$psi], inference(elimIffRefl, [status(thm), 0], [removeTseitin4])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/p9_test_3.p b/lisa-sets2/src/test/resources/p9_test_3.p deleted file mode 100644 index d6289bc1a..000000000 --- a/lisa-sets2/src/test/resources/p9_test_3.p +++ /dev/null @@ -1,116 +0,0 @@ -fof(conj, conjecture, [] --> [? [X]: ! [Y]: (p(Y) | ~p(X))]). - - - -fof(neg_conjecture, assumption, [~? [X]: ! [Y]: (p(Y) | ~p(X))] --> [~? [X]: ! [Y]: (p(Y) | ~p(X))], inference(hyp, [status(thm), 0], [])). - - -fof(r1, let, ~? [X]: ! [Y]: (p(Y) | ~p(X))). - - -fof(neg_conjecture_nnf, plain, [$r1] --> [! [X]: ? [Y]: (~p(Y) & p(X))], inference(rightNnf, [status(thm), 0, 0], [neg_conjecture])). - - -fof(sko_iff5, plain, [$r1] --> [! [X]: (? [Y]: (~p(Y) & p(X)) <=> (~p(# [Y]: ((~p(Y) & p(X)))) & p(X)))], inference(existsIffEpsilon, [status(thm), 0], [])). - - -fof(eps_subst5, plain, [! [X]: (? [Y]: (~p(Y) & p(X)) <=> (~p(# [Y]: ((~p(Y) & p(X)))) & p(X))),$r1] --> [! [X]: (~p(# [Y]: ((~p(Y) & p(X)))) & p(X))], inference(rightSubstPred, [status(thm), 0, 0, 'HOLE', $fof(! [X]: HOLE(X))], [neg_conjecture_nnf])). - - -fof(sko_cut5, plain, [$r1] --> [! [X]: (~p(# [Y]: ((~p(Y) & p(X)))) & p(X))], inference(cut, [status(thm), 0], [sko_iff5, eps_subst5])). - - -fof(sko_subst5, plain, [! [X]: # [Y]: ((~p(Y) & p(X))) = Sk5(X),$r1] --> [! [X]: (~p(Sk5(X)) & p(X))], inference(rightSubstFun, [status(thm), 0, 0, 'THOLE', $fof(! [X]: (~p(THOLE(X)) & p(X)))], [sko_cut5])). - - -fof(r2, let, ! [X]: # [Y]: ((~p(Y) & p(X))) = Sk5(X)). - - -fof(neg_conjecture_pre, plain, [$r2,$r1] --> [! [V0]: (~p(Sk5(V0)) & p(V0))], inference(rightPrenex, [status(thm), 0, 0], [sko_subst5])). - - -fof(neg_conjecture_V0, plain, [$r2,$r1] --> [(~p(Sk5(V0)) & p(V0))], inference(instForall, [status(thm), 0, $fot(V0)], [neg_conjecture_pre])). - - -fof(ts_cla1, plain, [(Ts1(V0) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [~p(Sk5(V0)),~Ts1(V0)], inference(clausify, [status(thm), 0], [])). - - -fof(ts_claQ1_1, plain, [! [V0]: (Ts1(V0) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [~p(Sk5(V0)),~Ts1(V0)], inference(leftForall, [status(thm), 0, $fot(V0)], [ts_cla1])). - - -fof(ts_clb1, plain, [(Ts1(V0) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [p(V0),~Ts1(V0)], inference(clausify, [status(thm), 0], [])). - - -fof(ts_clbQ1_1, plain, [! [V0]: (Ts1(V0) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [p(V0),~Ts1(V0)], inference(leftForall, [status(thm), 0, $fot(V0)], [ts_clb1])). - - -fof(ts_ax_just1, plain, [(Ts1(V0) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [Ts1(V0)], inference(rightSubstIff, [status(thm), 0, 0, $fof(HOLE), 'HOLE'], [neg_conjecture_V0])). - - -fof(ts_axQ1_1, plain, [! [V0]: (Ts1(V0) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [Ts1(V0)], inference(leftForall, [status(thm), 0, $fot(V0)], [ts_ax_just1])). - - -fof(r3, let, ! [V0]: (Ts1(V0) <=> (~p(Sk5(V0)) & p(V0)))). - - -fof(ts_claQ1_1_p9r, plain, [$r3,$r2,$r1] --> [~p(Sk5(V0)),~Ts1(V0)], inference(instMult, [status(thm), [tuple3('V0', $fot(V0), [])]], [ts_claQ1_1])). - - -fof(ts_clbQ1_1_p9r, plain, [$r3,$r2,$r1] --> [p(V0),~Ts1(V0)], inference(instMult, [status(thm), [tuple3('V0', $fot(V0), [])]], [ts_clbQ1_1])). - - -fof(ts_axQ1_1_p9r, plain, [$r3,$r2,$r1] --> [Ts1(V0)], inference(instMult, [status(thm), [tuple3('V0', $fot(V0), [])]], [ts_axQ1_1])). - - -fof(8, plain, [$r3,$r2,$r1] --> [p(Sk5(V100)),~Ts1(Sk5(V100))], inference(instMult, [status(thm), [tuple3('V0', $fot(Sk5(V100)), [])]], [ts_clbQ1_1_p9r])). - - -fof(9, plain, [$r3,$r2,$r1] --> [~p(Sk5(V100)),~Ts1(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [ts_claQ1_1_p9r])). - - -fof(10, plain, [$r3,$r2,$r1] --> [~Ts1(Sk5(V100)),~Ts1(V100)], inference(res, [status(thm), 0], [8, 9])). - - -fof(5, plain, [$r3,$r2,$r1] --> [~Ts1(Sk5(V0)),~Ts1(V0)], inference(instMult, [status(thm), [tuple3('V100', $fot(V0), [])]], [10])). - - -fof(11, plain, [$r3,$r2,$r1] --> [Ts1(Sk5(V100))], inference(instMult, [status(thm), [tuple3('V0', $fot(Sk5(V100)), [])]], [ts_axQ1_1_p9r])). - - -fof(12, plain, [$r3,$r2,$r1] --> [~Ts1(Sk5(V100)),~Ts1(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [5])). - - -fof(13, plain, [$r3,$r2,$r1] --> [~Ts1(V100)], inference(res, [status(thm), 0], [11, 12])). - - -fof(a06, plain, [$r3,$r2,$r1] --> [~Ts1(V0)], inference(instMult, [status(thm), [tuple3('V100', $fot(V0), [])]], [13])). - - -fof(14, plain, [$r3,$r2,$r1] --> [Ts1(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [ts_axQ1_1_p9r])). - - -fof(15, plain, [$r3,$r2,$r1] --> [~Ts1(V100)], inference(instMult, [status(thm), [tuple3('V0', $fot(V100), [])]], [a06])). - - -fof(ts_sp1, plain, [$r3,$r2,$r1] --> [], inference(res, [status(thm), 0], [14, 15])). - - -fof(ts_inst1, plain, [! [V0]: ((~p(Sk5(V0)) & p(V0)) <=> (~p(Sk5(V0)) & p(V0))),$r2,$r1] --> [], inference(instPred, [status(thm), 'Ts1', $fof((~p(Sk5(V0)) & p(V0))), ['V0']], [ts_sp1])). - - -fof(sko_sp9, plain, [$r2,$r1] --> [], inference(elimIffRefl, [status(thm), 0], [ts_inst1])). - - -fof(sko_inst9, plain, [! [X]: # [Y]: ((~p(Y) & p(X))) = # [Y]: ((~p(Y) & p(X))),$r1] --> [], inference(instFun, [status(thm), 'Sk5', $fot(# [Y]: ((~p(Y) & p(X)))), ['X']], [sko_sp9])). - - -fof(sp_neg_conj, plain, [$r1] --> [], inference(elimEqRefl, [status(thm), 0], [sko_inst9])). - - -fof(nc_elim_1, assumption, [? [X]: ! [Y]: (p(Y) | ~p(X))] --> [? [X]: ! [Y]: (p(Y) | ~p(X))], inference(hyp, [status(thm), 0], [])). - - -fof(nc_elim_2, plain, [] --> [~? [X]: ! [Y]: (p(Y) | ~p(X)),? [X]: ! [Y]: (p(Y) | ~p(X))], inference(rightNot, [status(thm), 1], [nc_elim_1])). - - -fof(nc_elim_3, plain, [] --> [? [X]: ! [Y]: (p(Y) | ~p(X))], inference(cut, [status(thm), 0], [nc_elim_2, sp_neg_conj])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/steps_tests/cut.p b/lisa-sets2/src/test/resources/steps_tests/cut.p deleted file mode 100644 index efc73f636..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/cut.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1_1, axiom, [p] --> [q]). -fof(a1_2, axiom, [q] --> [r]). -fof(f1, plain, [p] --> [r], inference(cut, [status(thm), 0, 0], [a1_1, a1_2])). - -fof(a2_1, axiom, [p, q] --> [r, s]). -fof(a2_2, axiom, [s, t] --> [u, v]). -fof(f2, plain, [p, q, t] --> [r, u, v], inference(cut, [status(thm), 1, 0], [a2_1, a2_2])). - -fof(a3_1, axiom, [p(X) & Q(X, Y), r(Y)] --> [s(X, c)]). -fof(a3_2, axiom, [s(X, c)] --> [r(t)]). -fof(f3, plain, [p(X) & Q(X, Y), r(Y)] --> [r(t)], inference(cut, [status(thm), 0, 0], [a3_1, a3_2])). - - -fof(a4_1, axiom, [![X, Y] : (p(X) & Q(X, Y)), r(Y)] --> [![X] : s(X, c)]). -fof(a4_2, axiom, [![X] : s(X, c)] --> [![Y] : r(f(t))]). -fof(f4, plain, [![X, Y] : (p(X) & Q(X, Y)), r(Y)] --> [![Y] : r(f(t))], inference(cut, [status(thm), 0, 0], [a4_1, a4_2])). - - -%fof(a4_1, axiom, [![X, Y] : (p(X) & Q(#[X] : p(X), Y)), r(Y)] --> [![X] : s(X, c)]). -%fof(a4_2, axiom, [![X] : s(X, c)] --> [![Y] : r(f(t))]). -%fof(f4, plain, [![X, Y] : (p(X) & Q(#[X] : p(X), Y)), r(Y)] --> [![Y] : r(f(t))], inference(cut, [status(thm), 0, 0], [a4_1, a4_2])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/steps_tests/hyp.p b/lisa-sets2/src/test/resources/steps_tests/hyp.p deleted file mode 100644 index c16c1dbd8..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/hyp.p +++ /dev/null @@ -1,13 +0,0 @@ -fof(f1, plain, [p] --> [p], inference(hyp, [status(thm), 0], [])). -fof(f3, plain, [p, q] --> [p], inference(hyp, [status(thm), 0], [])). -fof(f4, plain, [q] --> [p, q], inference(hyp, [status(thm), 0], [])). -fof(f5, plain, [p, q] --> [r, q], inference(hyp, [status(thm), 1], [])). -fof(f6, plain, [p & q] --> [p & q], inference(hyp, [status(thm), 0], [])). -fof(f7, plain, [p | q] --> [p | q], inference(hyp, [status(thm), 0], [])). -fof(f8, plain, [p => q] --> [p => q], inference(hyp, [status(thm), 0], [])). -fof(f9, plain, [p(X, c) => q(X)] --> [p(X, c) => q(X)], inference(hyp, [status(thm), 0], [])). -fof(f10, plain, [![X] :( p(X, c) => q(X))] --> [![X] : (p(X, c) => q(X))], inference(hyp, [status(thm), 0], [])). -fof(f11, plain, [![X] : (p(X, c) => q(X))] --> [![Y] : (p(Y, c) => q(Y))], inference(hyp, [status(thm), 0], [])). -fof(f12, plain, [?[Y] : ![X] : (p(X, c) => q(X))] --> [?[X] : ![Y] : (p(Y, c) => q(Y))], inference(hyp, [status(thm), 0], [])). -fof(f13, plain, [?[Y] : ![X] : (p(X, c) => q(Y))] --> [?[X] : ![Y] : (p(Y, c) => q(X))], inference(hyp, [status(thm), 0], [])). - diff --git a/lisa-sets2/src/test/resources/steps_tests/instFun.p b/lisa-sets2/src/test/resources/steps_tests/instFun.p deleted file mode 100644 index 648758a14..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/instFun.p +++ /dev/null @@ -1,30 +0,0 @@ -fof(a1, axiom, [q(X)] --> []). -fof(f1, plain, [q(b)] --> [], inference(instFun, [status(thm), 'X', $fot(b), []], [a1])). - -fof(a2, axiom, [q(g(X, f(X)))] --> []). -fof(f2, plain, [q(g(f(c), f(f(c))))] --> [], inference(instFun, [status(thm), 'X', $fot(f(c)), []], [a2])). - -fof(a3, axiom, [q(X), q(g(X, f(X)))] --> [q(g(f(X, Y)))]). -fof(f3, plain, [q(f(b)), q(g(f(b), f(f(b))))] --> [q(g(f(f(b), Y)))], inference(instFun, [status(thm), 'X', $fot(f(b)), []], [a3])). - - -fof(a4, axiom, [![X] : q(g(X, f(Y)))] --> [q(g(f(X, Y)))]). -fof(f4, plain, [![Z] : q(g(Z, f(f(X))))] --> [q(g(f(X, f(X))))], inference(instFun, [status(thm), 'Y', $fot(f(X)), []], [a4])). - -fof(a5, axiom, [![X] : q(g(X, f(Y)))] --> [q(g(f(X, Y)))]). -fof(f5, plain, [![Y] : q(g(Y, f(f(X))))] --> [q(g(f(X, f(X))))], inference(instFun, [status(thm), 'Y', $fot(f(X)), []], [a5])). - -fof(a6, axiom, [q(F(c))] --> []). -fof(f6, plain, [q(g(c, c))] --> [], inference(instFun, [status(thm), 'F', $fot(g(X, X)), ['X']], [a6])). - -fof(a7, axiom, [q(G(X, f(c)))] --> []). -fof(f7, plain, [q(g(F(f(c)), F(F(X))))] --> [], inference(instFun, [status(thm), 'G', $fot(g(F(Y), F(F(X)))), ['X', 'Y']], [a7])). - -fof(a8, axiom, [![X] : q(G(X, f(c)))] --> []). -fof(f8, plain, [![X] : q(g(F(f(c)), F(F(X))))] --> [], inference(instFun, [status(thm), 'G', $fot(g(F(Y), F(F(X)))), ['X', 'Y']], [a8])). - - -fof(a9, axiom, [![X] : q(G(X, f(c)))] --> [?[Y] : q(G(b, f(Y)))]). -fof(f9, plain, [![X] : q(g(F(f(c)), F(F(X))))] --> [?[Y] : q(g(F(f(Y)), F(F(b))))], inference(instFun, [status(thm), 'G', $fot(g(F(Y), F(F(X)))), ['X', 'Y']], [a9])). - - diff --git a/lisa-sets2/src/test/resources/steps_tests/instPred.p b/lisa-sets2/src/test/resources/steps_tests/instPred.p deleted file mode 100644 index 3078860df..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/instPred.p +++ /dev/null @@ -1,30 +0,0 @@ -fof(a1, axiom, [A] --> []). -fof(f1, plain, [p(b, c) ] --> [], inference(instPred, [status(thm), 'A', $fof(p(b, c)), []], [a1])). - -fof(a2, axiom, [~(A | ~A)] --> []). -fof(f2, plain, [~(~p(b) | ~(~p(b)) )] --> [], inference(instPred, [status(thm), 'A', $fof(~p(b)), []], [a2])). - -fof(a3, axiom, [A, (A & ~p(b))] --> [(~A) => B]). -fof(f3, plain, [~p(B), (~p(B) & ~p(b))] --> [(~~p(B)) => B], inference(instPred, [status(thm), 'A', $fof(~p(B)), []], [a3])). - -fof(a4, axiom, [![X] : P(b, X)] --> []). -fof(f4, plain, [![A] : p(A, Z)] --> [], inference(instPred, [status(thm), 'P', $fof(p(Y, Z)), ['X', 'Y']], [a4])). - -fof(a5, axiom, [![X] : P(X, f(Y))] --> []). -fof(f5, plain, [![X] : P(f(Y), f(f(X)))] --> [], inference(instPred, [status(thm), 'P', $fof(P(Y, f(f(X)))), ['X', 'Y']], [a5])). - -fof(a6, axiom, [P(a, b) & ~P(c, d)] --> []). -fof(f6, plain, [P(X, f(a)) & ~P(X, f(c))] --> [], inference(instPred, [status(thm), 'P', $fof(P(X, f(Y))), ['Y', 'Z']], [a6])). - -fof(a7, axiom, [![X] : P(X, c)] --> []). -fof(f7, plain, [![X] :( q(X) | ![Y] : p(Y, c))] --> [], - inference(instPred, [status(thm), 'P', $fof(q(X) | ![X] : p(X, Y)), ['X', 'Y']], [a7])). - -fof(a8, axiom, [![X] : P(X, f(c))] --> [?[Y] : P(b, f(Y))]). -fof(f8, plain, [![X] : (q(X) | ![Y] : ~q(Y, f(f(c))))] --> [?[Z] : (q(b) | ![X] : ~(q(X, f(f(Z)))))], - inference(instPred, [status(thm), 'P', $fof(q(X) | ![X] : ~(q(X, f(Y)))), ['X', 'Y']], [a8])). - - -%fof(a8, axiom, [![X] : P(X, #[Y] : (Q(X) & P(X, Y)))] --> []). -%fof(f8, plain, [![X] :( q(X) | ![Z] : p(Z, #[Y] : (Q(X) & P(X, Y))))] --> [], -% inference(instPred, [status(thm), 'P', $fof(q(X) | ![X] : p(X, Y)), ['X', 'Y']], [a8])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/steps_tests/leftAnd.p b/lisa-sets2/src/test/resources/steps_tests/leftAnd.p deleted file mode 100644 index 7134aa2c2..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftAnd.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1, axiom, [p, q] --> [r]). -fof(f1, plain, [p & q] --> [r], inference(leftAnd, [status(thm), 0], [a1])). - -fof(a2, axiom, [a, p, q] --> [r]). -fof(f2, plain, [a, p & q] --> [r], inference(leftAnd, [status(thm), 1], [a2])). - -fof(a3, axiom, [P(X), Q(X)] --> [R]). -fof(f3, plain, [P(X) & Q(X)] --> [R], inference(leftAnd, [status(thm), 0], [a3])). - -fof(a4, axiom, [s, p, t, q] --> [u]). -fof(f4, plain, [s, p & q, t] --> [u], inference(leftAnd, [status(thm), 1], [a4])). - -fof(a5, axiom, [p(X), q(Y)] --> [r(X, Y)]). -fof(f5, plain, [p(X) & q(Y)] --> [r(X, Y)], inference(leftAnd, [status(thm), 0], [a5])). - - -fof(a6, axiom, [![X]: (p(X) & q(X)), (r(X) | s(X))] --> [(t(X) & u(X)), v(X)]). -fof(f6, plain, [![X]: (p(X) & q(X)) & (r(X) | s(X)), (r(X) | s(X))] --> [(t(X) & u(X)), v(X)], inference(leftAnd, [status(thm), 0], [a6])). - -fof(a7, axiom, [q, ![X]: (p(X) & q(X)), s(Y)] --> []). -fof(f7, plain, [![X]: (p(X) & q(X)), q & s(Y)] --> [], inference(leftAnd, [status(thm), 1], [a7])). diff --git a/lisa-sets2/src/test/resources/steps_tests/leftEpsilon.p b/lisa-sets2/src/test/resources/steps_tests/leftEpsilon.p deleted file mode 100644 index 19b85a068..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftEpsilon.p +++ /dev/null @@ -1,22 +0,0 @@ -fof(a1, axiom, [p, q] --> [r]). -fof(f1, plain, [p, q] --> [r], inference(leftExists, [status(thm), 0, 'X'], [a1])). - -fof(a2, axiom, [a, p(X)] --> [r]). -fof(f2, plain, [a, p(#[X] : Q(X))] --> [r], inference(leftExists, [status(thm), 1, 'X'], [a2])). - -fof(a3, axiom, [P(Z), Q(Y)] --> [R]). -fof(f3, plain, [P(Z), Q(#[X] : Q(X))] --> [R], inference(leftExists, [status(thm), 1, 'Y'], [a3])). - - -fof(a4, axiom, [p(X), q(Z) | q(Y)] --> [r(X, Y)]). -fof(f4, plain, [p(X), (q(#[X] : (q(X) | q(Y))) | q(Y))] --> [r(X, Y)], inference(leftExists, [status(thm), 1, 'Z'], [a4])). - - -fof(a6, axiom, [?[X]: (p(X) & q(Z)), (r(X) | s(Y))] --> [(t(X) & u(X)), v(X)]). -fof(f6, plain, [?[X]: (p(# [Y] : ? [X]: (p(X) & q(Y))) & q(Y)), (r(X) | s(Y))] --> [(t(X) & u(X)), v(X)], inference(leftExists, [status(thm), 0, 'Z'], [a6])). - -fof(a7, axiom, [q, ?[X]: (p(X) & q(Z)), s(Y)] --> []). -fof(f7, plain, [q, ?[X, Y]: (p(Y) & q(X)), s(Y)] --> [], inference(leftExists, [status(thm), 1, 'Z'], [a7])). - -fof(a8, axiom, [q, ?[X]: (p(X) & r(Z, Z)), s(Y)] --> []). -fof(f8, plain, [q, ?[X, Y]: (p(Y) & r(X, X)), s(Y)] --> [], inference(leftExists, [status(thm), 1, 'Z'], [a8])). diff --git a/lisa-sets2/src/test/resources/steps_tests/leftExists.p b/lisa-sets2/src/test/resources/steps_tests/leftExists.p deleted file mode 100644 index 87958f555..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftExists.p +++ /dev/null @@ -1,22 +0,0 @@ -fof(a1, axiom, [p, q] --> [r]). -fof(f1, plain, [?[X] : p, q] --> [r], inference(leftExists, [status(thm), 0, 'X'], [a1])). - -fof(a2, axiom, [a, p(X)] --> [r]). -fof(f2, plain, [a, ?[X] : p(X)] --> [r], inference(leftExists, [status(thm), 1, 'X'], [a2])). - -fof(a3, axiom, [P(Z), Q(Y)] --> [R]). -fof(f3, plain, [P(Z), ?[X] : Q(X)] --> [R], inference(leftExists, [status(thm), 1, 'Y'], [a3])). - - -fof(a4, axiom, [p(X), q(Z) | q(Y)] --> [r(X, Y)]). -fof(f4, plain, [p(X), ?[X] : (q(X) | q(Y))] --> [r(X, Y)], inference(leftExists, [status(thm), 1, 'Z'], [a4])). - - -fof(a6, axiom, [?[X]: (p(X) & q(Z)), (r(X) | s(Y))] --> [(t(X) & u(X)), v(X)]). -fof(f6, plain, [?[Y, X]: (p(X) & q(Y)), (r(X) | s(Y))] --> [(t(X) & u(X)), v(X)], inference(leftExists, [status(thm), 0, 'Z'], [a6])). - -fof(a7, axiom, [q, ?[X]: (p(X) & q(Z)), s(Y)] --> []). -fof(f7, plain, [q, ?[X, Y]: (p(Y) & q(X)), s(Y)] --> [], inference(leftExists, [status(thm), 1, 'Z'], [a7])). - -fof(a8, axiom, [q, ?[X]: (p(X) & r(Z, Z)), s(Y)] --> []). -fof(f8, plain, [q, ?[X, Y]: (p(Y) & r(X, X)), s(Y)] --> [], inference(leftExists, [status(thm), 1, 'Z'], [a8])). diff --git a/lisa-sets2/src/test/resources/steps_tests/leftForall.p b/lisa-sets2/src/test/resources/steps_tests/leftForall.p deleted file mode 100644 index 60c1eec1c..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftForall.p +++ /dev/null @@ -1,22 +0,0 @@ -fof(a1, axiom, [p, q] --> [r]). -fof(f1, plain, [![X] : p, q] --> [r], inference(leftForall, [status(thm), 0, $fot(X)], [a1])). - -fof(a2, axiom, [a, p(X)] --> [r]). -fof(f2, plain, [a, ![X] : p(X)] --> [r], inference(leftForall, [status(thm), 1, $fot(X)], [a2])). - -fof(a3, axiom, [P(X), Q(f(c))] --> [R]). -fof(f3, plain, [P(X), ![X] : Q(X)] --> [R], inference(leftForall, [status(thm), 1, $fot(f(c))], [a3])). - - -fof(a4, axiom, [p(X), q(g(Y, c)) | q(Y)] --> [r(X, Y)]). -fof(f4, plain, [p(X), ![X] : (q(X) | q(Y))] --> [r(X, Y)], inference(leftForall, [status(thm), 1, $fot(g(Y, c))], [a4])). - - -fof(a6, axiom, [![X]: (p(X) & q(f(c))), (r(X) | s(Y))] --> [(t(X) & u(X)), v(X)]). -fof(f6, plain, [![Y, X]: (p(X) & q(Y)), (r(X) | s(Y))] --> [(t(X) & u(X)), v(X)], inference(leftForall, [status(thm), 0, $fot(f(c))], [a6])). - -fof(a7, axiom, [q, ![X]: (p(X) & q(f(c))), s(Y)] --> []). -fof(f7, plain, [q, ![X, Y]: (p(Y) & q(X)), s(Y)] --> [], inference(leftForall, [status(thm), 1, $fot(f(c))], [a7])). - -fof(a7, axiom, [q, ![X]: (p(X) & r(f(c), f(c))), s(Y)] --> []). -fof(f7, plain, [q, ![X, Y]: (p(Y) & r(X, X)), s(Y)] --> [], inference(leftForall, [status(thm), 1, $fot(f(c))], [a7])). diff --git a/lisa-sets2/src/test/resources/steps_tests/leftIff.p b/lisa-sets2/src/test/resources/steps_tests/leftIff.p deleted file mode 100644 index 957d5f396..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftIff.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1, axiom, [p=>q, q=>p] --> [r]). -fof(f1, plain, [p<=>q] --> [r], inference(leftIff, [status(thm), 0], [a1])). - -fof(a2, axiom, [a, p=>q, q=>p] --> [r]). -fof(f2, plain, [a, p <=> q] --> [r], inference(leftIff, [status(thm), 1], [a2])). - -fof(a3, axiom, [P(X)=>Q(X), Q(X)=>P(X)] --> [R]). -fof(f3, plain, [P(X) <=> Q(X)] --> [R], inference(leftIff, [status(thm), 0], [a3])). - -fof(a4, axiom, [s, p=>q, t, q=>p] --> [u]). -fof(f4, plain, [s, p <=> q, t] --> [u], inference(leftIff, [status(thm), 1], [a4])). - -fof(a5, axiom, [p(X)=>q(Y), q(Y)=>p(X)] --> [r(X, Y)]). -fof(f5, plain, [p(X) <=> q(Y)] --> [r(X, Y)], inference(leftIff, [status(thm), 0], [a5])). - - -fof(a6, axiom, [![X]: (p(X)) => (r(X) | s(X)), (r(X) | s(X)) => ![X]: (p(X))] --> [(t(X) & u(X)), v(X)]). -fof(f6, plain, [![X]: (p(X)) <=> (r(X) | s(X)), (r(X) | s(X)) => ![X]: (p(X))] --> [(t(X) & u(X)), v(X)], inference(leftIff, [status(thm), 0], [a6])). - -fof(a7, axiom, [q=>s(Y), ![X]: (p(X) & q(X)), s(Y)=>q] --> []). -fof(f7, plain, [![X]: (p(X) & q(X)), q <=> s(Y)] --> [], inference(leftIff, [status(thm), 1], [a7])). diff --git a/lisa-sets2/src/test/resources/steps_tests/leftImplies.p b/lisa-sets2/src/test/resources/steps_tests/leftImplies.p deleted file mode 100644 index 5ad6306f1..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftImplies.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1_1, axiom, [] --> [p, q]). -fof(a1_2, axiom, [q] --> [r]). -fof(f1, plain, [p => q] --> [r, q], inference(leftImplies, [status(thm), 0], [a1_1, a1_2])). - -fof(a2_1, axiom, [p] --> [q]). -fof(a2_2, axiom, [s, t] --> []). -fof(f2, plain, [p, q => s, t] --> [], inference(leftImplies, [status(thm), 1], [a2_1, a2_2])). - -fof(a3_1, axiom, [q] --> [p]). -fof(a3_2, axiom, [s, t] --> []). -fof(f3, plain, [p => t , q, s] --> [], inference(leftImplies, [status(thm), 0], [a3_1, a3_2])). - -fof(a4_1, axiom, [P(X)] --> [R & r(f(g(X, Y))), Q(X)]). -fof(a4_2, axiom, [R & Q(X)] --> [R]). -fof(f4, plain, [P(X), Q(X) => (R & Q(X))] --> [R & r(f(g(X, Y))), R], inference(leftImplies, [status(thm), 1], [a4_1, a4_2])). - -fof(a5_1, axiom, [A] --> [(t(X) & u(Z)), v(f(c)), ![X]: (p(X) & q(X))]). -fof(a5_2, axiom, [(r(X) | s(X))] --> [(t(X) & u(Z))]). -fof(f5, plain, [A, ![X]: (p(X) & q(X)) => (r(X) | s(X))] --> [(t(X) & u(Z)), v(f(c))], inference(leftImplies, [status(thm), 1], [a5_1, a5_2])). - - diff --git a/lisa-sets2/src/test/resources/steps_tests/leftNot.p b/lisa-sets2/src/test/resources/steps_tests/leftNot.p deleted file mode 100644 index ec3f1536d..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftNot.p +++ /dev/null @@ -1,20 +0,0 @@ -fof(a1, axiom, [] --> [p]). -fof(f1, plain, [~p] --> [], inference(leftNot, [status(thm), 0], [a1])). - -fof(a2, axiom, [q] --> [r]). -fof(f2, plain, [~r, q] --> [], inference(leftNot, [status(thm), 0], [a2])). - -fof(a3, axiom, [p, q] --> [r]). -fof(f3, plain, [~r, p, q] --> [], inference(leftNot, [status(thm), 0], [a3])). - -fof(a4, axiom, [p(X)] --> [q(X)]). -fof(f4, plain, [~q(X), p(X)] --> [], inference(leftNot, [status(thm), 0], [a4])). - -fof(a5, axiom, [p(X, Y)] --> [![Y] : q(Y)]). -fof(f5, plain, [~![Y] : q(Y), p(X, Y)] --> [], inference(leftNot, [status(thm), 0], [a5])). - -fof(a6, axiom, [p(X) & q(Y)] --> [r(Z), ![X] : p(X) & q(Y)]). -fof(f6, plain, [p(X) & q(Y), ~r(Z)] --> [![X] : p(X) & q(Y)], inference(leftNot, [status(thm), 1], [a6])). - -fof(a7, axiom, [] --> [r(c), ![X] : p(X)]). -fof(f7, plain, [~![Y] : p(Y)] --> [r(c)], inference(leftNot, [status(thm), 0], [a7])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/steps_tests/leftOr.p b/lisa-sets2/src/test/resources/steps_tests/leftOr.p deleted file mode 100644 index b2b47e45b..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftOr.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1_1, axiom, [p] --> [q]). -fof(a1_2, axiom, [q] --> [r]). -fof(f1, plain, [p | q] --> [r, q], inference(leftOr, [status(thm), 0], [a1_1, a1_2])). - -fof(a2_1, axiom, [p, q] --> []). -fof(a2_2, axiom, [s, t] --> []). -fof(f2, plain, [p, q | s, t] --> [], inference(leftOr, [status(thm), 1], [a2_1, a2_2])). - -fof(a3_1, axiom, [p, q] --> []). -fof(a3_2, axiom, [s, t] --> []). -fof(f3, plain, [p | t , q, s] --> [], inference(leftOr, [status(thm), 0], [a3_1, a3_2])). - -fof(a4_1, axiom, [P(X), Q(X)] --> [R & r(f(g(X, Y)))]). -fof(a4_2, axiom, [R & Q(X)] --> [R]). -fof(f4, plain, [P(X), Q(X) | (R & Q(X))] --> [R & r(f(g(X, Y))), R], inference(leftOr, [status(thm), 1], [a4_1, a4_2])). - -fof(a5_1, axiom, [![X]: (p(X) & q(X)), A] --> [(t(X) & u(Z)), v(f(c))]). -fof(a5_2, axiom, [(r(X) | s(X))] --> [(t(X) & u(Z))]). -fof(f5, plain, [A, ![X]: (p(X) & q(X)) | (r(X) | s(X))] --> [(t(X) & u(Z)), v(f(c))], inference(leftOr, [status(thm), 1], [a5_1, a5_2])). - - diff --git a/lisa-sets2/src/test/resources/steps_tests/leftSubst.p b/lisa-sets2/src/test/resources/steps_tests/leftSubst.p deleted file mode 100644 index a50f614e4..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftSubst.p +++ /dev/null @@ -1,15 +0,0 @@ -fof(a1, axiom, [q(a)] --> []). -fof(f1, plain, [a = b, q(b)] --> [], inference(leftSubst, [status(thm), 0, $fof(q(X)), 'X'], [a1])). - -fof(a2, axiom, [q(g(a, f(c)))] --> []). -fof(f2, plain, [a = b, q(g(b, f(c)))] --> [], inference(leftSubst, [status(thm), 0, $fof(q(g(X, f(c)))), 'X'], [a2])). - -fof(a3, axiom, [q(g(a, f(a)))] --> []). -fof(f3, plain, [a = b, q(g(b, f(a)))] --> [], inference(leftSubst, [status(thm), 0, $fof(q(g(X, f(a)))), 'X'], [a3])). - -fof(a3, axiom, [q(g(a, f(a)))] --> []). -fof(f3, plain, [q(g(b, f(b))), a = b] --> [], inference(leftSubst, [status(thm), 1, $fof(q(g(X, f(X)))), 'X'], [a3])). - -fof(a4, axiom, [![X] : q(g(X, f(c)))] --> []). -fof(f4, plain, [f(c) = g(c, c), ![X] : q(g(X, g(c, c)))] --> [], inference(leftSubst, [status(thm), 0, $fof(![Z] : q(g(Z, X))), 'X'], [a4])). - diff --git a/lisa-sets2/src/test/resources/steps_tests/leftSubstIff.p b/lisa-sets2/src/test/resources/steps_tests/leftSubstIff.p deleted file mode 100644 index c38dcc394..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftSubstIff.p +++ /dev/null @@ -1,15 +0,0 @@ -fof(a1, axiom, [q(s)] --> []). -fof(f1, plain, [q(s) <=> q(t), q(t)] --> [], inference(leftSubstIff, [status(thm), 0, $fof(K), 'K'], [a1])). - -fof(a2, axiom, [a & p(s, t)] --> []). -fof(f2, plain, [p(s, t) <=> q(t), a & q(t)] --> [], inference(leftSubstIff, [status(thm), 0, $fof(a & K), 'K'], [a2])). - -fof(a3, axiom, [q(s) & (q(t) | q(s))] --> []). -fof(f3, plain, [q(s) <=> q(t), q(t) & (q(t) | q(s))] --> [], inference(leftSubstIff, [status(thm), 0, $fof(K & (q(t) | q(s))), 'K'], [a3])). - -fof(a3, axiom, [~(q(s) & q(t)) => q(s)] --> []). -fof(f3, plain, [~(~(a & q(t)) & q(t)) => ~(a & q(t)), q(s) <=> ~(a & q(t))] --> [], inference(leftSubstIff, [status(thm), 1, $fof(~(K & q(t)) => K), 'K'], [a3])). - -fof(a4, axiom, [![X] : ~(q(s) & q(X))] --> []). -fof(f4, plain, [q(s) <=> q(X), ![Y] : ~(q(X) & q(Y))] --> [], inference(leftSubstIff, [status(thm), 0, $fof(![X] : ~(K & q(X))), 'K'], [a4])). - diff --git a/lisa-sets2/src/test/resources/steps_tests/leftWeaken.p b/lisa-sets2/src/test/resources/steps_tests/leftWeaken.p deleted file mode 100644 index 591ed0a36..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/leftWeaken.p +++ /dev/null @@ -1,12 +0,0 @@ - -fof(a1, axiom, [] --> [p]). -fof(f1, plain, [q] --> [p], inference(leftWeaken, [status(thm), 0], [a1])). -fof(f2, plain, [q, P(X)] --> [p], inference(leftWeaken, [status(thm), 1], [f1])). -fof(f3, plain, [q, P(X), Q(X, c)] --> [p], inference(leftWeaken, [status(thm), 2], [f2])). -fof(f4, plain, [q, ![X] : (P(X) | Q(a, X)), P(X), Q(X, c)] --> [p], inference(leftWeaken, [status(thm), 1], [f3])). -fof(f5, plain, [q, ![X] : (P(X) | Q(a, X)), P(X), Q(X, c)] --> [p], inference(leftWeaken, [status(thm), 2], [f4])). -fof(f6, plain, [q, ![Y] : (P(Y) | Q(a, Y)), P(X), Q(X, c), p1 => p2] --> [p], inference(leftWeaken, [status(thm), 4], [f5])). - - - - diff --git a/lisa-sets2/src/test/resources/steps_tests/rightAnd.p b/lisa-sets2/src/test/resources/steps_tests/rightAnd.p deleted file mode 100644 index e4b6db5ac..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightAnd.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1_1, axiom, [q] --> [p]). -fof(a1_2, axiom, [r] --> [q]). -fof(f1, plain, [r, q] --> [p & q], inference(rightAnd, [status(thm), 0], [a1_1, a1_2])). - -fof(a2_1, axiom, [] --> [p, q]). -fof(a2_2, axiom, [] --> [s, t]). -fof(f2, plain, [] --> [p, q & s, t], inference(rightAnd, [status(thm), 1], [a2_1, a2_2])). - -fof(a3_1, axiom, [] --> [p, q]). -fof(a3_2, axiom, [] --> [s, t]). -fof(f3, plain, [] --> [p & t , q, s], inference(rightAnd, [status(thm), 0], [a3_1, a3_2])). - -fof(a4_1, axiom, [R & r(f(g(X, Y)))] --> [P(X), Q(X)]). -fof(a4_2, axiom, [R] --> [R & Q(X)]). -fof(f4, plain, [R & r(f(g(X, Y))), R] --> [P(X), Q(X) & (R & Q(X))], inference(rightAnd, [status(thm), 1], [a4_1, a4_2])). - -fof(a5_1, axiom, [(t(X) & u(Z)), v(f(c))] --> [![X]: (p(X) & q(X)), A]). -fof(a5_2, axiom, [(t(X) & u(Z))] --> [(r(X) | s(X))]). -fof(f5, plain, [(t(X) & u(Z)), v(f(c))] --> [A, ![X]: (p(X) & q(X)) & (r(X) | s(X))], inference(rightAnd, [status(thm), 1], [a5_1, a5_2])). - - diff --git a/lisa-sets2/src/test/resources/steps_tests/rightEpsilon.p b/lisa-sets2/src/test/resources/steps_tests/rightEpsilon.p deleted file mode 100644 index e69de29bb..000000000 diff --git a/lisa-sets2/src/test/resources/steps_tests/rightExists.p b/lisa-sets2/src/test/resources/steps_tests/rightExists.p deleted file mode 100644 index 3b763e240..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightExists.p +++ /dev/null @@ -1,23 +0,0 @@ -fof(a1, axiom, [r] --> [p, q]). -fof(f1, plain, [r] --> [?[X] : p, q], inference(rightExists, [status(thm), 0, $fot(X)], [a1])). - -fof(a2, axiom, [r] --> [a, p(X)]). -fof(f2, plain, [r] --> [a, ?[X] : p(X)], inference(rightExists, [status(thm), 1, $fot(X)], [a2])). - -fof(a3, axiom, [R] --> [P(X), Q(f(c))]). -fof(f3, plain, [R] --> [P(X), ?[X] : Q(X)], inference(rightExists, [status(thm), 1, $fot(f(c))], [a3])). - - -fof(a4, axiom, [r(X, Y)] --> [p(X), q(g(Y, c)) | q(Y)]). -fof(f4, plain, [r(X, Y)] --> [p(X), ?[X] : (q(X) | q(Y))], inference(rightExists, [status(thm), 1, $fot(g(Y, c))], [a4])). - - -fof(a6, axiom, [(t(X) & u(X)), v(X)] --> [?[X]: (p(X) & q(f(c))), (r(X) | s(Y))]). -fof(f6, plain, [(t(X) & u(X)), v(X)] --> [?[Y, X]: (p(X) & q(Y)), (r(X) | s(Y))], inference(rightExists, [status(thm), 0, $fot(f(c))], [a6])). - -fof(a7, axiom, [] --> [q, ?[X]: (p(X) & q(f(c))), s(Y)]). -fof(f7, plain, [] --> [q, ?[X, Y]: (p(Y) & q(X)), s(Y)], inference(rightExists, [status(thm), 1, $fot(f(c))], [a7])). - - -fof(a7, axiom, [] --> [q, ?[X]: (p(X) & r(f(c), f(c))), s(Y)]). -fof(f7, plain, [] --> [q, ?[X, Y]: (p(Y) & r(X, X)), s(Y)], inference(rightExists, [status(thm), 1, $fot(f(c))], [a7])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/steps_tests/rightForall.p b/lisa-sets2/src/test/resources/steps_tests/rightForall.p deleted file mode 100644 index 82ba2a416..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightForall.p +++ /dev/null @@ -1,22 +0,0 @@ -fof(a1, axiom, [r] --> [p, q]). -fof(f1, plain, [r] --> [![X] : p, q], inference(rightForall, [status(thm), 0, 'X'], [a1])). - -fof(a2, axiom, [r] --> [a, p(X)]). -fof(f2, plain, [r] --> [a, ![X] : p(X)], inference(rightForall, [status(thm), 1, 'X'], [a2])). - -fof(a3, axiom, [R] --> [P(X), Q(Y)]). -fof(f3, plain, [R] --> [P(X), ![X] : Q(X)], inference(rightForall, [status(thm), 1, 'Y'], [a3])). - - -fof(a4, axiom, [r(X, Y)] --> [p(X), q(Z) | q(Y)]). -fof(f4, plain, [r(X, Y)] --> [p(X), ![X] : (q(X) | q(Y))], inference(rightForall, [status(thm), 1, 'Z'], [a4])). - - -fof(a6, axiom, [(t(X) & u(X)), v(X)] --> [![X]: (p(X) & q(Z)), (r(X) | s(Y))]). -fof(f6, plain, [(t(X) & u(X)), v(X)] --> [![Y, X]: (p(X) & q(Y)), (r(X) | s(Y))], inference(rightForall, [status(thm), 0, 'Z'], [a6])). - -fof(a7, axiom, [] --> [q, ![X]: (p(X) & q(Z)), s(Y)]). -fof(f7, plain, [] --> [q, ![X, Y]: (p(Y) & q(X)), s(Y)], inference(rightForall, [status(thm), 1, 'Z'], [a7])). - -fof(a8, axiom, [] --> [q, ![X]: (p(X) & r(Z, Z)), s(Y)]). -fof(f8, plain, [] --> [q, ![X, Y]: (p(Y) & r(X, X)), s(Y)], inference(rightForall, [status(thm), 1, 'Z'], [a8])). diff --git a/lisa-sets2/src/test/resources/steps_tests/rightIff.p b/lisa-sets2/src/test/resources/steps_tests/rightIff.p deleted file mode 100644 index 3c1075704..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightIff.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1_1, axiom, [q] --> [p=>q]). -fof(a1_2, axiom, [r] --> [q=>p]). -fof(f1, plain, [r, q] --> [p <=> q], inference(rightIff, [status(thm), 0], [a1_1, a1_2])). - -fof(a2_1, axiom, [] --> [p, q=>s]). -fof(a2_2, axiom, [] --> [s=>q, t]). -fof(f2, plain, [] --> [p, q <=> s, t], inference(rightIff, [status(thm), 1], [a2_1, a2_2])). - -fof(a3_1, axiom, [] --> [p=>t, q]). -fof(a3_2, axiom, [] --> [s, t=>p]). -fof(f3, plain, [] --> [p <=> t , q, s], inference(rightIff, [status(thm), 0], [a3_1, a3_2])). - -fof(a4_1, axiom, [R & r(f(g(X, Y)))] --> [P(X), Q(X)=>(R & Q(X))]). -fof(a4_2, axiom, [R] --> [(R & Q(X)) => Q(X)]). -fof(f4, plain, [R & r(f(g(X, Y))), R] --> [P(X), Q(X) <=> (R & Q(X))], inference(rightIff, [status(thm), 1], [a4_1, a4_2])). - -fof(a5_1, axiom, [(t(X) & u(Z)), v(f(c))] --> [![X]: (p(X) & q(X))=>(r(X) | s(X)), A]). -fof(a5_2, axiom, [(t(X) & u(Z))] --> [(r(X) | s(X)) => ![X]: (p(X) & q(X))]). -fof(f5, plain, [(t(X) & u(Z)), v(f(c))] --> [A, ![X]: (p(X) & q(X)) <=> (r(X) | s(X))], inference(rightIff, [status(thm), 1], [a5_1, a5_2])). - - diff --git a/lisa-sets2/src/test/resources/steps_tests/rightImplies.p b/lisa-sets2/src/test/resources/steps_tests/rightImplies.p deleted file mode 100644 index 9c0679f01..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightImplies.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1, axiom, [r, p] --> [q]). -fof(f1, plain, [r] --> [p => q], inference(rightImplies, [status(thm), 0], [a1])). - -fof(a2, axiom, [p, r] --> [a, q]). -fof(f2, plain, [r] --> [a, p => q], inference(rightImplies, [status(thm), 1], [a2])). - -fof(a3, axiom, [P(X), R] --> [Q(X)]). -fof(f3, plain, [R] --> [P(X) => Q(X)], inference(rightImplies, [status(thm), 0], [a3])). - -fof(a4, axiom, [p, u] --> [s, t, q]). -fof(f4, plain, [u] --> [s, p => q, t], inference(rightImplies, [status(thm), 1], [a4])). - -fof(a5, axiom, [r(X, Y), p(X)] --> [q(Y)]). -fof(f5, plain, [r(X, Y)] --> [p(X) => q(Y)], inference(rightImplies, [status(thm), 0], [a5])). - - -fof(a6, axiom, [![X]: (p(X) | q(X)), (t(X) | u(X)), v(X)] --> [(r(X) & s(X))]). -fof(f6, plain, [(t(X) | u(X)), v(X)] --> [![X]: (p(X) | q(X)) => (r(X) & s(X)), (r(X) & s(X))], inference(rightImplies, [status(thm), 0], [a6])). - -fof(a7, axiom, [q] --> [![X]: (p(X) | q(X)), s(Y)]). -fof(f7, plain, [] --> [![X]: (p(X) | q(X)), q => s(Y)], inference(rightImplies, [status(thm), 1], [a7])). diff --git a/lisa-sets2/src/test/resources/steps_tests/rightNot.p b/lisa-sets2/src/test/resources/steps_tests/rightNot.p deleted file mode 100644 index 6c9354d16..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightNot.p +++ /dev/null @@ -1,20 +0,0 @@ -fof(a1, axiom, [p] --> []). -fof(f1, plain, [] --> [~p], inference(rightNot, [status(thm), 0], [a1])). - -fof(a2, axiom, [r] --> [q]). -fof(f2, plain, [] --> [~r, q], inference(rightNot, [status(thm), 0], [a2])). - -fof(a3, axiom, [r, p] --> [q]). -fof(f3, plain, [p] --> [~r, q], inference(rightNot, [status(thm), 0], [a3])). - -fof(a4, axiom, [q(X)] --> [p(X)]). -fof(f4, plain, [] --> [p(X), ~q(X)], inference(rightNot, [status(thm), 1], [a4])). - -fof(a5, axiom, [![Y] : q(Y)] --> [p(X, Y)]). -fof(f5, plain, [] --> [~![Y] : q(Y), p(X, Y)], inference(rightNot, [status(thm), 0], [a5])). - -fof(a6, axiom, [r(Z), ![X] : (p(X) & q(Y))] --> [p(X) & q(Y)]). -fof(f6, plain, [r(Z)] --> [p(X) & q(Y), ~![X] :( p(X) & q(Y))], inference(rightNot, [status(thm), 1], [a6])). - -fof(a7, axiom, [r(c), ![X] : p(X)] --> []). -fof(f7, plain, [r(c)] --> [~![Y] : p(Y)], inference(rightNot, [status(thm), 0], [a7])). diff --git a/lisa-sets2/src/test/resources/steps_tests/rightOr.p b/lisa-sets2/src/test/resources/steps_tests/rightOr.p deleted file mode 100644 index 66dd70411..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightOr.p +++ /dev/null @@ -1,21 +0,0 @@ -fof(a1, axiom, [r] --> [p, q]). -fof(f1, plain, [r] --> [p | q], inference(rightOr, [status(thm), 0], [a1])). - -fof(a2, axiom, [r] --> [a, p, q]). -fof(f2, plain, [r] --> [a, p | q], inference(rightOr, [status(thm), 1], [a2])). - -fof(a3, axiom, [R] --> [P(X), Q(X)]). -fof(f3, plain, [R] --> [P(X) | Q(X)], inference(rightOr, [status(thm), 0], [a3])). - -fof(a4, axiom, [u] --> [s, p, t, q]). -fof(f4, plain, [u] --> [s, p | q, t], inference(rightOr, [status(thm), 1], [a4])). - -fof(a5, axiom, [r(X, Y)] --> [p(X), q(Y)]). -fof(f5, plain, [r(X, Y)] --> [p(X) | q(Y)], inference(rightOr, [status(thm), 0], [a5])). - - -fof(a6, axiom, [(t(X) | u(X)), v(X)] --> [![X]: (p(X) | q(X)), (r(X) & s(X))]). -fof(f6, plain, [(t(X) | u(X)), v(X)] --> [![X]: (p(X) | q(X)) | (r(X) & s(X)), (r(X) & s(X))], inference(rightOr, [status(thm), 0], [a6])). - -fof(a7, axiom, [] --> [q, ![X]: (p(X) | q(X)), s(Y)]). -fof(f7, plain, [] --> [![X]: (p(X) | q(X)), q | s(Y)], inference(rightOr, [status(thm), 1], [a7])). diff --git a/lisa-sets2/src/test/resources/steps_tests/rightRefl.p b/lisa-sets2/src/test/resources/steps_tests/rightRefl.p deleted file mode 100644 index ff7ad121a..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightRefl.p +++ /dev/null @@ -1,3 +0,0 @@ -fof(f1, plain, [r(c, d), p(X), a & b] --> [X = X], inference(rightRefl, [status(thm), 0], [])). - -fof(f2, plain, [r(c, d), p(X), a & b] --> [ p(X), a & b, g(X, c) = g(X, c)], inference(rightRefl, [status(thm), 2], [])). \ No newline at end of file diff --git a/lisa-sets2/src/test/resources/steps_tests/rightSubst.p b/lisa-sets2/src/test/resources/steps_tests/rightSubst.p deleted file mode 100644 index 7642c33b8..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightSubst.p +++ /dev/null @@ -1,15 +0,0 @@ -fof(a1, axiom, [] --> [q(a)]). -fof(f1, plain, [a = b] --> [q(b)], inference(rightSubst, [status(thm), 0, $fof(q(X)), 'X'], [a1])). - -fof(a2, axiom, [] --> [q(g(a, f(c)))]). -fof(f2, plain, [a = b] --> [q(g(b, f(c)))], inference(rightSubst, [status(thm), 0, $fof(q(g(X, f(c)))), 'X'], [a2])). - -fof(a3, axiom, [] --> [q(g(a, f(a)))]). -fof(f3, plain, [a = b] --> [q(g(b, f(a)))], inference(rightSubst, [status(thm), 0, $fof(q(g(X, f(a)))), 'X'], [a3])). - -fof(a3, axiom, [] --> [q(g(a, f(a)))]). -fof(f3, plain, [a = b] --> [q(g(b, f(b)))], inference(rightSubst, [status(thm), 0, $fof(q(g(X, f(X)))), 'X'], [a3])). - -fof(a4, axiom, [] --> [![X] : q(g(X, f(c)))]). -fof(f4, plain, [f(c) = g(c, c)] --> [![X] : q(g(X, g(c, c)))], inference(rightSubst, [status(thm), 0, $fof(![Z] : q(g(Z, X))), 'X'], [a4])). - diff --git a/lisa-sets2/src/test/resources/steps_tests/rightSubstIff.p b/lisa-sets2/src/test/resources/steps_tests/rightSubstIff.p deleted file mode 100644 index c349afc68..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightSubstIff.p +++ /dev/null @@ -1,15 +0,0 @@ -fof(a1, axiom, [] --> [q(s)]). -fof(f1, plain, [q(s) <=> q(t)] --> [q(t)], inference(rightSubstIff, [status(thm), 0, $fof(K), 'K'], [a1])). - -fof(a2, axiom, [] --> [a & p(s, t)]). -fof(f2, plain, [p(s, t) <=> q(t)] --> [a & q(t)], inference(rightSubstIff, [status(thm), 0, $fof(a & K), 'K'], [a2])). - -fof(a3, axiom, [] --> [q(s) & (q(t) | q(s))]). -fof(f3, plain, [q(s) <=> q(t)] --> [ q(t) & (q(t) | q(s))], inference(rightSubstIff, [status(thm), 0, $fof(K & (q(t) | q(s))), 'K'], [a3])). - -fof(a3, axiom, [] --> [~(q(s) & q(t)) => q(s)]). -fof(f3, plain, [q(s) <=> ~(a & q(t))] --> [~(~(a & q(t)) & q(t)) => ~(a & q(t))], inference(rightSubstIff, [status(thm), 0, $fof(~(K & q(t)) => K), 'K'], [a3])). - -fof(a4, axiom, [] --> [![X] : ~(q(s) & q(X))]). -fof(f4, plain, [q(s) <=> q(X)] --> [![Y] : ~(q(X) & q(Y))], inference(rightSubstIff, [status(thm), 0, $fof(![X] : ~(K & q(X))), 'K'], [a4])). - diff --git a/lisa-sets2/src/test/resources/steps_tests/rightWeaken.p b/lisa-sets2/src/test/resources/steps_tests/rightWeaken.p deleted file mode 100644 index 9006afa9c..000000000 --- a/lisa-sets2/src/test/resources/steps_tests/rightWeaken.p +++ /dev/null @@ -1,12 +0,0 @@ - -fof(a1, axiom, [p] --> []). -fof(f1, plain, [p] --> [q], inference(rightWeaken, [status(thm), 0], [a1])). -fof(f2, plain, [p] --> [q, P(X)], inference(rightWeaken, [status(thm), 1], [f1])). -fof(f3, plain, [p] --> [q, P(X), Q(X, c)], inference(rightWeaken, [status(thm), 2], [f2])). -fof(f4, plain, [p] --> [q, ![X] : (P(X) | Q(a, X)), P(X), Q(X, c)], inference(rightWeaken, [status(thm), 1], [f3])). -fof(f5, plain, [p] --> [q, ![X] : (P(X) | Q(a, X)), P(X), Q(X, c)], inference(rightWeaken, [status(thm), 2], [f4])). -fof(f6, plain, [p] --> [q, ![Y] : (P(Y) | Q(a, Y)), P(X), Q(X, c), p1 => p2], inference(rightWeaken, [status(thm), 4], [f5])). - - - -