History of Eqthy

0.4

Language:

• Eqthy documents embedded in Markdown can now include other Eqthy documents that they build upon, by putting the phrase "Requires Filename" at the start of a line.

Implementation:

• Multiple documents may now be processed in a single run of eqthy, listing all documents as command line arg- uments, with context (axioms and proved theorems) from each document being available in all subsequent doc- uments.
• --input-format option replaces --bare flag.
• Added type annotations to Python implementation. In the process, replaced namedtuples with dataclasses, and refactored the class hierarchies in some places, so that e.g. Variable is now a subclass of Term.
• Small improvement to parser (an error is now reported if an axiom, or anything that is not a theorem, follows a theorem.)

Distribution:

• Added a completed proof of De Morgan's Laws for Boolean algebra, contributed by Proloy Mishra (@pro465).
• Added a few other documents, including some basic theorems in Interior Algebra, as well as refactoring some of the existing documents to use the "Requires" facility to build upon other documents.
• Arranged the licensing information in accordance with the REUSE 3.0 convention.

0.3

Implementation:

• A bug where two terms could unify even though they have different constructors was discovered and fixed by Proloy Mishra (@pro465), who also repaired the proof in boolean-algebra.eqthy.md that had passed checking only due to this bug.
• Slightly improved logging produced in --verbose mode.

Distribution:

• The axiom system used in propositional-algebra.eqthy.md was identified to be inconsistent, also by @pro465. The axiom was replaced with one that is most likely not inconsistent, and the proof was repaired.
• Added some larger aspirational items to the TODO section of the README.

0.2

Language:

• Added support for with clause in by hints, allowing variables in the axiom or previously-proved theorem to be renamed before applying it to the current step.

Implementation:

• When there is a derivation error, the name of the theorem, and the step number within that theorem, are now included in the error message.
• Refactored and cleaned up (flake8) the code in small ways.

Distribution:

• Simplified the proof in the Propositional Algebra document.
• Added example documents containing proofs in Boolean Algebra and Combinatory Logic.
• Added a few more proofs in group theory, involving inverses.
• Added example documents demonstrating with and demonstrating using a previously-proved theorem in a step.
• Added this HISTORY.md file.

0.1

Initial release.