[pt] INFRAESTRUTURA PARA PROVADORES INTERATIVOS DE TEOREMAS NA WEB

[en] INFRASTRUCTURE FOR WEB-BASED INTERACTIVE THEOREM PROVERS

[pt] JEFFERSON DE BARROS SANTOS

[pt] WEB

[pt] INTERFACE GRAFICA

[pt] PROVA DE TEOREMAS

[en] WEB

[en] GRAPHIC INTERFACE

[en] THEOREM PROVING

[pt] Prova automática de teoremas consiste na prova de teoremas matemáticos por intermédio de programas de computador. Dependendo da linguagem lógica em uso, o processo de provar uma determinada fórmula pode não ser computável. Além disso, dependendo do cálculo dedutivo empregado, a busca por uma prova envolve lidar com a possibilidade de aplicação de longas sequências de axiomas e regras de inferência. Tudo isso reforça a necessidade da intervenção humana no processo de prova em sistemas denominados provadores interativos de teoremas ou assistentes de prova. Em um cenário típico, um usuário interage com a máquina de prova através de uma interface gráfica, normalmente implementada como um aplicativo desktop. Recentemente, porém, muitos aplicativos deste tipo passaram a ser oferecidos para seus usuários através da web. Esta forma de disponibilizar software evita que o usuário final se preocupe com questões de instalação e configuração e possibilita o acesso ao sistema de qualquer computador, com qualquer sistema operacional, bastando ter disponível uma conexão com a Internet. Nesta dissertação, estudamos possibilidades de uso da web como plataforma para a construção de ambientes interativos para prova de teoremas. Nossa proposta é estudar os diferentes modelos de interação entre usuário e ambientes de prova automatizados e verificar como estes modelos podem ser adaptados para a web. Como resultado, apresentamos uma ferramenta gráfica para visualização e manipulação direta de provas formais na web como uma interface alternativa entre usuários e provadores.

[en] Automatic theorem proving consists of proving mathematical theorems by means of computer programs. Depending on the logic used, the process of proving a formula is not computable. Moreover, depending of the deductive system applied to, the search for a proof can involve the application of long sequences of axioms and inference rules, reinforcing the need of human intervention in the proof process. Such systems are known as interactive theorem provers or proof assistants. In a typical scenario, the user interacts with the prover through a graphical interface, usually a desktop application. Recently, however, applications like those started to be delivered to users through the web. This way of software deployment avoids that final users have to deal with complex activities like prover installation and configuration and allows this user to access the system from different machines with a simple Internet connection. In this research we study the use of web as a platform for interactive theorem proving environments construction. Our purpose is to study some interaction models between user and automated proof environments and verify how these models can be adapted to work as a web application. As a result we show a graphical tool for visualization and direct manipulation of formal proofs on web to work as an alternative interface between user and proving machines.

EDWARD HERMANN HAEUSLER

DANIEL SCHWABE

EDWARD HERMANN HAEUSLER

MARCELO DA SILVA CORREA

ALEX DE VASCONCELLOS GARCIA

2010-09-27

2010-03-24

[pt] TEXTO

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

PORTUGUÊS

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318@1

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=16318@2

https://doi.org/10.17771/PUCRio.acad.16318