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

Instanciations

To: pvs-help@csl.sri.com
Subject: Instanciations
From: Laurent FERIER <lfe@info.fundp.ac.be>
Date: Wed, 02 Dec 1998 12:47:11 +0100
Cc: lfe.leibniz.info.fundp.ac.be@fundp.ac.be
Organization: Institut d'Informatique - FUNDP Namur

Hello!

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
mailto:lfe@info.fundp.ac.be

Prev by Date: Question about With
Next by Date: Instanciating unboud varaibles
Prev by thread: Re: Instanciating unboud varaibles
Next by thread: Instanciations
Index(es):
- Date
- Thread