Experiments with Automated Reasoning in the Class

Autor: Isabela Drămnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat
Přispěvatelé: West University of Timișoara [Roumanie] (WUT), Eszterházy Károly University, Rheinisch-Westfälische Technische Hochschule Aachen University (RWTH), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), This work is co-funded by the Erasmus+ Programme of the European Union, project ARC: Automated Reasoning in the Class, 2019-1-RO01-KA203-063943.
Jazyk: angličtina
Rok vydání: 2022
Předmět:
Zdroj: CICM 2022-15th Conference on Intelligent Computer Mathematics
CICM 2022-15th Conference on Intelligent Computer Mathematics, Sep 2022, Tbilisi / Hybrid, Georgia. pp.287-304, ⟨10.1007/978-3-031-16681-5_20⟩
Lecture Notes in Computer Science ISBN: 9783031166808
DOI: 10.1007/978-3-031-16681-5_20⟩
Popis: International audience; The European Erasmus+ project ARC-Automated Reasoning in the Class aims at improving the academic education in disciplines related to Computational Logic by using Automated Reasoning tools. We present the technical aspects of the tools as well as our education experiments, which took place mostly in virtual lectures due to the COVID pandemics. Our education goals are: to support the virtual interaction between teacher and students in the absence of the blackboard, to explain the basic Computational Logic algorithms, to study their implementation in certain programming environments, to reveal the main relationships between logic and programming, and to develop the proof skills of the students. For the introductory lectures we use some programs in C and in Mathematica in order to illustrate normal forms, resolution, and DPLL (Davis-Putnam-Logemann-Loveland) with its Chaff version, as well as an implementation of sequent calculus in the Theorema system. Furthermore we developed special tools for SAT (propositional satisfiability), some based on the original methods from the partners, including complex tools for SMT (Satisfiability Modulo Theories) that allow the illustration of various solving approaches. An SMT related approach is natural-style proving in Elementary Analysis, for which we developed and interesting set of practical heuristics. For more advanced lectures on rewrite systems we use the Coq programming and proving environment, in order on one hand to demonstrate programming in functional style and on the other hand to prove properties of programs. Other advanced approaches used in some lectures are the deduction based synthesis of algorithms and the techniques for program transformation.
Databáze: OpenAIRE
Externí odkaz: