[Logica-l] Re: Seminário 5/11/2020 - Kevin Buzzard (16h)

2020-11-02 Por tôpico Alexandre Rademaker 

Peço desculpas pela sequencia de emails, mas me chamaram atenção para o fato de 
que no meu primeiro anúncio, eu tinha dito 14h quando na realidade o seminário 
será  5 de Nov de 2020 as 04:00 PM (16H), conforme consta na página de 
inscrição.

At.,
Alexandre


> On 2 Nov 2020, at 22:44, Alexandre Rademaker  wrote:
> 
> 
> Para informação! Segue convite de palestra nesta quinta-feira as 16h.
> 
> https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX
>  
> 
> 
> Ab.,
> Alexandre
> 
>> Subject: Seminário 5/11/2020 - Kevin Buzzard
>> Date: 2 November 2020 11:24:45 GMT-3
>> Cc: Alexandre Rademaker mailto:aradema...@gmail.com>>
>> 
>> Titulo: Teaching mathematics to computers.
>> 
>> Palestrante: Kevin Buzzard
>> 
>> Resumo: 
>> Computers have changed the way that mathematics is done. The ability to do 
>> complicated calculations quickly has enabled humans to numerically solve 
>> differential equations, to check conjectures in number theory in billions of 
>> cases, and many many other examples. In applied mathematics in particular, 
>> the computer has revolutionised the subject.
>> But there are some areas of pure mathematics where computers are essentially 
>> completely unused. People studying theoretical questions about 
>> infinite-dimensional objects might find that traditional uses of computers 
>> are of no help to them -- they are trying to prove theorems, not compute 
>> examples.
>> Computer proof verification software offers a new way of using computers, 
>> which might be more useful to mathematicians looking for proofs. I will 
>> demonstrate some of this software (the Lean theorem prover, being developed 
>> by Microsoft Research), talk about why most mathematicians don't use it, and 
>> speculate about whether this will change in the future. No advanced pure 
>> mathematics background will be necessary.
>> 
>> Mini CV: 
>> Kevin Buzzard is a professor of pure mathematics at Imperial College London. 
>> He was a PhD student of Richard Taylor and his traditional mathematical work 
>> is in algebraic number theory. More recently he has become interested in 
>> teaching modern mathematical proofs to computers.
>> 
>> Convite:
>> 
>> Inscreva-se antecipadamente para esta reunião:
>> https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX
>>  
>> 
>> 
>> Após a inscrição, você receberá um e-mail de confirmação contendo 
>> informações sobre como entrar na reunião.
> 

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/488F36B6-CB2B-4CCD-9851-09EB17DF6435%40gmail.com.

[Logica-l] Fwd: Seminário 5/11/2020 - Kevin Buzzard

2020-11-02 Por tôpico Alexandre Rademaker 

Para informação! Segue convite de palestra nesta quinta-feira as 16h.

https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX
 


Ab.,
Alexandre

> Subject: Seminário 5/11/2020 - Kevin Buzzard
> Date: 2 November 2020 11:24:45 GMT-3
> Cc: Alexandre Rademaker 
> 
> Titulo: Teaching mathematics to computers.
> 
> Palestrante: Kevin Buzzard
> 
> Resumo: 
> Computers have changed the way that mathematics is done. The ability to do 
> complicated calculations quickly has enabled humans to numerically solve 
> differential equations, to check conjectures in number theory in billions of 
> cases, and many many other examples. In applied mathematics in particular, 
> the computer has revolutionised the subject.
> But there are some areas of pure mathematics where computers are essentially 
> completely unused. People studying theoretical questions about 
> infinite-dimensional objects might find that traditional uses of computers 
> are of no help to them -- they are trying to prove theorems, not compute 
> examples.
> Computer proof verification software offers a new way of using computers, 
> which might be more useful to mathematicians looking for proofs. I will 
> demonstrate some of this software (the Lean theorem prover, being developed 
> by Microsoft Research), talk about why most mathematicians don't use it, and 
> speculate about whether this will change in the future. No advanced pure 
> mathematics background will be necessary.
> 
> Mini CV: 
> Kevin Buzzard is a professor of pure mathematics at Imperial College London. 
> He was a PhD student of Richard Taylor and his traditional mathematical work 
> is in algebraic number theory. More recently he has become interested in 
> teaching modern mathematical proofs to computers.
> 
> Convite:
> 
> Inscreva-se antecipadamente para esta reunião:
> https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX
>  
> 
> 
> Após a inscrição, você receberá um e-mail de confirmação contendo informações 
> sobre como entrar na reunião.

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/9385933B-A868-4C20-8E17-DCB978420CF1%40gmail.com.

[Logica-l] Seminário remoto "Lógicos em Quarentena" 05/11/2020 (quinta-feira) 16:00h

2020-11-02 Por tôpico Bruno Lopes 
Numa iniciativa conjunta da Sociedade Brasileira de Lógica e do Grupo
de Interesse em Lógica da Sociedade Brasileira de Computação, gostaríamos
de convidar a todos a participarem do Seminário "Lógicos em Quarentena".
Trata-se de um seminário remoto com apresentações informais por membros da
comunidade e espaço para perguntas no fim. As apresentações usualmente são
gravadas e disponibilizadas na página do evento http://lq.sbl.org.br (com a
agenda completa).

Data: 05 de novembro de 2020 (quinta-feira)
Horário: 16:00h GMT-3
Apresentador: Carlos Olarte (ECT/UFRN)
Título: The L-Framework*: Structural Proof Theory in Rewriting Logic
Resumo: Structural properties such as admissibility and invertibility of
rules are crucial in proof theory, and they can be used for establishing
other key properties such as cut-elimination and completeness of focusing
in sequent systems.  Finding proofs for these properties requires inductive
reasoning over the provability relation, which is often quite elaborated,
exponentially exhaustive, and error prone. We propose automatic procedures
for proving structural properties of sequent systems. Our techniques are
based on the rewriting logic metalogical framework, and use rewrite- and
narrowing-based reasoning. They have been fully mechanized in Maude and the
resulting framework is generic  and modular since cut-freeness,
admissibility, and invertibility can be proved incrementally. The
L-Framework achieves a great degree of automation when used on several
sequent systems. Case studies include  intuitionistic, classical,
substructural and modal logics.
* https://carlosolarte.github.io/L-framework/


A apresentação ocorrerá pelo Google Meet através do link público
https://meet.google.com/pkq-fxvz-iou .


-- 
Bruno Lopes
Professor Adjunto
Instituto de Computação
Universidade Federal Fluminense
http://www.ic.uff.br/~bruno

-- 
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 ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAD-Wq0-W%3DdVze43B_YymsBZp6v6WFo7i0vg6W1U%3D%2B2KuR4i6uQ%40mail.gmail.com.