Tagging - 2015-10-11

« first day (1216 days earlier) ← previous day next day → last day (3117 days later) »

4:24 AM

So, we have theorem-provers and automated-theorem-proving... These looks the same to me in practice, so I think they should be synonyms.

Perhaps "automated-" should be the main tag, since its meaning is more obvious.

2 hours later…

Martin Sleziak

6:16 AM

@MiceElf There is also a third related tag, computer-assisted-proofs. as I learned here:

Q: Tags for automated theorem provers

I posted this in Tag merging and synonyms, but it's attracted no votes and no comments, so I figure maybe nobody's watching over there. http://math.stackexchange.com/tags/theorem-provers/info links to automated-theorem-proving, which has no summary or tag wiki and appears indistinguishable. The...

@MiceElf I disagree with this. Not every proof assistant is automated theorem prover, it might be simply "proof checker".

I agree that they can be in the same tag. But if we want to create synonym, the more general term should be master.

So i I had I had to choose from the existing tags, I would prefer theorem-provers or computer-assisted-proofs as the master tag.

In the thread I linked, dfeuer suggest a completely new tag automated-proof-systems as master.

I will add two Wikipedia links who - I hope - show that they are not the same thing:

Automated theorem proving

Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science. == Logical foundations == While the roots of formalised logic go back to Aristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalised mathematics. Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern...

Proof assistant

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer. == Comparison of systems == ACL2 – a programming language, a first-order logical theory, and a theorem prover (with both interactive and automatic modes) in the Boyer–Moore tradition. Coq – Which allows...

2 hours later…

Martin Sleziak

8:21 AM

The tag hahnbanach was created.

Q: Every $G \in BL(Y,K^n)$ has an extension $F \in BL(X,K^n)$

Let $X$ be a normed space and let $Y$ be a subspace of $X$. Then every every $G \in BL(Y,K^n)$ has an extension $F \in BL(X,K^n)$. If in particular, the norm on $K^n$ is the norm $||\cdot||_{\infty}$, then every $G \in BL(Y,K^n)$ has a norm preserving extension $F \in BL(X,K^n)$. Also every $G...

functional-analysis hahnbanach

I feel a bit mixed about tag concerning Hahn-Banach theorem. It is an important theorem, maybe such that might be useful.

But if we want to create such tag, it should at least be spelled correctly. E.g., the tag name would be hahn-banach-theorem. (I did not count, but it seems to be in 25 characters limit for the tag names.)

Anything else needing attention among new tags: math.stackexchange.com/tags?tab=new ?

I see also chain-rule there.

Q: Partial derivative of composition with multivariable function.

I think this should be an easy question? However, a quick google search has not revealed the confirmation I want, so I am posting here. If we have a function $f(x,y)$ and a monotonic transformation $g$. Let us now consider a monotonic transformation of $f$ using $g$: that is, let $v(x,y) = g(f(x...

multivariable-calculus derivatives partial-derivative chain-rule

As I read here, this tag has been created and removed in the past.

I am not sure whether there was some discussion on meta in chat whether this tag might be actually useful. My guess is that it is going to be removed again.

12 hours ago, by Martin Sleziak

Although I don't think that this is the best place to let other users know about a new tag - since this definitely do not answer that question.

I did not vote on your post, but if I had to guess why it has (at the moment) one downvote, the reason is probably that this does not answer the question. This is an announcement about creating new tag, which is completely unrelated to the feature request the OP is asking about. — Martin Sleziak 3 mins ago

One possible place to get feedback on new tag might be tagging chatroom. Although not many users visit this room. There is also tag management thread. Some proposals for new tags were posted there before tag creation. And that thread is also the place where I would expect to see reaction of other users, if somebody thought that some discussion about some newly created tag (like this one) is needed. — Martin Sleziak 1 min ago

BTW I really appreciate that you created also the tag-wiki. Many users who create new tags leave the tag-info empty. — Martin Sleziak 13 secs ago

12 hours later…

Martin Sleziak

8:48 PM

Martin, saw your comments at my "new/rare tags" answer, thanks. I simply deleted it. The first time I made a tag, complex-multiplication as in the David Cox book Primes of the form $x^2 + n y^2:$ Fermat, Class Field Theory, and Complex Multiplication, Willie Wong asked me what should go in the tag information; later he said he was mostly worried people would use it for instructions about how to multiply complex numbers. Anyway, i did figure out that I was supposed to put in some information for any tag I made; there have not been many. — Will Jagy 1 hour ago

« first day (1216 days earlier) ← previous day next day → last day (3117 days later) »

all rooms