# 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 Lead: Teimuraz Kutsia
Project Duration: 01/01/2017 - 31/12/2020

## Software

### PrhoLog

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}
}
[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}
}

[Cerna]

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

#### David M. Cerna

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

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

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

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

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

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

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}
}
[Cerna]

### Idempotent Anti-unification

#### David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2019. ACM Press, ISSN 1529-3785. [url] [pdf]
@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 = {2019},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Dundua]

### Variadic Equational Matching

#### Besik Dundua, Temur Kutsia, Mircea Marin

In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, , Lecture Notes in Computer Science 11617, pp. 77-92. 2019. Springer, ISBN 978-3-030-23249-8. [pdf]
@inproceedings{RISC5948,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic Equational Matching}},
booktitle = {{Intelligent Computer Mathematics - 12th International Conference, CICM 2019}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11617},
pages = {77--92},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-23249-8},
year = {2019},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti Coen},
refereed = {yes},
length = {16}
}
[Dundua]

### A Rule-based Approach to the Decidability of Safety of ABACα

#### Mircea Marin, Temur Kutsia, Besik Dundua

In: Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019, , pp. 173-178. 2019. ACM, ISBN 978-1-4503-6753-0. [url] [pdf]
@inproceedings{RISC5955,
author = {Mircea Marin and Temur Kutsia and Besik Dundua},
title = {{A Rule-based Approach to the Decidability of Safety of ABACα}},
booktitle = {{Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019}},
language = {english},
pages = {173--178},
publisher = {ACM},
isbn_issn = {ISBN 978-1-4503-6753-0},
year = {2019},
editor = {Florian Kerschbaum and Atefeh Mashatan and Jianwei Niu and Adam J. Lee},
refereed = {yes},
length = {6},
url = {https://doi.org/10.1145/3322431.3325416}
}
[Maletzky]

### Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL

#### A. Maletzky

In: Intelligent Computer Mathematics (Proceedings of CICM 2019, Prague, Czech Republic, July 8-12), , Proceedings of CICM 2019, Lecture Notes in Computer Science , pp. ?-?. 2019. Springer, to appear. [pdf]
@inproceedings{RISC5919,
author = {A. Maletzky},
title = {{Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL}},
booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2019, Prague, Czech Republic, July 8-12)}},
language = {english},
series = {Lecture Notes in Computer Science},
pages = {?--?},
publisher = {Springer},
isbn_issn = {?},
year = {2019},
note = {to appear},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti-Coen},
refereed = {yes},
length = {16},
conferencename = {CICM 2019}
}
[Maletzky]

### Gröbner Bases and Macaulay Matrices in Isabelle/HOL

#### A. Maletzky

RISC, JKU Linz. Technical report, 2019. Submitted to Formal Aspects of Computing. [pdf]
@techreport{RISC5929,
author = {A. Maletzky},
title = {{Gröbner Bases and Macaulay Matrices in Isabelle/HOL}},
language = {english},
year = {2019},
note = {Submitted to Formal Aspects of Computing},
institution = {RISC, JKU Linz},
length = {14}
}
[Maletzky]

### Theorema-HOL: Classical Higher-Order Logic in Theorema

#### A. Maletzky

Technical report no. 19-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 2019. [pdf]
@techreport{RISC5930,
author = {A. Maletzky},
title = {{Theorema-HOL: Classical Higher-Order Logic in Theorema}},
language = {english},
number = {19-03},
year = {2019},
month = {June},
length = {24},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Pau]

### Computing All Maximal Clique Partitions in a Graph

#### Temur Kutsia, Cleo Pau

Technical report no. 19-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
@techreport{RISC5939,
author = {Temur Kutsia and Cleo Pau},
title = {{Computing All Maximal Clique Partitions in a Graph}},
language = {english},
number = {19-04},
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}
}
[Pau]

### Solving Proximity Constraints

#### Temur Kutsia, Cleo Pau

Technical report no. 19-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
@techreport{RISC5950,
author = {Temur Kutsia and Cleo Pau},
title = {{Solving Proximity Constraints}},
language = {english},
number = {19-06},
year = {2019},
length = {22},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Pau]

### Matching and Generalization Modulo Proximity and Tolerance

#### Temur Kutsia, Cleo Pau

Technical report no. 19-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
@techreport{RISC5953,
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance}},
language = {english},
number = {19-07},
year = {2019},
length = {5},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Schreiner]

### Theorem and Algorithm Checking for Courses on Logic and Formal Methods

#### Wolfgang Schreiner

In: Post-Proceedings ThEdu'18, , Proceedings of 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, Electronic Proceedings in Theoretical Computer Science (EPTCS) 290, pp. 56-75. April 1 2019. Open Publishing Association, ISSN 2075-2180. [url] [pdf]
@inproceedings{RISC5895,
author = {Wolfgang Schreiner},
title = {{Theorem and Algorithm Checking for Courses on Logic and Formal Methods}},
booktitle = {{Post-Proceedings ThEdu'18}},
language = {english},
abstract = {The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms. A RISCAL specification describes an infinite class of models each of which has finite size; this allows to fully automatically check in such a model the validity of all theorems and the correctness of all algorithms. RISCAL thus enables us to quickly verify/falsify the specific truth of propositions in sample instances of a model class before attempting to prove their general truth in the whole class: the first can be achieved in a fully automatic way while the second typically requires our assistance. RISCAL has been mainly developed for educational purposes. To this end this paper reports on some new enhancements of the tool: the automatic generation of checkable verification conditions from algorithms, the visualization of the execution of procedures and the evaluation of formulas illustrating the computation of their results, and the generation of Web-based student exercises and assignments from RISCAL specifications. Furthermore, we report on our first experience with RISCAL in the teaching of courses on logic and formal methods and on further plans to use this tool to enhance formal education.},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {290},
pages = {56--75},
publisher = {Open Publishing Association},
isbn_issn = {ISSN 2075-2180},
year = {2019},
month = {April 1},
editor = {Pedro Quaresma and Walther Neuper},
refereed = {yes},
sponsor = {Linz Institute of Technology (LIT), Project LOGTECHEDU “Logic Technology for Computer Science Education” and OEAD WTZ project SK 14/2018 SemTech},
length = {20},
conferencename = {7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018},
url = {http://dx.doi.org/10.4204/EPTCS.290.5}
}