|
From: | Tim Daly |
Subject: | Re: [Axiom-developer] Fwd: Request for references |
Date: | Wed, 13 Dec 2017 11:36:15 -0500 |
Hi Tim,
I missed you yesterday, but I've added jguidry899 on skype now. 3pm my time usually works.
Best,
Florian
On 11.12.2017 15:12, Tim Daly wrote:
I tried to Skype but it failed.
I tried to call but it failed.
Lets use email.
I'll write later today.
Tim
On Sun, Dec 10, 2017 at 10:13 PM, Tim Daly <address@hidden> wrote:
There is a 6 hour time difference between Pittsburgh and
Berlin. I'll try to skype with you at 3pm your time (9am mine).
I'll be using the skype id jguidry899 as skype doesn't seem
to like any of my prior passwords for my normal id.
If this is not convenient, please let me know.
Tim
On Thu, Dec 7, 2017 at 1:51 PM, Florian Rabe <address@hidden>
wrote:
Yes, I'll be around.
Skype: florian.rabe
WhatsApp/cell phone: +49 1520 5321277
On 07.12.2017 17:47, Tim Daly wrote:
I'm a bit buried at the moment. I printed out your "top 5" papers.
I plan to read them over the weekend so I understand what you're doing.
Are you available some time next week? I have the whole week free.
Tim
On Thu, Dec 7, 2017 at 6:53 AM, Florian Rabe <address@hidden
<mailto:address@hidden>> wrote:
Hi Tim,
I'm exactly the right person to contact about this.
I'm CC'ing Michael Kohlhase with whom I ran the LATIN project a few
years ago, whose goal was to form at atlas of logics in this style.
The logical framework LF was developed for that purpose and my MMT
framework significantly abstracts from and generalizes the LF results.
You can find the most relevant papers at
https://uniformal.github.io/doc/philosophy/papers.html <
https://uniformal.github.io/doc/philosophy/papers.html >
We strongly commend any work on Axion that takes these logical
framework ideas into account.
An integration of our systems (which are good for defining the
logics) with Axiom (which needs to use the logics to verify results) would
be very interesting.
However, as your second email indicates you have found out already
yourself by now, the problem is quite hard.
Therefore, depending on your interests and available resources, I
have wildly different advice on how to proceed.
Maybe we should have a phone call about this?
Best,
Florian
On 06.12.2017 14:47, Tim Daly wrote:
James Davenport suggested I forward this question to you.
...
I'm trying to prove Axiom correct. (http://axiom-developer.org)
Axiom draws its power from organizing algorithms based on group
theory, adding propositions as the complexity increases. This
helps
limit the assumptions needed to provide algorithms.
Recently I've learned a bit about substructural and (super?)
structural
logics. So, for example, given the propositions
(W) Weakening
(C) Contraction
(E) Exchange
they can be combined to form (Crary):
W & C & E ==> Persistant logic.
W & ~C & E ==> Affine logic
~W & C & E ==> Strict logic
~W & ~C & E ==> Linear logic
W & C & ~E ==> ?
W & ~C & ~E ==> ?
~W & C & ~E ==> ?
~W & ~C & ~E ==> Ordered logic
In addition, there appears to be a group theory-like
organization of
logics above the substructural e.g. predicate, simply-typed
lambda,
and lambda calculus (Avigad).
Organizing these logics by the gradual introduction of
propositions
and properties would fit exactly into Axiom's structure and make
proof assumptions clear. I want to organize these in Axiom so the
proofs inherit the required logic.
Can you give me any references to a group-theory-like
organization
of the various logics, similar to the above? I have done a
literature
search but have not found anything yet.
Thank you.
Tim Daly
[Prev in Thread] | Current Thread | [Next in Thread] |