[en] INFRASTRUCTURE FOR WEB-BASED INTERACTIVE THEOREM PROVERS
[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 pr...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | pt |
| Published: |
MAXWELL
2010
|
| Subjects: | |
| Online Access: | https://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=16318@1 https://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=16318@2 http://doi.org/10.17771/PUCRio.acad.16318 |
| Summary: | [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. |
|---|