search

proofcert / checkers

This is not a game.
3 stars 2 forks source link

Ordinary Sequents Implementation #6

Closed shaolintl closed 7 years ago

shaolintl commented 7 years ago

See wiki about general idea.

Marco, I have a question. I figured out how to deal with the box/diamond idea but what are the H and F that we need to give to the diamonds? to the box?

emmevolpe commented 7 years ago

Hi Tomer! If I understand it correctly, at a modal rule you treat one box and several diamonds. Now:

H only changes at the last diamond (and takes the index of the box-formula). F is irrelevant for the box (can be 'none') and is equal to the index of the box-formula for the diamonds.

In case you are using the constructors for some reason, please notice that an index of the form: diaind index index is used for the child of a diamond-formula and not for the diamond-formula itself (there was a bug about this in the fpc for lmf-star).

emmevolpe commented 7 years ago

Small comment. It's not clear to me from the wiki and I think that in our implementation this does not affect anything, however, only diamond-formulas (and not the box-formula) should have the same MFI. In principle, multifocusing on both boxes and diamonds would be a mistake.

shaolintl commented 7 years ago

ok, I thought of adding MFI later since right now we are not doing anything with the index anyway... I will at least try to set it properly.

On 4 November 2016 at 17:50, emmevolpe notifications@github.com wrote:

Small comment. It's not clear to me from the wiki and I think that in our implementation this does not affect anything, however, only diamond-formulas (and not the box-formula) should have the same MFI. In principle, multifocusing on both boxes and diamonds would be a mistake.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258485859, or mute the thread https://github.com/notifications/unsubscribe-auth/AFj8VSCrnApUNWbNtwZCFOeFGmVEk1wIks5q62JrgaJpZM4KpvHR .

emmevolpe commented 7 years ago

I know it can look redundant, but maybe we should really add a simple LMF_OS layer that checks these things. It would give a sense to the use of multifocusing and keep us closer to the AiML paper.

The idea then would be:

On 04/11/2016 17:52, shaolintl wrote:

ok, I thought of adding MFI later since right now we are not doing anything with the index anyway... I will at least try to set it properly.

On 4 November 2016 at 17:50, emmevolpe notifications@github.com wrote:

Small comment. It's not clear to me from the wiki and I think that in our implementation this does not affect anything, however, only diamond-formulas (and not the box-formula) should have the same MFI. In principle, multifocusing on both boxes and diamonds would be a mistake.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258485859, or mute the thread

https://github.com/notifications/unsubscribe-auth/AFj8VSCrnApUNWbNtwZCFOeFGmVEk1wIks5q62JrgaJpZM4KpvHR .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258486303, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBD72S25GUiCqdVYsDv3w59TZ6ybOwks5q62LPgaJpZM4KpvHR.

shaolintl commented 7 years ago

It indeed seems redundant to me. The whole idea of FPC is to emulate things and if a layer is used only for one subclass, then it is redundant, no?

On 4 November 2016 at 18:06, emmevolpe notifications@github.com wrote:

I know it can look redundant, but maybe we should really add a simple LMF_OS layer that checks these things. It would give a sense to the use of multifocusing and keep us closer to the AiML paper.

The idea then would be:

  • OrdinarySequents takes a concrete OS proof and makes it checkable by the framework;
  • LMFOS is the instantiation of LMF* that forces it to emulate OS systems and one could use it even without having a concrete proof to check.

On 04/11/2016 17:52, shaolintl wrote:

ok, I thought of adding MFI later since right now we are not doing anything with the index anyway... I will at least try to set it properly.

On 4 November 2016 at 17:50, emmevolpe notifications@github.com wrote:

Small comment. It's not clear to me from the wiki and I think that in our implementation this does not affect anything, however, only diamond-formulas (and not the box-formula) should have the same MFI. In principle, multifocusing on both boxes and diamonds would be a mistake.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <https://github.com/proofcert/checkers/issues/6#issuecomment-258485859 , or mute the thread

https://github.com/notifications/unsubscribe-auth/ AFj8VSCrnApUNWbNtwZCFOeFGmVEk1wIks5q62JrgaJpZM4KpvHR .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258486303, or mute the thread https://github.com/notifications/unsubscribe-auth/ AQoBD72S25GUiCqdVYsDv3w59TZ6ybOwks5q62LPgaJpZM4KpvHR.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258490217, or mute the thread https://github.com/notifications/unsubscribe-auth/AFj8VQYgiE5FNjXyKbXsGOCZJE7X6a_2ks5q62YdgaJpZM4KpvHR .

emmevolpe commented 7 years ago

OK!

On 04/11/2016 18:08, shaolintl wrote:

It indeed seems redundant to me. The whole idea of FPC is to emulate things and if a layer is used only for one subclass, then it is redundant, no?

On 4 November 2016 at 18:06, emmevolpe notifications@github.com wrote:

I know it can look redundant, but maybe we should really add a simple LMF_OS layer that checks these things. It would give a sense to the use of multifocusing and keep us closer to the AiML paper.

The idea then would be:

  • OrdinarySequents takes a concrete OS proof and makes it checkable by the framework;
  • LMFOS is the instantiation of LMF* that forces it to emulate OS systems and one could use it even without having a concrete proof to check.

On 04/11/2016 17:52, shaolintl wrote:

ok, I thought of adding MFI later since right now we are not doing anything with the index anyway... I will at least try to set it properly.

On 4 November 2016 at 17:50, emmevolpe notifications@github.com wrote:

Small comment. It's not clear to me from the wiki and I think that in our implementation this does not affect anything, however, only diamond-formulas (and not the box-formula) should have the same MFI. In principle, multifocusing on both boxes and diamonds would be a mistake.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <https://github.com/proofcert/checkers/issues/6#issuecomment-258485859 , or mute the thread

https://github.com/notifications/unsubscribe-auth/ AFj8VSCrnApUNWbNtwZCFOeFGmVEk1wIks5q62JrgaJpZM4KpvHR .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258486303, or mute the thread https://github.com/notifications/unsubscribe-auth/ AQoBD72S25GUiCqdVYsDv3w59TZ6ybOwks5q62LPgaJpZM4KpvHR.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258490217, or mute the thread

https://github.com/notifications/unsubscribe-auth/AFj8VQYgiE5FNjXyKbXsGOCZJE7X6a_2ks5q62YdgaJpZM4KpvHR .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258490766, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBDxB5et0AXIIQunekoMEhC9hnadRnks5q62aggaJpZM4KpvHR.

shaolintl commented 7 years ago

ok, I have finished the first, buggy, version. Note that there might also be conceptual bugs.

You can see that in the translation from osequent to lmf-star, i dont expect any information in the node except:

When translating back from lmf-star to osequents, i lose all the information in the nodes, except optional index and index).

Anyway, you can checkout the branch and do the example..

emmevolpe commented 7 years ago

Thank you, Tomer!

If I work in the OS branch, do I have to merge the new lmf-star there too?

Il 04 nov 2016 7:08 PM, "shaolintl" notifications@github.com ha scritto:

ok, I have finished the first, buggy, version. Note that there might also be conceptual bugs.

You can see that in the translation from osequent to lmf-star, i dont expect any information in the node except:

  • for init, the optional index
  • for box, the list of diamond indices In addition, I dont have a state for osequents and just receive as argument the lmf-star-cert, which means that the state is the one included in this certificate (lmf-star and lmf-singlefoc).

When translating back from lmf-star to osequents, i lose all the information in the nodes, except optional index and index).

Anyway, you can checkout the branch and do the example..

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258506672, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBDzVoO9ocwJ42sdIaXdS87tDCN0aDks5q63SugaJpZM4KpvHR .

shaolintl commented 7 years ago

you should merge it to master and I will rebase the new branch with your changes if you want.

On 4 November 2016 at 19:16, emmevolpe notifications@github.com wrote:

Thank you, Tomer!

If I work in the OS branch, do I have to merge the new lmf-star there too?

Il 04 nov 2016 7:08 PM, "shaolintl" notifications@github.com ha scritto:

ok, I have finished the first, buggy, version. Note that there might also be conceptual bugs.

You can see that in the translation from osequent to lmf-star, i dont expect any information in the node except:

  • for init, the optional index
  • for box, the list of diamond indices In addition, I dont have a state for osequents and just receive as argument the lmf-star-cert, which means that the state is the one included in this certificate (lmf-star and lmf-singlefoc).

When translating back from lmf-star to osequents, i lose all the information in the nodes, except optional index and index).

Anyway, you can checkout the branch and do the example..

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258506672, or mute the thread https://github.com/notifications/unsubscribe-auth/ AQoBDzVoO9ocwJ42sdIaXdS87tDCN0aDks5q63SugaJpZM4KpvHR

.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258508637, or mute the thread https://github.com/notifications/unsubscribe-auth/AFj8VTV4LeHB3Tuj399_EIyuyou17t7Jks5q63aGgaJpZM4KpvHR .

emmevolpe commented 7 years ago

It's already merged to master.

Il 04 nov 2016 7:19 PM, "shaolintl" notifications@github.com ha scritto:

you should merge it to master and I will rebase the new branch with your changes if you want.

On 4 November 2016 at 19:16, emmevolpe notifications@github.com wrote:

Thank you, Tomer!

If I work in the OS branch, do I have to merge the new lmf-star there too?

Il 04 nov 2016 7:08 PM, "shaolintl" notifications@github.com ha scritto:

ok, I have finished the first, buggy, version. Note that there might also be conceptual bugs.

You can see that in the translation from osequent to lmf-star, i dont expect any information in the node except:

  • for init, the optional index
  • for box, the list of diamond indices In addition, I dont have a state for osequents and just receive as argument the lmf-star-cert, which means that the state is the one included in this certificate (lmf-star and lmf-singlefoc).

When translating back from lmf-star to osequents, i lose all the information in the nodes, except optional index and index).

Anyway, you can checkout the branch and do the example..

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub <https://github.com/proofcert/checkers/issues/6#issuecomment-258506672 , or mute the thread https://github.com/notifications/unsubscribe-auth/ AQoBDzVoO9ocwJ42sdIaXdS87tDCN0aDks5q63SugaJpZM4KpvHR

.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258508637, or mute the thread https://github.com/notifications/unsubscribe-auth/AFj8VTV4LeHB3Tuj399_ EIyuyou17t7Jks5q63aGgaJpZM4KpvHR .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258509511, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBD1Oq_X68FC3Bart2hfwXOQKNeVMnks5q63dBgaJpZM4KpvHR .

shaolintl commented 7 years ago

Ok, I have rebased it. I could not see the example file in master though... Are you sure it is there?

emmevolpe commented 7 years ago

Is your branch lmf-os? I can found the correct lmf-star in the branch 'master' but not in 'lmf-os'.

shaolintl commented 7 years ago

right, i forgot to push. but i dont see that also on master.

On 4 November 2016 at 21:21, emmevolpe notifications@github.com wrote:

Is your branch lmf-os? I can found the correct lmf-star in the branch 'master' but not in 'lmf-os'.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258537630, or mute the thread https://github.com/notifications/unsubscribe-auth/AFj8VRlgaXNvVhl5Y9vKn7v5oDvEjWK4ks5q65PHgaJpZM4KpvHR .

emmevolpe commented 7 years ago

Strange...

Everything works for me on lmf-star and master (and I have just pulled on my laptop after pushing from the lab). But in lmf-os I still see the old versions...

On 11/04/2016 09:25 PM, shaolintl wrote:

right, i forgot to push. but i dont see that also on master.

On 4 November 2016 at 21:21, emmevolpe notifications@github.com wrote:

Is your branch lmf-os? I can found the correct lmf-star in the branch 'master' but not in 'lmf-os'.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258537630, or mute the thread

https://github.com/notifications/unsubscribe-auth/AFj8VRlgaXNvVhl5Y9vKn7v5oDvEjWK4ks5q65PHgaJpZM4KpvHR .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258538589, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBD7189gy-JrsQks747_9WO9HfnNW9ks5q65TTgaJpZM4KpvHR.

shaolintl commented 7 years ago

not so strange, I forgot to pull the master branch before, sorry. I am working on it now.

shaolintl commented 7 years ago

ok, i have pushed it now

shaolintl commented 7 years ago

sorry

shaolintl commented 7 years ago

wait, still problems. git got crazy..

shaolintl commented 7 years ago

ok, should work now, sorry again.

emmevolpe commented 7 years ago

No problem. Thanks!

On 11/04/2016 09:48 PM, shaolintl wrote:

ok, should work now, sorry again.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/6#issuecomment-258543540, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBD2ta8I7Ryf-VBQDtPV59ua0vWU0wks5q65oTgaJpZM4KpvHR.

emmevolpe commented 7 years ago

The example is working now. Please refer to these versions of the fpcs.

shaolintl commented 7 years ago

Thanks, merged to master and deleted