On the Shen Reasoning System

[Antti Ylikoski]

I understand that there is there the idea or the plan to build a

system corresponding to the MRS, or a MRS like but better system, with

Shen.

I would love to learn more about these plans.

One possibility would be to simply convert the CL MRS to Shen.

Converting CL code to Shen of course would be very straightforward.

Another option would be to design and implement a Shen reasoning

system based on the construction of the MRS, but a novel and hopefully

a better system, optimally with some novel innovations.  I understand

that this one is the way to go, that has been planned.  I shall get

the LPC book by Dr Tarver and delve into it when I shall have time for

that.  It may be necessary to get the Book of Shen as well.

It also is relevant as to these plans that I currently am searching

for a new employment, which will influence the amount of time and work

I can dedicate to the CL MRS project.  My alma mater was the Aalto

University, http://www.aalto.fi, which is considered a very bad

employer by many individuals.

regards, Antti Y

Helsinki, Finland

[Mark Tarver]

The Shen reasoning system (whose components are on my computer) was designed to enable programmers to do formal proofs about programs and Shen programs in particular.  Rather different from MRS.

Mark

[Mark Tarver]

You should be able to improve on the MRS using types; you can implement an LCF-style system - or a program synthesis tool a la Martin Lof.

Mark

[Mark Tarver]

look at the program on http://www.shenlanguage.org/LPC/lpc.html

[Antti Ylikoski]

OK; yes I see; I was a little bit careless in the use of language; the words "the Shen reasoning system" refer to your program proof system; I intended to express there, "the Shen version of the MRS system".

The last time I learned about program verification and proving programs, I was said to that the full scale program verification is an undecidable problem.  It is EXTREMELY interesting if you have some good results as to creating proofs for programs.  Could you tell here a little about those results?

regards, Antti Y

Helsinki, Finland

[Mark Tarver]

What I have will instantaneously translate any purely functional Shen program into a set of (conditional) equations in polymorphically typed second-order logic.   But to make that into a program verification system you need an IDE and a library of tactics and for that you need time and £.

Mark

--
You received this message because you are subscribed to a topic in the Google Groups "Shen" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/qilang/_72x6Yywsl8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to qilang+un...@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at http://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[Mark Tarver]

The thing is that automated reasoning systems have many applications - from data handling to expert systems to program verification to hardware verification to solving challenge problems.  You have to be clear about what domain you want to enter.

And the systems are seriously big.  the BMTP was about 100K lines of Lisp.    You can divide that by 3 for Shen but that's still big.   To embark on that you need to capitalise the effort.

Mark

To unsubscribe from this group and all its topics, send an email to qilang+unsubscribe@googlegroups.com.

[Antti Ylikoski]

OK, thanks Mark for a short but really good point on the usefulness of

automated reasoning systems.

Right now I feel there are there two courses of action that could be

taken:

a) I could finish converting and building the CL MRS, and then comment

and document and e-mail it for the Shen group, in order for them to be

able to build a corresponding capability in the Shen language; or

b) I could start specifying a Shen MRS system here in this group, plus

of course with all the other existing telework forms, personal

messages and such, and then I could operate as a MRS consultant for

the Shen MRS group.

How do you think Mark, what would be the most intelligent :)) thing to

do about this work?

regards, Antti Y

Helsinki, Finland

To unsubscribe from this group and all its topics, send an email to qilang+un...@googlegroups.com.

[Mark Tarver]

What I tell most people who approach me; you should follow your heart.  I think probably most members of the Shen will support you if you want to specify the MRS in Shen, so b) is probably better.   You might give a thought as to what you want your system to do - do you have a practical application or is it for interest?   Either way if you want to do it in Shen you have to begin with the type theory and the data structures of the system.  You need to define the MRS as a math'l structure.   

Mark