[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] Translating Mizar into some standard FOPL-like format?

To: mizar-forum@mizar.uwb.edu.pl
Subject: [mizar] Translating Mizar into some standard FOPL-like format?
From: "Ben Goertzel" <ben@goertzel.org>
Date: Tue, 21 Oct 2008 21:09:31 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:mime-version:content-type :x-google-sender-auth; b=ISCx0fLBJUsg9nxZf8YAU5O5Usq2LvlaQ0qxiAkSSqRhkLNpSW0mnxFrer7QB+3M43 HZV8D2N8fCh8zgvXhAGJRpPfrKBxiVb6gHQP/UDX5SS1pprNzyutLWuJOCHBaWGWUszx trzn6cYjbTW4dZyEw2jrf/OBZ03n8iANiqM7s=

Hi,

I haven't kept up with this list lately, and I'm curious what is the current state of efforts to translate the Mizar corpus of theorems and proofs into some fairly standard first-order-predicate-logic-like formalism?

Has this been done by now? If so is the translated version of Mizar available?

If not, what is your general thinking about the most desirable "target formalism" for the translation effort ... and, what is the status of partially-complete efforts?

thanks
Ben Goertzel

Prev by Date: [mizar] Revising UPROOTS: Global Choine
Next by Date: Re: [mizar] Translating Mizar into some standard FOPL-like format?
Index(es):
- Chronological
- Thread