Oi Joao, Se for para engenheiros, vc pode se inspirar no EARS para a escrita de requisitos. É basicamente uma linguagem controlada que pode ser traduzida para LTL e usada para a verificação formal e síntese de sistemas.
Achei a seguinte referência, mas existem muitas outras. https://www.researchgate.net/publication/316972696_Just_Formal_Enough_Automated_Analysis_of_EARS_Requirements Essa metodologia tem sido usada com algum sucesso no desenvolvimento de sistemas críticos. My two cents, Vivek On Thu 16. Nov 2023 at 17:08, Adolfo Neto <[email protected]> wrote: > 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ê 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/CANspyYXmx6Uw8TYNb5ViL7ThEetsMrxHrRymfJ2jpJyMqG9iJA%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYXmx6Uw8TYNb5ViL7ThEetsMrxHrRymfJ2jpJyMqG9iJA%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/CAFx3SPKqj8fvjC_SQoM2ESJwfVk%2Bq2hABmjQYy_4Dn%2BwH8uZRQ%40mail.gmail.com.
