Updated site structure for clarity of purpose and navigation.
Proof builder performance and resource usage both greatly improved.
Many incremental improvements in proof builder user interface.
Full user interface support for exponentiation. While ‘**’ is still
accepted, ‘^’ is the official symbol for it.
Interactive demos of forward and goal-directed proof.
Miscellaneous updates to content.
07/2024
The entire proof builder system is now converted from JavaScript to Typescript and compiles with minimal errors.
The axiom of induction now properly contains an internal quantifier.
The inference rule / command that sets up an induction proof now imports relevant assumptions into the scope of the quantifier.
In proofs that have a goal, steps with the goal’s conclusion highlight undesired assumptions in red to indicate that they need to be proved true.
There is now a formal “subgoal” rule. This allows induction proofs to stay the same as before except for use of an official subgoal in proving the inductive case.
Improvements to manual and automatic simplification.
Numerous improvements to presentation of rules in menus and proof displays.
05/2024
New “detach” inference rule. Selecting the conclusion of a step
searches for facts with assumptions it matches. The rule
substitutes into the fact, then removes it as true.
