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

Combinatorics and Codes for Information Security [SBA-K1]

Project Duration: 01/01/2017 - 31/12/2020

Software

PρLog (pronounced Pē-rō-log) is an experimental tool that extends logic programming with strategic conditional transformation rules, combining Prolog with ρLog calculus. It deals with term sequences (also called hedges), transforming them by conditional rules. Transformations are nondeterministic and may yield ...

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. ...

Publications

[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna , Temur Kutsia

Technical report no. 20-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. RISC Report, Febrary 2020. [pdf]
@techreport{RISC6080,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
language = {english},
abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },
number = {20-02},
year = {2020},
month = {Febrary},
howpublished = {RISC Report},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[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, , pp. 1-7. 2020. https://doi.org/10.1145/3341525.3387409.
@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 = {1--7},
isbn_issn = {https://doi.org/10.1145/3341525.3387409},
year = {2020},
editor = {ACM},
refereed = {yes},
length = {7}
}
[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: CSEDU 2020, , pp. 1-8. 2020. not yet known.
@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 = {{CSEDU 2020}},
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 = {1--8},
isbn_issn = {not yet known},
year = {2020},
editor = {Springer},
refereed = {yes},
length = {8}
}
[Cerna]

A Note on Anti-unification and the Theory of Semirings

David M. Cerna

RISC. Technical report, 2020. [pdf]
@techreport{RISC6101,
author = {David M. Cerna},
title = {{A Note on Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only identity equations (more than one) is nullary. Such pure theories are artificial and are of little effect on practical aspects of anti-unification. In this work, we extend these nullarity results to the theory of semirings, a heavily studied theory with many practical applications. Furthermore, our argument holds over semirings with commutative multiplication and/or idempotent addition. },
year = {2020},
institution = {RISC},
length = {4}
}
[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), , 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]
@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/}
}
[Dramnesc]

Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema

Isabela Dramnesc, Tudor Jebelean

Technical report no. 20-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2020. [pdf]
@techreport{RISC6094,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema}},
language = {english},
number = {20-04},
year = {2020},
month = {April},
length = {25},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Dundua]

Constraint Solving over Multiple Similarity Relations

Besik Dundua, Temur Kutsia, Mircea Marin, Cleopatra Pau

In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), , Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 30:1-30:19. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [url]
@inproceedings{RISC6133,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleopatra Pau},
title = {{Constraint Solving over Multiple Similarity Relations}},
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 = {30:1--30:19},
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 = {19},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.30}
}
[Kutsia]

Unification modulo alpha-equivalence in a mathematical assistant system

Temur Kutsia

Technical report no. 20-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2020. [pdf]
@techreport{RISC6074,
author = {Temur Kutsia},
title = {{Unification modulo alpha-equivalence in a mathematical assistant system}},
language = {english},
number = {20-01},
year = {2020},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Kutsia]

Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques

Ilias Kotsireas, Temur Kutsia, Dimitris Simos

Annals of Mathematics and Artificial Intelligence 88(1), pp. 213-236. 2020. ISSN 1573-7470. [url] [pdf]
@article{RISC6116,
author = {Ilias Kotsireas and Temur Kutsia and Dimitris Simos},
title = {{ Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques}},
language = {english},
journal = {Annals of Mathematics and Artificial Intelligence},
volume = {88},
number = {1},
pages = {213--236},
isbn_issn = {ISSN 1573-7470},
year = {2020},
refereed = {yes},
length = {24},
url = {https://doi.org/10.1007/s10472-018-9607-9}
}
[Kutsia]

Proceedings of The 34th International Workshop on Unification, UNIF 2020

Temur Kutsia and Andrew M. Marshall (Editors)

Technical report no. 20-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2020. [pdf]
@techreport{RISC6129,
author = {Temur Kutsia and Andrew M. Marshall (Editors)},
title = {{Proceedings of The 34th International Workshop on Unification, UNIF 2020}},
language = {english},
number = {20-10},
year = {2020},
length = {82},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Reichl]

The Integration of SMT Solvers into the RISCAL Model Checker

Franz-Xaver Reichl

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. April 2020. [pdf]
@misc{RISC6103,
author = {Franz-Xaver Reichl},
title = {{The Integration of SMT Solvers into the RISCAL Model Checker}},
language = {english},
abstract = {In this thesis we present an alternative approach to check specifications from asubstantial subset of the RISC Algorithm Language (RISCAL). The main goal forthis new approach is to speed up checks done in RISCAL. For this purpose wedeveloped a translation from the RISCAL language to the SMT-LIB language (usingthe QF_UFBV logic). The realisation of this translation in particular required to solvethe problems of eliminating RISCAL’s quantifiers and of encoding RISCAL’s typesand operations. We formally described core components of this translation, provedsome aspects of their correctness, and implemented it in the programming languageJava. We tested the implementation together with the SMT solvers Boolector, CVC4,Yices and Z3, on several real world RISCAL specifications. Additionally, we evaluatedthe performance of our approach by systematic benchmarks and compared it withthat of the original RISCAL checking mechanism. Finally, we analysed the testsin order to determine patterns in specifications that could possibly have a negativeinfluence on the performance of the presented method. The tests showed that amongthe four used SMT solvers, the solver Yices delivered, for almost all, tests the bestresults. Additionally, the tests indicated that the translation is indeed a viablealternative to RISCAL’s current checking method, especially when used togetherwith Yices. So the translation used with Yices was substantially faster than RISCALin approximately 75% of the test cases. Nevertheless, the tests also illustrated thatRISCAL could still check certain test cases substantially faster. Thus, the translationcannot fully replace RISCAL’s current checking methods.},
year = {2020},
month = {April},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal methods, automated reasoning, model checking, program verification},
sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU.},
length = {151}
}
[Reichl]

Mathematical Model Checking Based on Semantics and SMT

Wolfgang Schreiner, Franz-Xaver Reichl

Transactions on Internet Research 16(2), pp. 4-13. July 2020. IPSI, ISSN 1820-4503. [url]
@article{RISC6117,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{Mathematical Model Checking Based on Semantics and SMT}},
language = {english},
abstract = {We report on the usage and implementation of RISCAL, a model checker formathematical theories and algorithms based on a variant of first-order logicwith finite models; this allows to automatically decide the validity of allformulas and to verify the correctness of all algorithms specified by suchformulas. We describe the semantics-based implementation of the checker aswell as a recently developed alternative based on SMT solving, andexperimentally compare their performance. Furthermore, we report on ourexperience with RISCAL for enhancing education in computer science andmathematics, in particular in academic courses on logic, formal methods, andformal modeling. By the use of this software, students are encouraged toactively engage with the course material by solving concrete problems wherethe correctness of a solution is automatically checked; if a solution is notcorrect or the student gets stuck, the software provides additional insightand hints that aid the student towards the desired result.},
journal = {Transactions on Internet Research},
volume = {16},
number = {2},
pages = {4--13},
publisher = {IPSI},
isbn_issn = {ISSN 1820-4503},
year = {2020},
month = {July},
refereed = {yes},
keywords = {model checking, logic, semantics, formal verification, reasoning about programs, computer science education},
sponsor = {Johannes Kepler University, Linz, Institute of Technology(LIT) project LOGTECHEDU and OEAD WTZ project SK 14/2018 SemTech},
length = {10},
url = {http://ipsitransactions.org/journals/papers/tir/2020jul/p2.pdf}
}

[Cerna]

Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire

David M. Cerna

Submitted to the RISC Report Series. Feburary 2019. [pdf] [xlsx]
@techreport{RISC5885,
author = {David M. Cerna},
title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
language = {english},
abstract = {In this technical report we cover the choice of layout and intentions behind our end of the semester questionnaire as well as our interpretation of student answers, resulting statistical analysis, and inferences. Our questionnaire is to some extent free-form in that we provide instructions concerning the desired content of the answers but leave the precise formulation of the answer to the student. Our goal, through this approach, was to gain an understanding of how the students viewed there own progress and interest in the course without explicitly guiding them. Towards this end, we chose to have the students draw curves supplemented by short descriptions of important features. We end with a discussion of the benefits and downsides of such a questionnaire as well as what the results entail concerning future iterations of the course. },
year = {2019},
month = {Feburary},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

The Castle Game

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]
@techreport{RISC5886,
author = {David M. Cerna},
title = {{The Castle Game}},
language = {english},
abstract = {A description of a game for teaching certain aspects of first-order logic based on the Drink's Paradox. },
year = {2019},
length = {3},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

Manual for AXolotl

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf] [zip] [jar]
@techreport{RISC5887,
author = {David M. Cerna},
title = {{Manual for AXolotl}},
language = {english},
abstract = {In this document we outline how to play our preliminary version of \textbf{AX}olotl. We present a sequence of graphics illustrating the step by step process of playing the game. },
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

Higher-Order Pattern Generalization Modulo Equational Theories

David M. Cerna and Temur Kutsia

Submitted to the RISC Report Series. 2019. [pdf]
@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {In this paper we address Three problems related to unital anti-unification. First, we develop a generalalgorithm based on a tree grammar representation of the set of computed generalizations. Secondlywe show that restricting the algorithm to computing linear generalizations only or to term signaturescontaining a single unital function results in a procedure which is minimal complete and Finitary.Thirdly, we show that when the term signature contains two unital functions, unital anti-unification isNullary.The algorithm does not depend on the number of idempotent function symbols in the input terms. Thelanguage generated by the grammar is the minimal complete set of generalizations of the givenanti-unification problem, which implies that idempotent anti-unification is infinitary.},
year = {2019},
length = {40},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

AXolotl: A Self-study Tool for First-order Logic

David Cerna

Submitted to the RISC Report Series. May 2019. [pdf]
@techreport{RISC5936,
author = {David Cerna},
title = {{AXolotl: A Self-study Tool for First-order Logic}},
language = {english},
year = {2019},
month = {May},
length = {4},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

A Generic Framework for Higher-Order Generalizations

David M. Cerna, Temur Kutsia

In: Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), , Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [url]
@inproceedings{RISC5947,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {131},
pages = {10:1--10:19},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2019},
editor = {Herman Geuvers},
refereed = {yes},
length = {19},
url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}
}
[Cerna]

On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]
@techreport{RISC5981,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
year = {2019},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

A Mobile Application for Self-Guided Study of Formal Reasoning

David M. Cerna and Rafael Kiesel and Alexandra Dzhiganskaya

Submitted to the RISC Report Series. October 2019. [pdf]
@techreport{RISC5991,
author = {David M. Cerna and Rafael Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
language = {english},
abstract = {In this work we introduce AXolotl, a self-study aid designed to guide students through the basics offormal 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 goalwas to minimize the possibility of user errors which distract from the learning process. Such as typosor inconsistent application of the provided rules. The system includes a zoomable proof viewer whichdisplays the progress made so far and allows for storage of the completed proofs as a JPEG or L A TEXfile. 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, AXolotlsupports problems which can be solved using rules which transform a single expression into a set ofexpressions. This covers educational scenarios found in our first semester introduction to logic courseand helps bridge the gap between propositional and first-order reasoning. Future developments willinclude rewrite rules which take a set of expressions and return a set of expressions, as well as aquantified first-order extension.},
year = {2019},
month = {October},
length = {18},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}