search

metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

Tweak Gource captions about books and articles #1625

Open david-a-wheeler opened 4 years ago

david-a-wheeler commented 4 years ago

@benjub recommended tweaking the Gource captions about books and articles in https://github.com/metamath/set.mm/pull/1620#issuecomment-621776957 , but that issue is already closed, so here is a new issue to track that.

@benjub :

@david-a-wheeler and @nmegill : If articles are mentioned, then I think @digama0 's article "Models for Metamath" is (very) important, as well as @nmegill's foundational article. I think it would be more readable to mention books and articles in a unified way. For the concerned lines, this would give:

1995-xx-xx|Article: Norman Megill, A Finitely Axiomatized Formalization of Predicate Calculus with Equality
2008-07-25|Book: Norman Megill, Metamath, A Computer Language for ....... [original title]
2016-01-28|Article: Mario Carneiro, Models for Metamath
2016-08-08|Article: Daniel Whalen, Holophrasm: a Neural Automated Theorem Prover for Higher-Order Logic
2019-06-02|Book: Norman Megill and David A. Wheeler, Metamath: A Computer Language for Mathematical Proofs
2019-10-22|Article: Mario Carneiro, Metamath Zero: The Cartesian Theorem Prover
david-a-wheeler commented 4 years ago

The publication of "A Finitely Axiomatized Formalization of Predicate Calculus with Equality" only lists "Summer 1995" as its publication date, and I have to use a specific day. So I'll use the revision date, that's when it was completed so it's a defensible date.

That leads to this entry:

1995-07-14|Article: Norman Megill, "A Finitely Axiomatized Formalization of Predicate Calculus with Equality"
benjub commented 4 years ago

@david-a-wheeler You think that 1995-07-14 is a "defensible" date ?? Don't forget that things tend to get stormed on Bastille day !