Eduardo, Na verdade estou aprendendo Lean ainda. Meu objetivo é ver Lean como uma ferramenta para a escrita de programas mesmo. Por isso não vi nada ainda nesta direção.
João, Eu uso o texto A Estrutura de um Argumento com meus alunos. Não é nada muito avançado. O link está no Guia de Estudos da Prova 1 na página http://logicaparacomputacao.github.io On Thu, 16 Nov, 2023, 12:07 pm Eduardo Ochs, <[email protected]> wrote: > 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 <[email protected]> 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 <[email protected]> >> --- >> 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 [email protected]. >> 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 <[email protected]> > --- > Você recebeu essa mensagem porque está inscrito 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 [email protected]. > Para acessar essa 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 > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6jUsgTQcThMJ%2BF9uf77o-2TpnaDX-%3Dor%3DHOoo4LvtFd4g%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- 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 [email protected]. Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYXmx6Uw8TYNb5ViL7ThEetsMrxHrRymfJ2jpJyMqG9iJA%40mail.gmail.com.
