LPC eBook and translation

[Dmitry Shlagoff]

Hi everyone.

First of all, Mark, thanks for LPC -- the brilliant book!

I have a 2nd edition LPC copy and I'm interested in having a eBook version (maybe PDF, FB2, ePub -- whatever).

Also, I want to translate the book to Russian -- what do you think about this prospect? I don't know much about the money side of things tho, as well copyright and publishing.

Another one idea is to have some webpage with LPC's provedit! (and extensions) available without the need to install shen on local computer since it raises the bar of entry considerably.

I will be pleased to hear what do you think about this matter!

[Mark Tarver]

Hi,

I think I got your message through the contact form on the Shen site?  I've been meaning to get back to you.

First thank you for the offer.  LPC is likely to have a third edition - perhaps next year.  I actually want to replace 

some material on resolution (which is partly covered in TBoS) with material on first-order model theory and 

Skolem's Paradox which is philosophically more interesting.   I'd like to update the software for 

the book too.

The new software may be part of a generic programable proof assistant for any sequent-based logic 

E-copy has been hampered by the weakness of DRM but this might be changing now.   E-copy of my work is likely to

happen next year if the tech checks out.

I think your suggestions are good, web page included and I'll return to them as soon as I've got the current tranche of 

work off my desk.   This might be January time, but I will come back to this.

Mark

[Bruno Deferrari]

> Another one idea is to have some webpage with LPC's provedit! (and extensions) available without the need to install shen on local computer since it raises the bar of entry considerably.

If LPC still works with the BSD versions of Shen (which it did, so I guess it still works) it should be quite straightforward to produce binaries for all platforms using the same CI system we currently use for Shen/SBCL and Shen/Scheme.

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/94b6bfa4-d170-49a6-87cd-9a0d1ac0dc4an%40googlegroups.com.

--

BD

[Bruno Deferrari]

I meant "if provedit! still ...."

--

BD

[Dmitry Shlagoff]

I think there is a problem with accessibility of this setup to people who wants just to play with things, not to commit to installation of some not-so-well-known binaries. I bought the book by an accident, for example, -- I know nothing about Shen etc but I do think LPC is a great book on the subject and my proposal is to separate LPC material from Shen intricacies for people who can be driven away by this. One way, in my opinion, is to provide webpage with all the required bits: provedit!, afst, resolution etc. It would make easier to control Shen version and concrete backend in order to ensure we have working setup for users.

пятница, 4 декабря 2020 г. в 22:03:29 UTC+7, Bruno Deferrari:

[Mark Tarver]

There's not much concrete I want to do in this period until I've got through

the ongoing work bringing SP 28 onto line.  That said,  I should be done by the

end of this month.   

LPC has its origins in a discrete maths course I taught at Stony Brook in 2003.

It was the last academic post I held or am likely to hold.  The course drew the wrath

of the old guard in the department who were going to arraign me in front of a committee.

I have somewhere a transcript of my resignation and statement of my position on teaching CS.

It is actually worth a read.

As regards LPC 2nd edition, it is less influenced by the requirements of Stony Brook CS dept.

than my original notes, but I'd planned a 3rd edition.  I wanted to cover model theory for 

first-order logic and then to discuss Skolem's Paradox and ontological reduction.  Other 

possible candidates for inclusion are Herbrand's theorem, Paradoxes of Strict Implication,

and possibly a soundness and completeness proof for the logic system in the book.  The system 

was specifically designed to encourage proof skills in students and is original to the book AFAIK.

This would be packaged with a new program described.

 "my proposal is to separate LPC material from Shen intricacies for people who can be driven away by 

 this. One way, in my opinion, is to provide webpage with all the required bits: provedit!, afst, 

 resolution etc. It would make easier to control Shen version  and concrete backend in order to ensure 

 we have working setup for users."

One thing that emerged from a poll of over 200 students at Stony Brook is that only 8 preferred using

paper to using a computer to do proofs.  Sequent proofs really require some computer support 

unlike Fitch or Lemmon's natural deduction systems which do lend themselves to paper.

The original program should still run but IMO it looks a bit clunky as my old code sometimes 

does to me.  There is a new program which is essentially a shell - it can be programmed to 

work with any logic presentable in sequent notation.   It is shorter, neater and more

generally usable than the old program.  I have begun to link this up to a graphical interface

so that proof assistants for any logic can be run off easily.  I stopped work on it because

of commitments elsewhere.   

It is true that the program has become somewhat detached from the text and people have to hunt it down.  

I expect that many people read the book w.o. even assaying a proof.  I don't think that one need know 

much Shen to do a proof - my students knew none.  Only if you want to write tactics do you have to

program.  LPC contains some gentle examples in a chapter.

The suggestions here are useful and the system certainly deserves its own space and when the current workload 

is done I'll revisit this question next month.

Mark

[Mark Tarver]

Hello;  as promised I did get back to this.  Rather later than planned since work took rather longer than expected.

As regards e-books,  I'm all for them, the problem is that DRM has been hitherto not worth a damn.  However there is a new technology 

coming up - Bookchain - based on the block chain which might change the game.   I've written to the MD of the company Scenarex who

markets this technology and I'm open to this system if it works.

Translating to Russian.  I guess you're in Russia?   The Russians had a key part in Shen because Russians funded the development of Shen

from 2010-2012.  I'm open to that.  We'd probably have to do an NDA and arrange for you to have some means of remuneration if possible.

I'm working on legal stuff wrt organising this last aspect into something less ad hoc than currently exists right now.

I think the idea of a dedicated web page is excellent.  Either a dedicated site or a page with links to the Shen home page.  I think probably the

latter for the moment.   SP does have the capacity in principle to allow users to upload their material to the Shen site.  So it would be possible

for you to have your own page maintained by yourself.    This capacity is not in SP 30 because there is a big website makeover on the way.

But it is likely to be in SP 31.

Being able to run Provedit! from the browser is an excellent idea.  Ramil Farkshatov actually created an online Shen under Javascript quite a

number of years ago.    It should be possible to run an online graphical version of this program.    I would myself like to replace TCL/tk in SP

by a BUI - browser user interface - which are currently becoming hot.

Provedit! is rather old and I'm working on a better version called the GPA (General Proof Assistant) which can be programmed for any sequent

based system - not just FOL.    This would go into a system called the Logic Lab which is an inventory of logic tools under a 'free for educational

and personal use' license.    This would include the code for the FTP which incorporates clause form conversion and tools for reasoning about

Shen programs.   I'd suggest that the website page for LPC point into the Logic Lab.

Mark

On Wednesday, 2 December 2020 at 17:16:18 UTC wess...@gmail.com wrote:

[Mark Tarver]

Oh, an addendum - there is an LPC 3rd edition - not completed, sitting on my machine.

Mark

[Mark Tarver]

Hello,

Finally this has come up to the top of my to do list; having got the other stuff out of the way.

I'll write to you on this issue.

Mark

On Wednesday, 2 December 2020 at 17:16:18 UTC wess...@gmail.com wrote: