Automated Reasoning

At RISC we are devoted to the foundations, the design, and the implementation of software to generate mathematical proofs.

The main enterprise in the area of automated reasoning at RISC is the Theorema project. Theorema has been initiated around 1995 by Bruno Buchberger, who has led the project ever since. Some activities in the area of formal methods are tightly related to what we do in automated reasoning.

Ongoing Projects

Software

Theorema

A Mathematical Assistant System implemented in Mathematica

The present prototype version of the Theorema software system is implemented in Mathematica . The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. ...

MoreSoftware Website

Publications

2021

[Cerna]

A Special Case of Schematic Syntactic Unification

David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]
[bib]
@techreport{RISC6349,
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}
[Dundua]

Variadic equational matching in associative and commutative theories

Besik Dundua, Temur Kutsia, Mircea Marin

Journal of Symbolic Computation 106, pp. 78-109. 2021. Elsevier, ISSN 0747-7171. [doi] [pdf]
[bib]
@article{RISC6260,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic equational matching in associative and commutative theories}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {106},
pages = {78--109},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1016/j.jsc.2021.01.001}
}
[Jebelean]

A Heuristic Prover for Elementary Analysis in Theorema

Tudor Jebelean

Technical report no. 21-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@techreport{RISC6293,
author = {Tudor Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
language = {english},
abstract = {We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.},
number = {21-07},
year = {2021},
month = {April},
keywords = {Theorema, S-decomposition, automated theorem proving},
length = {29},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Kutsia]

9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), short and work-in-progress papers

Temur Kutsia (editor)

Technical report no. 21-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6359,
author = {Temur Kutsia (editor)},
title = {{9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), short and work-in-progress papers}},
language = {english},
abstract = {This collection contains short and work-in-progress papers presented at the 9th International Symposium on Symbolic Computation in Software Science, SCSS 2021.},
number = {21-16},
year = {2021},
month = {August},
keywords = {Symbolic computation, software science, artificial intelligence},
length = {56},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Maletzky]

A generic and executable formalization of signature-based Gröbner basis algorithms

Alexander Maletzky

J. Symb. Comput. 106, pp. 23-47. 2021. Elsevier, ISSN 0747-7171. arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001. [url]
[bib]
@article{RISC6225,
author = {Alexander Maletzky},
title = {{A generic and executable formalization of signature-based Gröbner basis algorithms}},
language = {english},
journal = {J. Symb. Comput.},
volume = {106},
pages = {23--47},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
note = {arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001},
refereed = {yes},
length = {25},
url = {https://arxiv.org/abs/2012.02239}
}
[Pau]

Proximity-Based Unification and Matching for Full Fuzzy Signatures

Temur Kutsia, Cleo Pau

Technical report no. 21-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@techreport{RISC6296,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},
language = {english},
abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},
number = {21-08},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},
length = {15},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Pau]

Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures

Temur Kutsia, Cleo Pau

Technical report no. 21-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@techreport{RISC6297,
author = {Temur Kutsia and Cleo Pau},
title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},
number = {21-09},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},
length = {15},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Pau]

Proximity-Based Unification and Matching for Fully Fuzzy Signatures

Cleo Pau, Temur Kutsia

In: Proceedings of the 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021, , pp. 1-6. 2021. IEEE, isbn 978-1-6654-4407-1. [doi] [pdf]
[bib]
@inproceedings{RISC6369,
author = {Cleo Pau and Temur Kutsia},
title = {{Proximity-Based Unification and Matching for Fully Fuzzy Signatures}},
booktitle = {{Proceedings of the 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021}},
language = {english},
pages = {1--6},
publisher = {IEEE},
isbn_issn = {isbn 978-1-6654-4407-1},
year = {2021},
editor = { },
refereed = {yes},
length = {6},
url = {https://doi.org/10.1109/FUZZ45933.2021.9494438}
}
[Reichl]

Semantic Evaluation versus SMT Solving in the RISCAL Model Checker

Wolfgang Schreiner, Franz-Xaver Reichl

Technical report no. 21-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6328,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{Semantic Evaluation versus SMT Solving in the RISCAL Model Checker}},
language = {english},
abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion oftheir fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room forimprovements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},
number = {21-11},
year = {2021},
month = {June},
keywords = {model checking, satisfiability solving, formal specification, formal verficiation},
sponsor = {JKU Linz Institute of Technology (LIT) Project LOGTECHEDU, Aktion Österreich- Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255.},
length = {30},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Reichl]

First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving

Wolfgang Schreiner, Franz-Xaver Reichl

In: Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021, Temur Kutsia (ed.), Electronic Proceedings in Theoretical Computer Science 342, pp. 99-113. September 2021. ISSN 2075-2180. [doi]
[bib]
@inproceedings{RISC6361,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving}},
booktitle = {{Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021}},
language = {english},
abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original approach of semantic evaluation (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation of the two approaches and a discussion of their fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, we identify classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room for improvements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {342},
pages = {99--113},
isbn_issn = {ISSN 2075-2180},
year = {2021},
month = {September},
editor = {Temur Kutsia},
refereed = {yes},
keywords = {model checking, SMT solving, first-order logic, automated reasoning, formal methods},
sponsor = {e JKU Linz LIT Project LOGTECHEDU, Aktion Österreich-Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255},
length = {15},
url = {https://doi.org/10.4204/EPTCS.342.9}
}
[Schreiner]

Thinking Programs

Wolfgang Schreiner

Texts & Monographs in Symbolic Computation 1st edition, 2021. Springer, Cham, Switzerland, Hardcover ISBN 978-3-030-80506-7, Softcover ISBN 978-3-030-80509-8, eBook ISBN 978-3-030-80507-4. [doi]
[bib]
@book{RISC6371,
author = {Wolfgang Schreiner},
title = {{Thinking Programs}},
language = {english},
series = {Texts & Monographs in Symbolic Computation},
publisher = {Springer},
address = {Cham, Switzerland},
isbn_issn = {Hardcover ISBN 978-3-030-80506-7, Softcover ISBN 978-3-030-80509-8, eBook ISBN 978-3-030-80507-4},
year = {2021},
edition = {1st},
translation = {0},
length = {636},
url = {https://doi.org/10.1007/978-3-030-80507-4}
}
[Windsteiger]

Automated Theorem Proving in the Classroom

W. Windsteiger

Technical report no. 21-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2021. Extended version of keynote talk at ADG 2021 conference. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6356,
author = {W. Windsteiger},
title = {{Automated Theorem Proving in the Classroom}},
language = {english},
abstract = {We report on several scenarios of using automated theorem proving software in university education. In particular,we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial intelligence. The purpose of using logic-software in our teaching is emph{not} to teach studentsthe proper use of a particular piece of software. In contrast, we try to emph{employ} certain software in orderto spark students' motivation and to support their understanding of logic principles they are supposed tounderstand after having passed the course. In a sense, we try to let the software act as a logic-tutor, the software is not an additional subject we teach.},
number = {21-15},
year = {2021},
month = {August},
note = {Extended version of keynote talk at ADG 2021 conference},
keywords = {Theorema, Logic Education},
length = {18},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

2020

[Cerna]

Idempotent Anti-unification

David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [doi] [pdf]
[bib]
@article{RISC6023,
author = {David Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification}},
language = {english},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {2},
pages = {10:1--10:32},
publisher = {ACM Press},
isbn_issn = {ISSN 1529-3785},
year = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Cerna]

Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App

David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: ITICSE 2020, ACM (ed.), Proceedings of ITICSE, pp. 61-67. 2020. 9781450368742. [doi]
[bib]
@inproceedings{RISC6096,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App}},
booktitle = {{ITICSE 2020}},
language = {english},
abstract = {In this paper, we share our experiences concerning the introduc-tion of the Android-based self-study app AXolotl within the first-semester logic course offered at our university. This course is manda-tory for students majoring in Computer Science and Artificial In-telligence. AXolotl was used as part of an optional lab assignmentbridging clausal reasoning and SAT solving with classical reason-ing, proof construction, and first-order logic. The app provides anintuitive interface for proof construction in various logical calculiand aids the students through rule application. The goal of thelab assignment was to help students make a smoother transitionfrom clausal and decompositional reasoning used earlier in thecourse to inferential and contextual reasoning required for proofconstruction and first-order logic. We observed that the lab had apositive influence on students’ understanding and end the paperwith a discussion of these results.},
pages = {61--67},
isbn_issn = {9781450368742},
year = {2020},
editor = {ACM},
refereed = {yes},
length = {7},
conferencename = {ITICSE},
url = {https://dl.acm.org/doi/10.1145/3341525.3387409}
}
[Cerna]

Computational Logic in the First Semester of Computer Science: An Experience Report

David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU, Springer (ed.), Proceedings of CSEDU, pp. 374-381. 2020. 978-989-758-417-6. [doi]
[bib]
@inproceedings{RISC6097,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Computational Logic in the First Semester of Computer Science: An Experience Report}},
booktitle = {{Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU}},
language = {english},
abstract = {Nowadays, logic plays an ever-increasing role in modern computer science, in theory as well as in practice.Logic forms the foundation of the symbolic branch of artificial intelligence and from an industrial perspective,logic-based verification technologies are crucial for major hardware and software companies to ensure thecorrectness of complex computing systems. The concepts of computational logic that are needed for such purposes are often avoided in early stages of computer science curricula. Instead, classical logic education mainlyfocuses on mathematical aspects of logic depriving students to see the practical relevance of this subject. Inthis paper we present our experiences with a novel design of a first-semester bachelor logic course attendedby about 200 students. Our aim is to interlink both foundations and applications of logic within computerscience. We report on our experiences and the feedback we got from the students through an extensive surveywe performed at the end of the semester.},
pages = {374--381},
isbn_issn = {978-989-758-417-6},
year = {2020},
editor = {Springer},
refereed = {yes},
length = {8},
conferencename = {CSEDU},
url = {https://www.scitepress.org/Link.aspx?doi=10.5220/0009464403740381}
}
[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna, Temur Kutsia

In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 26:1-26:20. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC6132,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {26:1--26:20},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {20},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12352/}
}
[Cerna]

Higher-order pattern generalization modulo equational theories

David M. Cerna, Temur Kutsia

Mathematical Structures in Computer Science 30(6), pp. 627-663. 2020. ISSN 0960-1295. [url]
[bib]
@article{RISC6226,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-order pattern generalization modulo equational theories}},
language = {english},
journal = {Mathematical Structures in Computer Science},
volume = {30},
number = {6},
pages = {627--663},
isbn_issn = {ISSN 0960-1295},
year = {2020},
refereed = {yes},
length = {37},
url = {https://www.cambridge.org/core/services/aop-cambridge-core/content/view/88E26F155F0FD02B3EDD648971D9AD1B/S0960129520000110a.pdf/higher-order-pattern-generalization-modulo-equational-theories.pdf}
}
[Cerna]

Anti-unification and the Theory of Semirings

David M. Cerna

Theor. Comput. Sci. 848, pp. 133-139. 2020. RISC / CAS ICS, 0304-3975. [doi]
[bib]
@article{RISC6234,
author = {David M. Cerna},
title = {{Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only unitequations (more than one) is nullary. Such pure theories are artificial and are of little effect onpractical aspects of anti-unification. In this work, we extend these nullarity results to the theory ofsemirings, a heavily studied theory with many practical applications. Furthermore, our argumentholds over semirings with commutative multiplication and/or idempotent addition. We also cover afew open questions discussed in previous work.},
journal = {Theor. Comput. Sci.},
volume = {848},
pages = {133--139},
isbn_issn = {0304-3975},
year = {2020},
refereed = {yes},
institution = {RISC / CAS ICS},
length = {7},
url = {https://doi.org/10.1016/j.tcs.2020.10.020}
}
[Cerna]

Schematic Refutations of Formula Schemata

David Cerna and Alexander Leitsch and Anela Lolic

Journal of Automated Reasoning, pp. -. 2020. 1573-0670. [doi]
[bib]
@article{RISC6235,
author = {David Cerna and Alexander Leitsch and Anela Lolic},
title = {{Schematic Refutations of Formula Schemata}},
language = {english},
abstract = {Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.},
journal = {Journal of Automated Reasoning},
pages = {--},
isbn_issn = {1573-0670},
year = {2020},
refereed = {yes},
length = {47},
url = {https://doi.org/10.1007/s10817-020-09583-8}
}
[Cerna]

A Mobile Application for Self-Guided Study of Formal Reasoning

David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya

In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019, Pedro Quaresma and Walther Neuper and Jo{ {a}}o Marcos (ed.), EPTCS 313, pp. 35-53. 2020. 2075-2180. [doi]
[bib]
@inproceedings{RISC6236,
author = {David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
booktitle = {{Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019}},
language = {english},
abstract = {In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.},
series = {EPTCS},
volume = {313},
pages = {35--53},
isbn_issn = {2075-2180},
year = {2020},
editor = {Pedro Quaresma and Walther Neuper and Jo{~{a}}o Marcos},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4204/EPTCS.313.3}
}

Loading…