[Logica-l] An experiment concerning mathematical writing

[Joao Marcos]

Sobre clareza e estilo na escrita matemática
http://gowers.wordpress.com/2013/03/25/an-experiment-concerning-mathematical-writing/
um experimento de Tim Gowers.

Vale a pena participar!
JM

[Joao Marcos]

Dando continuidado ao interessante experimento...
http://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/

JM

--
http://sequiturquodlibet.googlepages.com/

[Joao Marcos]

Acabou de ser publicado (em open access) o paper com o "experimento
sobre escrita matemática", de Tim Gowers, que mencionei aqui na lista
em 2013:

A Fully Automatic Theorem Prover with Human-Style Output
Journal of Automated Reasoning
February 2017, Volume 58, Issue 2, pp 253–291


JM

--
http://sequiturquodlibet.googlepages.com/

[Walter Alexandre Carnielli]

A informação esta incompleta. O primeiro autor eh  M. Ganesalingam.

Ganesalingam, M., & Gowers, W. T.

Journal of Automated Reasoning

February 2017, Volume 58, Issue 2, pp 253–291

A Fully Automatic Theorem Prover with Human-Style Output

doi.org/10.1007/s10817-016-9377-1

O artigo esta disponivel aqui:

http://link.springer.com/article/10.1007%2Fs10817-016-9377-1

e um pre-print (bastante diferente do final) no Arxiv aqui:

https://arxiv.org/pdf/1309.4501v1.pdf

Interessantemente, na versão do Arxiv eles se referem bastante ao "influential" artigo  de Alan Bundy,  

Bundy, A. A Science of Reasoning, in `Computational Logic: Essays in Honor of Alan Robinson', eds Lassez J-L & Plotkin, G., MIT Press, pp 178-198, 1991.

mas nao o mencionam nas referências! Na versão final, o "influential" artigo desaparece.

O programa tem 3000 linhas em Haskell, segundo os autores;  me parece ate surpreendentemente pequeno pelo conteudo de "inteligência" que contem:

https://github.com/mg262/research/raw/master/robotone.zip

Eu nao tenho competência para mexer com isso, mas seria muito interessante se alguém pudesse programa-lo para demonstrar teoremas de Geometria Analitica. Com certeza,  dah para mostrar   tudo o que tem nos livros-texto usuais.Eu ajudaria...

Walter

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgjKvBM3nUKmh90b3_wL2TaE99pmqXKrNG9raAwkr81HQ%40mail.gmail.com.

[Joao Marcos]

Obrigado por complementar as informações do meu email anterior, Walter.

> Interessantemente, na versão do Arxiv eles se referem bastante ao
> "influential" artigo de Alan Bundy,
>
> Bundy, A. A Science of Reasoning, in `Computational Logic: Essays in Honor
> of Alan Robinson', eds Lassez J-L & Plotkin, G., MIT Press, pp 178-198,
> 1991.

A propósito, o "extended abstract" do Alan Bundy pode ser encontrado a
partir da página dele:
http://www.research.ed.ac.uk/portal/files/412469/A_Science_of_Reasoning.pdf
Segundo o Google Scholar, o artigo conta atualmente 175 citações.

O artiguinho termina com uma "Personal Note" interessante:

"For many years I have regarded myself as a researcher in automatic
theorem proving. However, by analysing the methodology I have pursued
in practice, I now realise that my real motivation is the building of
a science of reasoning in the form outlined above. Now that I have
identified, explicitly, the science I have been implicitly engaged in
for the last fifteen years, I intend to pursue it with renewed vigour.
I invite you to join me."


JM