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.

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

2019

[Cerna]

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

David M. Cerna

Feburary 2019. [pdf] [xlsx]
[bib]
@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]
[bib]
@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]
[bib]
@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 with a unit element

David M. Cerna and Temur Kutsia

2019. [pdf]
[bib]
@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories with a unit element}},
language = {english},
abstract = {We consider anti-unification for simply typed lambda terms in theories defined by associativity,commutativity, identity (unit element) axioms and their combinations, and develop a sound andcomplete algorithm which takes two lambda terms and computes their equational generalizations inthe form of higher-order patterns. The problem is finitary: the minimal complete set of suchgeneralizations contains finitely many elements. We define the notion of optimal solution andinvestigate special fragments of the problem for which the optimal solution can be computed in linearor polynomial time.},
year = {2019},
length = {25},
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]
[bib]
@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), Herman Geuvers (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [url]
[bib]
@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]
[bib]
@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}
}
[Dundua]

Variadic Equational Matching

Besik Dundua, Temur Kutsia, Mircea Marin

In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen (ed.), Lecture Notes in Computer Science 11617, pp. 77-92. 2019. Springer, ISBN 978-3-030-23249-8. [pdf]
[bib]
@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, Florian Kerschbaum, Atefeh Mashatan, Jianwei Niu, Adam J. Lee (ed.), pp. 173-178. 2019. ACM, ISBN 978-1-4503-6753-0. [url] [pdf]
[bib]
@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), Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti-Coen (ed.), Proceedings of CICM 2019, Lecture Notes in Computer Science , pp. ?-?. 2019. Springer, to appear. [pdf]
[bib]
@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]
[bib]
@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]
[bib]
@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]
[bib]
@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]
[bib]
@techreport{RISC5950,
author = {Temur Kutsia and Cleo Pau},
title = {{Solving Proximity Constraints}},
language = {english},
number = {19-06},
year = {2019},
length = {21},
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]
[bib]
@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, Pedro Quaresma and Walther Neuper (ed.), 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]
[bib]
@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}
}
[Schreiner]

A Categorical Semantics of Relational First-Order Logic

Wolfgang Schreiner, Valerie Novitzká, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March 2019. [pdf]
[bib]
@techreport{RISC5900,
author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},
title = {{A Categorical Semantics of Relational First-Order Logic}},
language = {english},
abstract = {We present a categorical formalization of a variant of first-order logic. Unlike other textson this topic, the goal of this paper is to give a very transparent and self-contained accountwithout requiring more background than basic logic and set theory. Our focus is to showhow the semantics of first order formulas can be derived from their usual deduction rules.For understanding the core ideas, it is not necessary to investigate the internal term structureof atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations;in this sense our variant of first-order logic is “relational”. While the derived semanticsis based on categorical principles, it is nevertheless “constructive” in that it describesexplicit computations of the truth values of formulas. We demonstrate this by modeling thecategorical semantics in the RISCAL (RISC Algorithm Language) system which allows usto validate the core propositions by automatically checking them in finite models.},
year = {2019},
month = {March},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},
sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},
length = {34}
}
[Schreiner]

A Coalgebraic Operational Semantics for an Imperative Language

William Steingartner, Valerie Novitzká, Wolfgang Schreiner

Computing and Informatics, pp. -. 2019. ISSN 1335-9150. To appear.
[bib]
@article{RISC5980,
author = {William Steingartner and Valerie Novitzká and Wolfgang Schreiner},
title = {{A Coalgebraic Operational Semantics for an Imperative Language}},
language = {english},
abstract = {Operational semantics is a known and popular semantic method fordescribing the execution of programs in detail. The traditional definition of thismethod defines each step of a program as a transition relation. We present a newapproach on how to define operational semantics as a coalgebra over a category ofconfigurations. Our approach enables us to deal with a program that is written in asmall but real imperative language containing also the common program constructsas input and output statements, and declarations. A coalgebra enables to defineoperational semantics in a uniform way and it describes the behavior of the programs.The state space of our coalgebra consists of the configurations modeling theactual states; the morphisms in a base category of the coalgebra are the functionsdefining particular steps during the program’s executions. Polynomial endofunctordetermines this type of systems. Another advantage of our approach is its easy implementationand graphical representation, which we illustrate on a simple program.},
journal = {Computing and Informatics},
pages = {--},
isbn_issn = {ISSN 1335-9150},
year = {2019},
note = {To appear},
refereed = {yes},
length = {28}
}
[Schreiner]

Applying Statistical Model Checking to the Analysis of a Retrial Queueing System with Constant Time Impatience

Wolfgang Schreiner, János Sztrik

Technical report no. 00-00 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. September 2019. [pdf]
[bib]
@techreport{RISC5986,
author = {Wolfgang Schreiner and János Sztrik},
title = {{Applying Statistical Model Checking to the Analysis of a Retrial Queueing System with Constant Time Impatience}},
language = {english},
abstract = {We report on experiments with the automated analysis of a finite-source queueing systemwith an unreliable server where clients abort unserved requests after some maximum (con-stant) amount of time. In earlier work, we created a CTMC model of this system where theconstant time bound was approximated by an Erlang distribution and analyzed this modelwith the probabilistic model checker PRISM. However, due to state space explosion onlyinstances of the system with a very small number of clients could be analyzed. In this paper,we extend the results to larger systems by applying the statistical model checking capabilitiesof PRISM where results are approximated by sampling a large number of simulation runs.In particular, we address the change from the analysis of the steady state behavior of thesystem to the analysis of finite runs of the system and the trade-off between the accuracy ofthe results and the computational efforts needed to derive them.},
number = {00-00},
year = {2019},
month = {September},
keywords = {performance modeling, formal methods, probabilistic model checking},
sponsor = {Supported by the Aktion Österreich-Ungarn project 101öu7.},
length = {11},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

2018

[Amiridze]

Anti-Unification and Natural Language Processing

N. Amiridze, T. Kutsia

In: Fifth Workshop on Natural Language and Computer Science, NLCS’18, A. Asudeh, V. de Paiva, L. Moss (ed.), EasyChair preprints 203, pp. 1-12. 2018. [url] [pdf]
[bib]
@inproceedings{RISC5707,
author = {N. Amiridze and T. Kutsia},
title = {{Anti-Unification and Natural Language Processing}},
booktitle = {{Fifth Workshop on Natural Language and Computer Science, NLCS’18}},
language = {english},
series = {EasyChair preprints},
number = {203},
pages = {1--12},
isbn_issn = { },
year = {2018},
editor = {A. Asudeh and V. de Paiva and L. Moss},
refereed = {yes},
length = {12},
url = {https://doi.org/10.29007/fkrh}
}

Loading…