search

OpenLogicProject / fitch-checker

JavaScript/PHP Fitch-style natural deduction proof editor and checker (NO LONGER MAINTAINED)
GNU General Public License v3.0
51 stars 5 forks source link

Allow zero-place predicates in FOL #12

Open rzach opened 5 years ago

rzach commented 5 years ago

When https://github.com/rzach/forallx-yyc/issues/15 is dealt with, forallx will allow zero-place predicate symbols. The proof checker should then do the same.

rzach commented 5 years ago

As of Fall 2019 edition of forallx-yyc, FOL syntax has atomic formulas surrounded by parentheses, and sentence letters are counted as FOL formulas. That means that the parser can distinguish between quantifiers (Ax) and formulas (A(x)). Change the code to correctly parse FOL formulas. This no longer requires choosing if the proof is in TFL or FOL.

frabjous commented 5 years ago

Looks like it's not just parentheses that are added, but also commas between the terms for polyadic predicates.

I'm not thrilled about this change if these parentheses and commas are to be treated as mandatory. I'm too lazy to write "R(x, y)" rather than "Rxy" every time; and if they're not mandatory, it doesn't solve the "∀x" problem. But I don't really consider that a very serious problem; maybe others do.

Ideally, however, the code would be modular enough to allow an instructor to choose their own precise syntactic rules. This would go along with also making the precise deduction rule set modifiable as well. Of course, that's a bigger project than just tweaking the current parse function.

I've been thinking for awhile of a much larger project which may involve a complete rewrite of all this stuff, also involving the ability for students to log in, save answers, get scores on exercises, etc., which would mean either making it all into a plugin for Moodle, or using the LTI standard for interoperability with an LMS, or something similar. Does anyone use an LMS other than Moodle? (Maybe this is not the place to have this discussion.)

rzach commented 5 years ago

True, yes. I wasn't suggesting you do this; more of a reminder to myself that this should be done if it's going to work with my version of forallx. And yes, we should make it so that it works the old way too: a switch for original forallx or forallx-yyc syntax.

In the long run, the carnap package (https://carnap.io/) is maybe the way to go for LMS integration & automated grading. (I use Brightspace/D2L)