search

daviddoret / punctilious

A human-friendly and developer-friendly math proof assistant
https://github.com/daviddoret/punctilious
MIT License
2 stars 0 forks source link

Dev #244

Closed daviddoret closed 1 year ago

daviddoret commented 1 year ago

version 1.0.10:

feature #242: constant-declaration

issue #238: alpha-equivalence

issue #226: develop minimal logic (M0).

lock mechanism for axiom-inclusion and axiom-interpretation.

issue #229: elaborate intuitionistic logic (j0) theory.

issue #231: compose the theory declaration and list the extended theories.

issue #232: provide the capability to forbid the inclusion of new inference-rules in a theory.

issue #233: provide the capability to forbid the inclusion of new axioms / definitions in a theory.

rename theory-elaboration-sequence to theory-derivation which is more accurate.

rename Formula to CompoundFormula.

bug #237: formula equivalence does not account for the presence of free variables in both formula, not necessarily at the same positions.

design flaw correction: UniverseOfDiscourse inherits from TheoreticalObject, and not from SymbolicObject