search

gleachkr / Carnap-Old

An interactive proof checker that runs in the browser
http://gleachkr.github.io/Carnap/
GNU General Public License v3.0
3 stars 0 forks source link

Predicate Logic #36

Closed davidfaraci closed 8 years ago

davidfaraci commented 9 years ago

System reads 'x_1' as '*_1': image By the way, is there a reason the parser needs to interpret x as x_1 as it did here? It might be nice for ease of reading/writing to allow just simple variables.

Also, would it be possible to have the system interpret predicates without parentheses--i.e., read Fa as F(a)?

JakeEhrlich commented 9 years ago

So we actually took the first step in doing this here: https://github.com/gleachkr/Carnap/issues/24 Should be an easy fix. How it interpreted x_1 is a bug for sure. I'll see if I can look at this later this week.

gleachkr commented 9 years ago

Yep. I think you can use "x,y,z" now, when you're writing a proof. When carnap is just picking its own variables, it uses "x_1,x_2...". It'd be good to change the interface for this webapp so that it respects the user's choice of variables, rather than regenerating the formula according to carnap's recipe.

It also looks like unbound variables just show up as "*_1", which they should not do.

I'll see if I can take care of these issues this afternoon.

gleachkr commented 9 years ago

Ok, I've fixed the generation of premises. It should now retain the variables that you chose when you wrote out the problem. There's also a side-effect here of improving error messages, I think (they'll now use the user-generated bound variables too). The free variable issue might need some more thought. I'm a little torn, since it seems kind of nice to have a visual flag that a variable hasn't been bound. But maybe some other flag would be better?

gleachkr commented 9 years ago

About the question of reading Fa as F(a)---This would be possible, but the most straightforward way of doing it would prevent you from using arbitrary strings as predicates and constants, since Fat(Albert) would end up being confused with F(a).

Things are set up right now so that in principle you can swap different formula-parsers for a single language, so maybe the thing to do would be to have a strict parser that insists on one-character predicates and relations, and a liberal parser that doesn't, but that requires parentheses? Once I get a "settings" box working, you could just pick the formula-parser you want for the problem at hand, or configure a problem sheet to use whatever parser you've brought your students up on. Would that work?

davidfaraci commented 9 years ago

That sounds perfect to me. With a system this flexible, why not make it even more so!

On Fri, Sep 11, 2015 at 3:35 PM, gleachkr notifications@github.com wrote:

About the question of reading Fa as F(a)---This would be possible, but the most straightforward way of doing it would prevent you from using arbitrary strings as predicates and constants, since Fat(Albert) would end up being confused with F(a).

Things are set up right now so that in principle swap different formula-parsers for a single language, so maybe the thing to do would be to have a strict parser that insists on one-character predicates and relations, and a liberal parser that doesn't, but that requires parentheses? Once I get a "settings" box working, you could just pick the formula-parser you want for the problem at hand, or configure a problem sheet to use whatever parser you've brought your students up on. Would that work?

— Reply to this email directly or view it on GitHub https://github.com/gleachkr/Carnap/issues/36#issuecomment-139643450.

gleachkr commented 9 years ago

OK, commit 19ed42670f0614d31951b688672308bc096fad10 lets you configure the syntax of a proof box. Example number 4 on the front page shows how it works---in strict mode, every symbol is a single character (usually a letter---constants can also be digits), and parentheses are required only when necessary to resolve ambiguity (I'm open to suggestions about how to make this even more compact---We could, for example, break up the character sets for the different symbol types, which I think would let us do without parentheses entirely, at least in the atomic formulas---it'd basically be polish notation).

So far, it's set up for FOLBox, the (now rather badly named) piece of javascript that turns chunks of a given piece of html into interactive proofs. You configure the parser by adding classes to the html chunks that are going to become proofs.

I think it'd also make sense to have a menu (e.g. in the ShowThis app) that lets you select configuration options, and pin those down when you make a problem sheet url, so I'll leave this issue open until we've got something like that.

gleachkr commented 8 years ago

Ok, the projected feature has now been added to ShowThis, so I'll go ahead and close.