12

ALEKS (http://www.aleks.com/) is a good way of learning procedural math, because it is very systematic and forces you to master the dependencies of a kind of problem before working on that kind of problem itself. Also the interface is very clean and user-friendly.

The method of ALEKS seems especially well-suited to introductory logic (truth tables, symbolizing English sentences, truth trees, proofs in SL or PL, etc.), but ALEKS doesn't have a logic program. Has anyone else made something like this?

(Note: I asked this question on math.SE and nobody has answered it for a long time so I'm asking it here. Here is the link to the post on math.SE: https://math.stackexchange.com/questions/722363/is-there-a-program-like-aleks-for-mathematical-logic)

Community
  • 1
Joshua Meyers
  • 231
  • 1
  • 5

3 Answers3

5

The most relevant piece of software of which I'm aware is called Proof Designer.

Proof Designer is a Java applet that writes outlines of proofs in elementary set theory, under the guidance of the user. It is designed to help students learn to write proofs.

It was created by Dan Velleman, who (as you can see on his site) was the AMM editor 2007-2011.

The first page linked to above includes a list of 64 suggested problems. (Direct link.)

(He has, at least in the past, used it as a part of his course on Mathematical Logic at Amherst College.)

Benjamin Dickman
  • 18,470
  • 2
  • 41
  • 114
  • 1
    Interesting -- it looks like sort of a stripped-down version of a proof assistant? So perhaps also relevant to http://matheducators.stackexchange.com/questions/224/teaching-logic-with-a-proof-assistant – Mike Shulman Apr 02 '14 at 21:14
  • @MikeShulman I don't want to duplicate my answers, so I will post it as a comment there! – Benjamin Dickman Apr 02 '14 at 21:22
2

If you are looking for a system to perform interactive proof exercise in logic, building natural deduction trees for example, I can cite: coqweb, Lurch and edukera.com. They are interactive proof systems which can check some student proofs. In Lurch, the student type his proof and annotate it to explain to the system where are the facts and justifications. In Edukera, you have a point and click user interface, the student can chose which theorem or logical rule to apply and the system update the current state of the textual proof and even a graphical proof tree in the upcoming version.

Julien Narboux
  • 181
  • 6
1

Logic 2010 (http://logiclx.humnet.ucla.edu/) seems to be what I am looking for, though I am not sure because I have not seen it in use. I am going to a school where it is used next year, so I will ask my classmates to see it and then I can give more details.

Joshua Meyers
  • 231
  • 1
  • 5