[Top][All Lists]

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

[Axiom-developer] Request for references

From: Tim Daly
Subject: [Axiom-developer] Request for references
Date: Wed, 6 Dec 2017 04:06:50 -0500

I'm trying to prove Axiom correct.

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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]