search

meta-logic / lltp

TPTP linear logic version
GNU General Public License v3.0
13 stars 2 forks source link

minor clarifications #6

Closed vcvpaiva closed 4 years ago

vcvpaiva commented 4 years ago

hi Giselle,

Kleene's book has both classical and intuitionsitic theorems, actually one has to read the section carefully to find only the intuitonistic ones, hence my "clarification". but sure I don't mind not adding "classical", but I wish we could give it (and some other things mentioned) a better bibliography description.

about two, I do object to calling them call-by-name and call-by-value, as I think these names are misleading. The translations exist in pure logic, where no evaluation mechanism needs to be mentioned. Using either translation you can have both a call-by-name and a call-by-value evaluation mechanism. Yes, I agree that this is a widespread convention and many people use it for the two Girard's translations as a shortcut, but I still think this is a bad use of these names and personally I do not want to perpetuate it.

Thanks! Valeria

On Fri, May 8, 2020 at 3:37 AM Giselle Reis notifications@github.com wrote:

@gisellemnr commented on this pull request.

Hi Valeria,

Thanks for the edits! I left a few comments on the pull request before merging.

Best, Giselle

In README.md https://github.com/meta-logic/lltp/pull/6#discussion_r422070819:

-Benchmark of problems for linear logic provers +a benchmark of problems for linear logic provers

Maybe use uppercase A?

In README.md https://github.com/meta-logic/lltp/pull/6#discussion_r422071108:

@@ -25,11 +25,11 @@ specified as fof(name, axiom, F) and fof(name, conjecture, F) respective

Intuitionistic problems

The collection of intuitionistic problems is described in [4] and it can be found in the directory ILL. The problems were obtained from three main sources:

-1. Kleene's problems for intuitionistic logic from "Introduction to Metamathematics" +1. Kleene's theorems for classic and intuitionistic logic from "Introduction to Metamathematics" (New York: van Nostrand, 1952)

This is a list of where the intuitionistic problems come from, so shouldn't we only mention Kleene's intuitionistic problems?

In README.md https://github.com/meta-logic/lltp/pull/6#discussion_r422071635:

  1. Intuitionistic Logic Theorem Provers library ILTP
    1. Petri-nets from the Model Checking Contest

-The collections ILLTP-\* and KLE-\* are obtained via the translations call-by-name, call-by-value [1] and Liang and Miller's 0/1 [2], +The collections ILLTP-\* and KLE-\* are obtained via the Girard translations in [1] and Liang and Miller's 0/1 [2],

I would keep call-by-name and call-by-value (even if only in parentheses) since there are people who may identify more immediately the transformations by these names.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/meta-logic/lltp/pull/6#pullrequestreview-408150057, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIZ3H5MDOSM5GMCFBQ2PEDRQPOGVANCNFSM4M4ACAGQ .

-- Valeria de Paiva http://vcvpaiva.github.io/ http://www.cs.bham.ac.uk/~vdp/

vcvpaiva commented 4 years ago

one way to solve this might be to say

The collections ILLTP-\* and KLE-\* are obtained via the Girard translations in [1] (sometimes called call-by-name and call-by-value translations) and Liang and Miller's 0/1 [2],

thanks for dealing with this!

On Fri, May 8, 2020 at 10:08 AM Valeria de Paiva valeria.depaiva@gmail.com wrote:

hi Giselle,

Kleene's book has both classical and intuitionsitic theorems, actually one has to read the section carefully to find only the intuitonistic ones, hence my "clarification". but sure I don't mind not adding "classical", but I wish we could give it (and some other things mentioned) a better bibliography description.

about two, I do object to calling them call-by-name and call-by-value, as I think these names are misleading. The translations exist in pure logic, where no evaluation mechanism needs to be mentioned. Using either translation you can have both a call-by-name and a call-by-value evaluation mechanism. Yes, I agree that this is a widespread convention and many people use it for the two Girard's translations as a shortcut, but I still think this is a bad use of these names and personally I do not want to perpetuate it.

Thanks! Valeria

On Fri, May 8, 2020 at 3:37 AM Giselle Reis notifications@github.com wrote:

@gisellemnr commented on this pull request.

Hi Valeria,

Thanks for the edits! I left a few comments on the pull request before merging.

Best, Giselle

In README.md https://github.com/meta-logic/lltp/pull/6#discussion_r422070819:

-Benchmark of problems for linear logic provers +a benchmark of problems for linear logic provers

Maybe use uppercase A?

In README.md https://github.com/meta-logic/lltp/pull/6#discussion_r422071108:

@@ -25,11 +25,11 @@ specified as fof(name, axiom, F) and fof(name, conjecture, F) respective

Intuitionistic problems

The collection of intuitionistic problems is described in [4] and it can be found in the directory ILL. The problems were obtained from three main sources:

-1. Kleene's problems for intuitionistic logic from "Introduction to Metamathematics" +1. Kleene's theorems for classic and intuitionistic logic from "Introduction to Metamathematics" (New York: van Nostrand, 1952)

This is a list of where the intuitionistic problems come from, so shouldn't we only mention Kleene's intuitionistic problems?

In README.md https://github.com/meta-logic/lltp/pull/6#discussion_r422071635:

  1. Intuitionistic Logic Theorem Provers library ILTP
    1. Petri-nets from the Model Checking Contest

-The collections ILLTP-\* and KLE-\* are obtained via the translations call-by-name, call-by-value [1] and Liang and Miller's 0/1 [2], +The collections ILLTP-\* and KLE-\* are obtained via the Girard translations in [1] and Liang and Miller's 0/1 [2],

I would keep call-by-name and call-by-value (even if only in parentheses) since there are people who may identify more immediately the transformations by these names.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/meta-logic/lltp/pull/6#pullrequestreview-408150057, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIZ3H5MDOSM5GMCFBQ2PEDRQPOGVANCNFSM4M4ACAGQ .

-- Valeria de Paiva http://vcvpaiva.github.io/ http://www.cs.bham.ac.uk/~vdp/

-- Valeria de Paiva http://vcvpaiva.github.io/ http://www.cs.bham.ac.uk/~vdp/

gisellemnr commented 4 years ago

I see your point. I'll add the clarification in parenthesis. Thanks!

vcvpaiva commented 4 years ago

thanks!!

On Sat, May 9, 2020 at 2:25 AM Giselle Reis notifications@github.com wrote:

I see your point. I'll add the clarification in parenthesis. Thanks!

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/meta-logic/lltp/pull/6#issuecomment-626136153, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIZ3H26WF3XDQKOOFCCKR3RQUOSFANCNFSM4M4ACAGQ .

-- Valeria de Paiva http://vcvpaiva.github.io/ http://www.cs.bham.ac.uk/~vdp/