Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Message-Id: <199111070123.AA09813@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: witnesses
Date: Wed, 06 Nov 91 17:23:07 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>


How does one go about solving a goal like this one (obviuosly trivialized
to show the point):

g(
"? x:* . I x = x"
);;

Is this a theorem?????  I just ran up against it and its time to go home,
so I haven't had time to think it through.  I believe its a theorem, but...

This

e(
EXISTS_TAC "5"
);;

won't work since the type variables need to be instatiated.  One could
rewrite EXISTS_TAC, except that the validity proof would require changing

   I (x:num) = x

into

   I (x:*) = x


and INST_TYPE doesn't work backwards.

It seems like this says (is we could quantify over type vars):

?- ! * . ? x:* . I x = x

This is true, but the proof seems to ask for some sort of infinite case
analysis on the type var.

Am I making too much of something simple??? Ideas???

--phil--


Phil Windley                          |  windley@cs.uidaho.edu
Assistant Professor                   |  windley@cheetah.cs.uidaho.edu
Department of Computer Science        |
University of Idaho                   |  Phone: 208.885.6501
Moscow, ID 83843                      |  Fax:   208.885.6645