The word processor that can check your math

Why is the version number less than 1.0? What features are missing and planned for future versions?

The current version of Lurch has most but not all of what we hope to have in Lurch version 1.0 some day.  The current version is fully functional for actually checking mathematics, and reasonably polished for certain applications like propositional logic, predicate logic, elementary set theory, etc.  But there are some major features that are currently missing that we hope to add in future versions.

  1. Mathematical typesetting. The current version cannot display math expressions that are anything other than a horizontal sequence of math symbols and characters.  In particular, it cannot render complicated expressions that contain fractions (like the LaTeX \frac{1}{2}), matrices, etc.  This is naturally a high priority to add in the future.
  2. Customizable parser. While the rules in the current version are completely customizable, the parser that is used to interpret math expressions typed in meaningful expression bubbles (see the Advanced Users Guide) is currently built-in and difficult to extend to new notation.  In the future the parser will be completely customizable by the Lurch author who can make the notation match his or her textbook, lecture notes, or any other notation they invent and would like to use.
  3. Expression types. The rule identifiers that appear in a Lurch rule definition can currently be instantiated with (almost) any expression when trying to determine if the expression being justified and its premises satisfy the rule.  In the future we hope to allow the rule author the ability to restrict rule identifiers so that they can only be instantiated with an expression of a certain type (like a statement, or a set, or a natural number, etc.).  The type of an expression will also be customizable and compatible with the customizable parser.
  4. Higher Level Rules. Currently the if-then and iff rule definitions make it possible to easily write custom rules that can check a single step of your work.  But there are times when the need to validate every step of your work may result in an overly pedantic or detailed proof that focusses on steps that might detract from the main ideas of your proof.  To assist with that we can implement higher level rules as additional rule definition types. Examples of such rules in the current version are the CAS rules which use a CAS to validate any step of work that involves showing two standard CAS math expressions are algebraically equivalent.  In the future we would like to add other such rules, such as a rule that avoids the need to do propositional logic steps individually by having a single rule that checks if the conclusion follow from the premises as a tautology.
  5. Improved AI.  Currently Lurch has a few shortcuts for reducing the burden on the user to bubble things in his proof.  For example, the meaningful expressions on a numbered list are automatically labeled by the line number so that the user doesn’t have to label those meaningful expressions in order to refer to them as premises.  It is also assumed that premises that are not cited are automatically cited to be the expressions of the appropriate type immediately preceding the expression being justified.  These shortcuts can be supplemented with additional rules, such as having Lurch find premises wherever they may occur in the document, or having it auto-bubble reasons and labels and premises whenever it can make a reasonable guess in order to save the user work.  Better control over how aggressive Lurch is at doing these things will allow the instructor to decide how much help is too much and how much is just enough.

These are just some of the main features we hope to have in future version.

Comments are currently closed.