Towards Verified Handwritten Calculational Proofs

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2018

Autores

Mendes, A (Autor) Outra; Ferreira, JF (Autor) Outra

Ata de Conferência Internacional

Título: INTERACTIVE THEOREM PROVING, ITP 2018

Páginas: 432-440

9th International Conference on Interactive Theorem Proving (ITP) Held as Part of the Federated Logic Conference (FloC)

Oxford, ENGLAND, JUL 09-12, 2018

Indexação

ISI Web of Knowledge - 1 Citação

Outras Informações

ID Authenticus: P-00Q-8Q0

DOI: 10.1007/978-3-319-94821-8_25

Abstract (EN): Despite great advances in computer-assisted proof systems, writing formal proofs using a traditional computer is still challenging due to mouse-and-keyboard interaction. This leads to scientists often resorting to pen and paper to write their proofs. However, when handwriting a proof, there is no formal guarantee that the proof is correct. In this paper we address this issue and present the initial steps towards a system that allows users to handwrite proofs using a pen-based device and that communicates with an external theorem prover to support the users throughout the proof writing process. We focus on calculational proofs, whereby a theorem is proved by a chain of formulae, each transformed in some way into the next. We present the implementation of a proof-of-concept prototype that can formally verify handwritten calculational proofs without the need to learn the specific syntax of theorem provers.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 9