Oi João, acho que 1) o que você está procurando tem muito a ver com o livro do Ganesalingam, que é de 2013, 2) o pessoal do Lean tem trabalhado muito pra implementar sintaxes que pareçam com certos modos de organizar definições e provas em linguagem natural, 3) quem entende mesmo de Lean aqui é o Adolfo Neto, eu só consegui fazer coisas muito básicas nele... será que a gente consegue que o Adolfo nos ajude com pitacos e links? Adolfo, plz?
Meus links: Mohan Ganesalingam: "The Language of Mathematics" https://www.springer.com/gp/book/9783642370113 Alguns blog posts sobre o livro do Ganesalingam: https://gowers.wordpress.com/2013/03/25/an-experiment-concerning-mathematical-writing/ https://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/ https://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/ Lean - um formato pra provas com justificativas: https://lean-lang.org/theorem_proving_in_lean/theorem_proving_in_lean.pdf#page=48 Alguns slides sobre "elaboration": http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=20 [[]], Eduardo On Thu, 16 Nov 2023 at 10:29, Joao Marcos <botoc...@gmail.com> wrote: > PessoALL: > > Por razões pedagógicas, estive buscando por exercícios de _tradução_ > entre "a" linguagem natural (qualquer uma que eu seja capaz de ler) e > linguagens formais de teorias lógicas apropriadas. Também estive > buscando exercícios na direção oposta, isto é, envolvendo _leituras > naturais_ de asserções descritas em linguagens formais. Ambas > categorias de exercícios parecem ser extremamente importantes para os > estudantes curiosos em saber *pra quê serve tudo isso*. > > Agradeço desde já por quaisquer sugestões que vocês puderem > compartilhar comigo de material (de qualquer nível) para a prática > destas tarefas. Tenho interesse particular por materiais que *não* > tratem de teorias matemáticas, mas que, ao invés, envolvam a > formalização de outros fragmentos interessantes da linguagem natural. > Materiais envolvendo _erros_ de tradução, numa direção ou na outra, > são particularmente bem-vindos! > > Caso seja de interesse dos colegas, posso ao final compilar aqui as > referências recebidas, na lista ou fora dela. > > Saudações lógico-naturais, > Joao Marcos > > -- > http://sequiturquodlibet.googlepages.com/ > > -- > LOGICA-L > Lista acadêmica brasileira dos profissionais e estudantes da área de > Lógica <logica-l@dimap.ufrn.br> > --- > 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+unsubscr...@dimap.ufrn.br. > Para acessar esta discussão na web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgSXODHR0OMA6c-VUELwn3MrhOggxB8LgCoOwrCqJb-og%40mail.gmail.com > . > -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logica-l@dimap.ufrn.br> --- 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+unsubscr...@dimap.ufrn.br. Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6jUsgTQcThMJ%2BF9uf77o-2TpnaDX-%3Dor%3DHOoo4LvtFd4g%40mail.gmail.com.
