Professor da Freie Universität Berlin realizou palestras em evento que marcou transição para a Escola Politécnica
Foto: arquivo pessoal
A atividade de encerramento das comemorações pelos 40 anos da Faculdade de Informática contou com a presença de Christoph Benzmüller, da Freie Universität Berlin e da Saarland University, Saarbrücken, ambas na Alemanha. O evento também marcou a transição para a Escola Politécnica da PUCRS.
Durante as palestras What has the Mechanisation of Category Theory in Common with Proving God’s Existence? e Automated Reasoning in Higher-order and Non-classical Logics, Benzmüller abordou temas como fundamentos computacionais teóricos e ferramentas computacionais de auxílio para a construção de sistemas dedutivos; o potencial interdisciplinar da Computação além do uso de aparatos computacionais; e diversas variantes do argumento ontológico de Gödel para a existência de Deus que foram analisadas com ferramentas automatizadas em computador.
Atualmente, Benzmüller é visitante na University of Luxembourg. Suas pesquisas anteriores incluíram instituições como Stanford University (EUA), University of Cambridge, University of Birmingham e University of Edinburgh (Inglaterra). Benzmüller concedeu uma entrevista na qual falou sobre lógica universal, abordagem metalógica e automação de raciocínio, entre outros temas.
Entrevista
Qual a Importância da Lógica (Matemática) para a Ciência da Computação, Inteligência Artificial, Filosofia e outras áreas?
Nessas áreas, um interesse especial foi atribuído à Lógica em, pelo menos, dois aspectos: (a) como uma ferramenta fundamental que permite um rigoroso modelamento e análise de teorias, sistemas, processos, argumentos, etc., e (b) como um objeto de estudo e desenvolvimento contínuo em si mesmo. A palavra lógica, de fato, designa muitos formalismos lógicos existentes no dia de hoje e que foram desenvolvidos nessas áreas para dar apoio a algumas aplicações práticas.
Como a Lógica pode ser aplicada em áreas como a Filosofia?
Muitos formalismos lógicos se originaram e se inspiraram na filosofia teórica e na metafísica. Cientistas da computação, em particular, às vezes se esquecem disso. Nos meus trabalhos atuais, estou aplicando os provadores de teoremas, ou seja, sistemas computacionais utilizados para a automação do raciocínio lógico, com vistas a uma análise crítica e rigorosa dos argumentos proeminentes na filosofia como, por exemplo, o argumento ontológico para a existência de Deus. Em nossos experimentos, os provadores de teoremas deram inclusive contribuições inovadoras e detectaram defeitos em argumentos humanos.
Em quais outras áreas a Lógica está presente no dia a dia e muitas vezes não é percebida pelo público leigo?
A lógica está no centro de uma argumentação racional e uma argumentação racional é fundamental para os nossos processos científicos e enquanto sociedade em geral. Logo, a Lógica é importante e vai muito além da filosofia, ciência da computação e inteligência artificial. Infelizmente, tem se observado um declínio da racionalidade nos últimos tempos, por exemplo, em debates políticos ao redor do mundo. Isso é muito ruim e deveríamos unir nossos esforços para reverter essa tendência novamente.
No que consiste o método utilizado para comprovar o argumento ontológico de Gödel? Em que áreas pode ser aplicado? Poderia exemplificar?
A análise do argumento de Gödel em um computador requer uma implementação prévia das variantes de formalismos lógicos expressivos, denominadas lógicas modais de primeira ordem. Essas lógicas dão embasamento a um manejo adequado das noções de necessidade e possibilidade, que são importantes neste contexto. Geralmente, as variantes das lógicas modais de primeira ordem são importantes para as formalizações na área da metafísica, que tipicamente exigem um alto nível de expressividade para capturar de maneira adequada as noções e termos complexos na medida em que ocorrem.
Entretanto, a implementação de lógicas tão ricas em computadores é, sem dúvida, bastante triviais. Em nosso trabalho, fazemos uso de uma abordagem indireta, que nos permite reutilizar as tecnologias empregadas para provar os teoremas existentes. A ideia principal é empregar a lógica clássica de primeira ordem como uma metalógica, na qual poderemos modelar e implementar as variantes das lógicas modais de primeira ordem. Então implementamos esse último modelo dando seguimento à modelagem e análise do argumento ontológico.
Essa abordagem metalógica ao raciocínio universal pode ser aplicada em muitas outras áreas. Hoje eu tenho um interesse especial em adaptar essa técnica para a implementação de uma denominada lógica deôntica, que é relevante no sentido de permitir que as máquinas executem um raciocínio legal e ético. Até então muitos poucos modelos como esse descrito acima foram implementados.
Qual a relação entre os seus interesses de pesquisa com a área de Prova Automática de Teoremas?
A Prova automática de teoremas está no foco de nossas pesquisas. Junto com meus alunos Alexander Steen e Max Wisniewski na FU Berlin, estou trabalhando no desenvolvimento de uma prova automática de teoremas de primeira ordem Leo-III (http://page.mi.fu-berlin.de/lex/leo3/), e antes disso, eu trabalhei no desenvolvimento do Leo-II (http://page.mi.fu-berlin.de/cbenzmueller/leo/) em um projeto com Larry Paulson, na Cambridge University, no Reino Unido. Esses sistemas funcionam, a princípio, como raciocinadores centrais em nossa abordagem metalógica ao raciocínio universal. No entanto, eu frequentemente faço uso desses raciocinadores de maneira indireta através de um outro sistema, o processador de fórmulas Isabelle/HOL, cuja interface usuário é bastante interativa e apresenta pontes potenciais aos provadores de teoremas externos, incluindo aquele que foi desenvolvido por mim, o Leo. Eu geralmente tiro enorme proveito das coalescências atuais das tecnologias de prova automática de teorema que tem sido utilizadas nas minhas pesquisas em assistentes de prova de primeira ordem, particularmente o Isabelle/HOL. Tem se visto um rápido avanço no suporte de automação nesses sistemas e sem sombra de dúvida elas trazem muitos benefícios nas aplicações.
Qual a importância prática de uma Lógica Universal (conforme foi pensada por Leibniz) onde é possível raciocinar sobre qualquer outra lógica?
Aplicações distintas, em particular aquelas que englobam disciplinas diferentes, geralmente exigem formalismos lógicos bastante diferenciados. Infelizmente ainda não chegamos a uma abordagem lógica universal, particularmente, uma que tenha relevância prática e que poderia ser empregada nessas aplicações (conforme pensado por Leibniz). Isso é lastimável já que implementar e manter todas as espécies heterogêneas em uma lógica abrangente é sem dúvida muito difícil e exigiria muitos recursos. Logo, não é de surpreender que muitas espécies dessa vasta gama de elementos somente existam no papel, nunca tendo sido implementadas e aplicadas na prática.
A abordagem metalógica ao raciocínio universal lógico que eu estou propondo aqui tem o objetivo de reverter essa situação. A mensagem principal é: embora não seja possível propor uma lógica universal como um “objeto” conforme pensado por Leibniz, pode ser possível ter uma metalógica universal onde poderemos modelar, analisar e aplicar as várias espécies desses elementos. E nesse sentido, essa abordagem tenta oferecer uma resposta interessante ao desafio de Leibniz.
Em quais pesquisas o senhor está trabalhando no momento?
Eu considero a ética de máquina um tópico bastante relevante em minhas pesquisas. Aparentemente a automação de raciocínio não trivial ético e legal em máquinas exige a implementação de formalismos lógicos potentes e robustos (por exemplo, a lógica deôntica moderna). Atualmente eu tenho investigado se uma abordagem metalógica para um raciocínio lógico universal tem algum impacto em tal lógica e em suas aplicações em ética de máquina e lei de máquina.
