diff --git a/LISA Reference Manual.pdf b/LISA Reference Manual.pdf
index 906435e4e6b5d7fcd132c57896cf07d86704556e..a4f64cbc8843cd905e63b0b863119832574abcc8 100644
Binary files a/LISA Reference Manual.pdf and b/LISA Reference Manual.pdf differ
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index c5d2967ded8c571b051e165f166bf87c27d894cc..6f27c597e980e9b2eaa4b6ba79ea9c7e6f5aaa12 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -258,6 +258,8 @@ object Printer {
case RightSubstEq(_, t1, _, _, _, _) => pretty("R. SubstEq", t1)
case LeftSubstIff(_, t1, _, _, _, _) => pretty("L. SubstIff", t1)
case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
+ case InstFunSchema(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
+ case InstPredSchema(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
case SCSubproof(_, _, false) => pretty("SCSubproof (hidden)")
case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
}
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 8e1e772bde023e8c6bb5f7494a29e34e43620ce8..da0ab913031b47a7465a2d510c4568b47676060f 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -112,7 +112,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* Those variables are replaced by the actual arguments of p.
* @return phi[psi(a1,..., an)/p]
*/
- def instantiatePredicateSchema(phi: Formula, p: SchematicPredicateLabel, psi: Formula, a: List[VariableLabel]): Formula = {
+ def instantiatePredicateSchema(phi: Formula, p: SchematicPredicateLabel, psi: Formula, a: Seq[VariableLabel]): Formula = {
require(a.length == p.arity)
phi match {
case PredicateFormula(label, args) =>
@@ -139,7 +139,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* Those variables are replaced by the actual arguments of f.
* @return phi[r(a1,..., an)/f]
*/
- def instantiateFunctionSchema(phi: Formula, f: SchematicFunctionLabel, r: Term, a: List[VariableLabel]): Formula = {
+ def instantiateFunctionSchema(phi: Formula, f: SchematicFunctionLabel, r: Term, a: Seq[VariableLabel]): Formula = {
require(a.length == f.arity)
phi match {
case PredicateFormula(label, args) => PredicateFormula(label, args.map(instantiateFunctionSchema(_, f, r, a)))
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 03411af89036811ad6b942419ba3f739c7daccfc..25c23e0e72aab95c21e93f1c7d0f1121d958388b 100644
--- a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -87,7 +87,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
* Those variables are replaced by the actual arguments of f.
* @return t[r(a1,..., an)/f]
*/
- def instantiateFunctionSchema(t: Term, f: SchematicFunctionLabel, r: Term, a: List[VariableLabel]): Term = {
+ def instantiateFunctionSchema(t: Term, f: SchematicFunctionLabel, r: Term, a: Seq[VariableLabel]): Term = {
require(a.length == f.arity)
t match {
case VariableTerm(label) => t
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 372699abbe43d3a6f84c9d4e505cfc843ca599d2..11fd361ef0fb440dbc07828fa64b5fdc4f7422b2 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -401,6 +401,35 @@ object SCProofChecker {
else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
else (false, Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
else (false, Nil, "Predicate schema ?q must have arity 0.")
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------------------
+ * Γ[r(a)/?f] |- Δ[r(a)/?f]
+ * </pre>
+ */
+ case InstFunSchema(bot, t1, f, r, a) =>
+ val expected = (ref(t1).left.map(phi => instantiateFunctionSchema(phi, f, r, a)), ref(t1).right.map(phi => instantiateFunctionSchema(phi, f, r, a)))
+ if (isSameSet(bot.left, expected._1))
+ if (isSameSet(bot.right, expected._2))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
+ else (false, Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
+
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------------------
+ * Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
+ * </pre>
+ */
+ case InstPredSchema(bot, t1, p, psi, a) =>
+ val expected = (ref(t1).left.map(phi => instantiatePredicateSchema(phi, p, psi, a)), ref(t1).right.map(phi => instantiatePredicateSchema(phi, p, psi, a)))
+ if (isSameSet(bot.left, expected._1))
+ if (isSameSet(bot.right, expected._2))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
+ else (false, Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
case SCSubproof(sp, premises, _) =>
if (premises.size == sp.imports.size){
@@ -409,7 +438,7 @@ object SCProofChecker {
val r_subproof = checkSCProof(sp)
if (r_subproof._1)
(true, Nil, "")
- else (false, r_subproof._2, "Subproof reports an error:\n"+r_subproof._3)
+ else (false, r_subproof._2, r_subproof._3)
} else (false, Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
} else (false, Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index cf79543367bde60c6c3ce6827dff22f56f695eaf..5c1470c96a5535899cd8a828835a3128ec1e6fe1 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -1,6 +1,7 @@
package lisa.kernel.proof
-import lisa.kernel.fol.FOL._
+import lisa.kernel.fol.FOL.*
+
import scala.collection.immutable.Set
@@ -262,20 +263,36 @@ object SequentCalculus {
case class RightSubstEq(bot: Sequent, t1: Int, s: Term, t: Term, phi: Formula, f: SchematicFunctionLabel) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
- * Γ, φ[a/h] |- Δ
+ * Γ, φ[a/?p] |- Δ
* ---------------------
- * Γ, a↔b, φ[b/h] |- Δ
+ * Γ, a↔b, φ[b/?p] |- Δ
* </pre>
*/
case class LeftSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
- * Γ |- φ[a/h], Δ
+ * Γ |- φ[a/?p], Δ
* ---------------------
- * Γ, a↔b |- φ[b/h], Δ
+ * Γ, a↔b |- φ[b/?p], Δ
* </pre>
*/
case class RightSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------------------
+ * Γ[r(a)/?f] |- Δ[r(a)/?f]
+ * </pre>
+ */
+ case class InstFunSchema(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] )
+ /**
+ * <pre>
+ * Γ |- Δ
+ * --------------------------
+ * Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
+ * </pre>
+ */
+ case class InstPredSchema(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] )
// Proof Organisation rules
case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display:Boolean = true) extends SCProofStep {