A integração do tutorial interativo TryLogic via IMS Learning Tools Interoperability: construindo uma infraestrutura para o ensino de Lógica através de estratégias de demonstração e refutação

Abstract

Logic courses represent a pedagogical challenge and the recorded number of cases of failures
 and of discontinuity in them is often high. Amont other difficulties, students face
 a cognitive overload to understand logical concepts in a relevant way. On that track,
 computational tools for learning are resources that help both in alleviating the cognitive
 overload scenarios and in allowing for the practical experimenting with theoretical
 concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed
 at teaching to solve logical conjectures either by proofs or refutations. The tool was
 developed from the architecture of the tool TryOcaml, through support of the communication
 of the web interface ProofWeb in accessing the proof assistant Coq. The goals of
 TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving
 problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts
 related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing
 interactive tasks to the students. The present study also aims at: presenting our
 implementation of a formal system for refutation; describing the integration of our infrastructure
 with the Virtual Learning Environment Moodle through the IMS Learning
 Tools Interoperability specification; presenting the Conjecture Generator that works for
 the tasks involving proving and refuting; and, finally to evaluate the learning experience
 of Logic students through the application of the conjecture solving task associated to the
 use of the TryLogic

A disciplina de Lógica representa um desa o tanto para docentes como para discentes, o
 que em muitos casos resulta em reprovações e desistências. Dentre as dificuldades enfrentadas
 pelos alunos está a sobrecarga da capacidade cognitiva para compreender os conceitos
 lógicos de forma relevante. Neste sentido, as ferramentas computacionais de aprendizagem
 são recursos que auxiliam a redução de cenários de sobrecarga cognitiva, como também
 permitem a experiência prática de conceitos teóricos. O presente trabalho propõe uma
 tutorial interativo chamado TryLogic, visando ao ensino da tarefa de Demonstração
 ou Refutação (DxR) de conjecturas lógicas. Trata-se de uma ferramenta desenvolvida a
 partir da arquitetura do TryOcaml através do suporte de comunicação da interface web
 ProofWeb para acessar o assistente de demonstração de teoremas Coq. Os objetivos do
 TryLogic são: (1) Apresentar um conjunto de lições para aplicar estratégias heurísticas
 de análise de problemas em Lógica Proposicional; (2) Organizar em passo-a-passo a exposi
 ção dos conteúdos de Dedução Natural e Semântica Proposicional de forma sequencial;
 e (3) Fornecer aos alunos tarefas interativas. O presente trabalho propõe também apresentar
 a nossa implementação de um sistema formal de refutação; descrever a integração
 de nossa infraestrutura com o Ambiente Virtual de Aprendizagem Moodle através da especi
 cação IMS Learning Tools Interoperability ; apresentar o Gerador de Conjecturas de
 tarefas de Demonstração e Refutação e, por m, avaliar a experiência da aprendizagem
 de alunos de Lógica através da aplicação da tarefa de DxR em associação à utilização do
 TryLogic