[Gcl-devel] HOL (was Re: closed world)

[Camm Maguire]

Matt Kaufmann <address@hidden> writes:

> Hi, John --
> 
> Just to add (to J's answers) an explicit answer to your final
> question:
> 
> >> Finally, what would happen
> >> if one were to add an axiom like this to ACL2? 
> 
> It's sound to add such an axiom.  If you do so, then you are
> restricting the set of models to which ACL2 applies.  For example, if
> someone wants to formalize a web universe in which there are objects
> around other than the basic ones you mention, then they couldn't
> include a book that has the axiom you mention.
> 
> And here's another reason to avoid such an axiom:
> 
> By the way, in the embedding of ACL2 into HOL reported on at this
> summer's ACL2 workshop, it was convenient to define an ACL2 model in
> HOL with objects that are not all the basic ones you mention.  (In
> case you're curious, we formalized ACL2 symbols as something like HOL
> pairs <package_name, symbol_name>, but where "ill-formed" pairs such
> as <"ACL2", "CAR"> are not considered to be symbols (in this case
> because the symbol-package-name of acl2::car is "COMMON-LISP", not
> "ACL2").)
> 

Hi Matt!  Just wanted to point out something that might be useful to
you all -- I've uploaded a package of HOL88 built atop gcl to Debian,
which of course includes its own ML implementation written in lisp.
In principle one could embed HOL into ACL2, if desired.

Take care,

> -- Matt
>    X-IronPort-MID: 85061174
>    X-SBRS: 3.5
>    X-BrightmailFiltered: true
>    X-Brightmail-Tracker: AAAAAA==
>    X-IronPort-AV: i="4.09,386,1157346000"; 
>       d="scan'208"; a="85061174:sNHT20179776"
>    Date: Fri, 3 Nov 2006 16:36:31 -0600
>    From: John Erickson <address@hidden>
>    Content-Disposition: inline
>    Reply-To: address@hidden
>    Sender: address@hidden
>    X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
>    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
>    X-UTCS-Spam-Status: No, hits=-142 required=200
> 
>    It is my understanding that ACL2 is not a 'closed world' logic, in
>    other words there is no theorem of the form (or (integerp x)
>    (stringp x) (symbolp x) ... ).  I have a few questions about this.
>    First, is this a correct characterization of ACL2?  Second, is there
>    any particular reason for this choice?  Finally, what would happen
>    if one were to add an axiom like this to ACL2? 
> 
>    John
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah