git @ Cat's Eye Technologies Eqthy / master HISTORY.md
master

Tree @master (Download .tar.gz)

HISTORY.md @master — view rendered · raw · history · blame 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
<!--
Copyright (c) 2022-2024 Chris Pressey, Cat's Eye Technologies
This file is distributed under a 2-clause BSD license.  See LICENSES directory:
SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Eqthy
-->

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](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.