[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]



I've got some problem when using the inst and instanciate prover
instructions, can anybody tell me what I do wrong?

The antecedent is something like

 {-1}  FORALL (I1 : T1, I2 : T1, x : T2) : something involving I1, I2, x

* inst? instanciates that formula with skolem variables (from another
  formula) I1!1, I2!1 and nothing for x. 
* I would like to instanciate that formula with I2!1, I1!1 and nothing
  for x. I tried with 

   (inst -1 "I2!1" "I1!1" "-")

  which does not work (no change on (INST...)). I alos tried other 
  things, but they do not work either. What's the problem????

Thanks you

Laurent Ferier
FUNDP - Namur, Belgium