A carregar...
Publicação
ONLINE INTERACTIVE TOOL FOR LEARNING LOGICAL PROOF SYSTEMS
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 2.56 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
For many areas, including mathematics and computer science, logic is a basic but important
topic. In particular, the notions of natural deduction and proof systems for natural
deduction are of fundamental interest.
Students learning logic benefit from the use of interactive, visual tools where they can
solve exercises and receive feedback from their attempts. However, most of these tools are
based on installable programs, or static, making it hard to expand them with additional
learning material and exercises. The few available online tools and courses focusing on
logic also tend to skip the topic of natural deduction.
The goal of this thesis is the development of a tool that hosts an interactive, visual
proof assistant in which a student can create (or load) a proof and attempt to solve it,
occasionally receiving feedback to help the student learn and progress at their own pace.
The tool’s design would leverage the work done on previously created tools of this kind
and function as a complementary tool for computational logic courses or any course that
includes natural deduction.
To achieve this, the system must implement basic logic algorithms, feature a logic
reasoner for the supported branches of logic, be capable of parsing text into formulas,
have mechanisms to provide feedback to users regarding errors and finally some kind of
exercise management system, allowing a qualified user to save proofs that can later be
loaded by any user, while maintaining the state it was saved as.
Finally, it’s intended to leverage its usability for automatic evaluation purposes, by
incorporating the system, if possible, with existing online e-learning platforms, such as
Moodle.
Para muitas áreas, incluindo matemática e ciência da computação, a lógica é um tópico básico mas importante. Em particular, as noções de dedução natural e sistemas de prova para dedução natural são de interesse fundamental. Estudantes que estejam a aprender lógica beneficiam da utilização de ferramentas interativas e visuais onde podem resolver exercícios e receber feedback durante as suas tentativas. No entanto, a maioria destas ferramentas baseia-se em programas instaláveis, ou estáticos, o que torna difícil expandi-los com exercicios e material de aprendizagem adicional. As poucas ferramentas e cursos online disponíveis que se focam em lógica também tendem a omitir o tópico da dedução natural. O objetivo desta tese é o desenvolvimento de uma ferramenta que aloje um assistente de prova interativo e visual, no qual um estudante pode criar (ou carregar) uma prova e tentar resolvê-la, ocasionalmente recebendo feedback que o ajude a aprender e progredir ao seu próprio ritmo. O design da ferramenta aproveitaria o trabalho realizado em ferramentas deste tipo criadas anteriormente e funcionaria como uma ferramenta complementar para cursos de lógica computacional ou qualquer curso que inclua dedução natural. Para alcançar isto, o sistema deve implementar algoritmos lógicos básicos, conter um raciocinador lógico para os ramos de lógica suportados, ser capaz de transformar texto em fórmulas, ter mecanismos para fornecer feedback a utilizadores referente a erros e, finalmente, algum tipo de sistema de gestão de exercícios, permitindo a um utilizador qualificado guardar provas que podem posteriormente ser carregadas por qualquer utilizador, mantendo o estado em que foi guardada. Por fim, pretende-se aproveitar a sua usabilidade para fins de avaliação automática, incorporando o sistema, se possível, em plataformas de e-learning online existentes, como o Moodle.
Para muitas áreas, incluindo matemática e ciência da computação, a lógica é um tópico básico mas importante. Em particular, as noções de dedução natural e sistemas de prova para dedução natural são de interesse fundamental. Estudantes que estejam a aprender lógica beneficiam da utilização de ferramentas interativas e visuais onde podem resolver exercícios e receber feedback durante as suas tentativas. No entanto, a maioria destas ferramentas baseia-se em programas instaláveis, ou estáticos, o que torna difícil expandi-los com exercicios e material de aprendizagem adicional. As poucas ferramentas e cursos online disponíveis que se focam em lógica também tendem a omitir o tópico da dedução natural. O objetivo desta tese é o desenvolvimento de uma ferramenta que aloje um assistente de prova interativo e visual, no qual um estudante pode criar (ou carregar) uma prova e tentar resolvê-la, ocasionalmente recebendo feedback que o ajude a aprender e progredir ao seu próprio ritmo. O design da ferramenta aproveitaria o trabalho realizado em ferramentas deste tipo criadas anteriormente e funcionaria como uma ferramenta complementar para cursos de lógica computacional ou qualquer curso que inclua dedução natural. Para alcançar isto, o sistema deve implementar algoritmos lógicos básicos, conter um raciocinador lógico para os ramos de lógica suportados, ser capaz de transformar texto em fórmulas, ter mecanismos para fornecer feedback a utilizadores referente a erros e, finalmente, algum tipo de sistema de gestão de exercícios, permitindo a um utilizador qualificado guardar provas que podem posteriormente ser carregadas por qualquer utilizador, mantendo o estado em que foi guardada. Por fim, pretende-se aproveitar a sua usabilidade para fins de avaliação automática, incorporando o sistema, se possível, em plataformas de e-learning online existentes, como o Moodle.
Descrição
Palavras-chave
Logic Proof System Natural Deduction Online Interactive Propositional Logic