# 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

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

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

#### David M. Cerna

In: T.B.D, , Proceedings of T.B.D, pp. 1-17. 2019. T.B.D. [pdf]
@inproceedings{RISC5841,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
booktitle = {{T.B.D}},
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.},
pages = {1--17},
isbn_issn = {T.B.D},
year = {2019},
editor = {T.B.D},
refereed = {yes},
length = {17},
conferencename = {T.B.D}
}

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

### A Generic Framework for Higher-Order Generalizations

#### David M. Cerna, Temur Kutsia

Technical report no. 19-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
@techreport{RISC5883,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
language = {english},
number = {19-01},
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}
}

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

### First Order: The Game

#### David M. Cerna

2019. [pdf] [jar]
@techreport{RISC5887,
author = {David M. Cerna},
title = {{First Order: The Game}},
language = {english},
abstract = {A Manual for playing the Game in the Jar file. The game is based on implication based proof situations. This is a demo code for a much larger software project being developed},
year = {2019},
length = {11},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

### Anti-Unification and Natural Language Processing

#### N. Amiridze, T. Kutsia

In: Fifth Workshop on Natural Language and Computer Science, NLCS’18, , EasyChair preprints 203, pp. 1-12. 2018. [url] [pdf]
@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}
}

### Term-Graph Anti-Unification

#### Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

Technical report no. 18-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2018. [pdf]
@techreport{RISC5549,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
language = {english},
number = {18-02},
year = {2018},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

### Idempotent Anti-unification

#### David M. Cerna Temur Kutsia

RISC. Technical report, Feb. 2018. Submitted for review. [pdf]
@techreport{RISC5530,
author = {David M. Cerna Temur Kutsia},
title = {{Idempotent Anti-unification }},
language = {english},
abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},
year = {2018},
month = {Feb.},
note = {Submitted for review},
institution = {RISC},
length = {27}
}

### Primitive Recursive Proof Systems for Arithmetic

#### David M. Cerna

RISC. Technical report, January 2018. In revision. [pdf]
@techreport{RISC5528,
author = {David M. Cerna},
title = {{Primitive Recursive Proof Systems for Arithmetic}},
language = {english},
abstract = {Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extensionof the LK-calculus with equality and an additional inference rule formalizing induction.While this formalism was enough (with the addition of some meta-theoretic argumentation)to show the consistency of arithmetic, alternative formulations of induction such asthe infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmeticproofs obfuscated by the inference rule formulation of induction. For example, questionsconcerning the elimination of cut, consistency, and proof shape are given more clarity. Thesame could be said for functional interpretations of arithmetic such as system T whichenumerates the recursive functions provably total by arithmetic. A key feature of thesevariations on the formalization of arithmetic is that they get somewhat closer to formalizingthe concept of induction directly using the inferences of the LK-calculus, albeit byadding extra machinery at the meta-level. In this work we present a recursive sequentcalculus for arithmetic which can be syntactically translated into Gentzen formalism ofarithmetic and allows proof normalization to the LK-calculus with equality.},
year = {2018},
month = {January },
note = {In revision},
institution = {RISC},
length = {20}
}

### Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques

#### Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

Journal of Symbolic Computation 90, pp. 3-41. 2018. Elsevier, 07477171. [url]
@article{RISC5715,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {90},
pages = {3--41},
publisher = {Elsevier},
isbn_issn = {07477171},
year = {2018},
refereed = {yes},
keywords = {algorithm synthesis ; automated reasoning ; natural--style proving},
length = {39},
url = {https://doi.org/10.1016/j.jsc.2018.04.002}
}

### Pattern-based calculi with finitary matching

#### Sandra Alves, Besik Dundua, Mário Florido, Temur Kutsia

Logic Journal of the IGPL 26(2), pp. 203-243. 2018. ISSN 1367-0751. [url]
@article{RISC5763,
author = {Sandra Alves and Besik Dundua and Mário Florido and Temur Kutsia},
title = {{Pattern-based calculi with finitary matching}},
language = {english},
journal = {Logic Journal of the IGPL},
volume = {26},
number = {2},
pages = {203--243},
isbn_issn = {ISSN 1367-0751},
year = {2018},
refereed = {yes},
length = {41},
url = {https://doi.org/10.1093/JIGPAL/jzx059}
}

### Experiments with Automatic Proofs in Elementary Analysis

#### T. Jebelean

Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2018. Work in progress. [pdf] [zip] [pdf]
@techreport{RISC5692,
author = {T. Jebelean},
title = {{Experiments with Automatic Proofs in Elementary Analysis}},
language = {english},
abstract = {Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non--clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms.We demonstrate on some concrete examples several heuristic techniques for the automation of natural--style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra.Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions.These techniques are being implemented in the {\em Theorema} system and are able to construct automatically natural--style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.},
number = {18-06},
year = {2018},
month = {April},
keywords = {Satisfiability Checking, Natural-style Proofs, Symbolic Computation},
sponsor = {European project Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},
length = {33},
type = {Work in progress},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

### Idempotent Generalization is Infinitary

#### David M. Cerna and Temur Kutsia

RISC. Technical report, RISC Report, 2018. [pdf]
@techreport{RISC5529,
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Generalization is Infinitary}},
language = {english},
abstract = {Let §\mathbf{I}_{S}$be an equational theory s.t. for each$f\in S$,$f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP)$f(a,b) \triangleq g(a,b)$modulo$\mathbf{I}_{\lbrace f,g \rbrace}$admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo$\mathbf{I}_{\lbrace f\rbrace}$,$f(a,f(a,b)) \triangleq f(b,f(a,b))\$ admits infinitely many lggs.},
year = {2018},
howpublished = {RISC Report},
institution = {RISC},
length = {1}
}

### Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL

#### A. Maletzky, F. Immler

In: Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17), , Proceedings of CICM 2018, Lecture Notes in Computer Science 11006, pp. 178-193. 2018. Springer, ISBN 978-3-319-96811-7. The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16. [url]
@inproceedings{RISC5733,
author = {A. Maletzky and F. Immler},
title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL}},
booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17)}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11006},
pages = {178--193},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-96811-7},
year = {2018},
note = {The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16},
editor = {Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef},
refereed = {yes},
length = {16},
conferencename = {CICM 2018},
url = {https://doi.org/10.1007/978-3-319-96812-4_16}
}

### Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)

#### A. Maletzky, F. Immler

RISC, JKU Linz. Technical report, May 2018. arXiv:1805.00304 [cs.LO]. [url]
@techreport{RISC5734,
author = {A. Maletzky and F. Immler},
title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)}},
language = {english},
year = {2018},
month = {May},
note = {arXiv:1805.00304 [cs.LO]},
institution = {RISC, JKU Linz},
length = {28},
url = {https://arxiv.org/abs/1805.00304}
}

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

#### A. Maletzky

RISC. Technical report, December 2018. [pdf]
@techreport{RISC5814,
author = {A. Maletzky},
title = {{Gröbner Bases and Macaulay Matrices in Isabelle/HOL}},
language = {english},
year = {2018},
month = {December},
institution = {RISC},
length = {15}
}

### A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms

#### A. Maletzky

RISC. Technical report, September 2018. Submitted. [pdf]
@techreport{RISC5815,
author = {A. Maletzky},
title = {{A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms}},
language = {english},
year = {2018},
month = {September},
note = {Submitted},
institution = {RISC},
length = {31}
}

### Proximity-Based Generalization

#### Temur Kutsia, Cleo Pau

In: 32nd International Workshop on Unification, UNIF 2018, , pp. - . 2018. [pdf]
@inproceedings{RISC5713,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Generalization}},
booktitle = {{32nd International Workshop on Unification, UNIF 2018}},
language = {english},
pages = { -- },
isbn_issn = { },
year = {2018},
editor = {Mauricio Ayala-Rincon and Philippe Balbiani},
refereed = {yes},
length = {0}
}

### WebEx: Web Exercises for RISCAL

#### Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October 2018. [pdf]
@techreport{RISC5793,
author = {Wolfgang Schreiner},
title = {{WebEx: Web Exercises for RISCAL}},
language = {english},
abstract = {We report on a software framework "WebEx" for developing web-basedstudent exercises whose correctness is checked with the help of the RISCAL (RISCAlgorithm Language) software. This framework allows to generate from anappropriately annotated RISCAL specification file an HTML file that serves asthe frontend to a remote execution service. Student input (RISCAL fragments) aretransmitted to this execution service which generates from the annotatedspecification file and the input a plain RISCAL specification on which RISCAL isinvoked (in a non-interactive mode); the success status of the execution and theproduced output are reported back to the web interface. For each successfulexercise the server produces a digitally signed certificate that is returned tothe user who may submit this certificate as a proof of successful completion ofthe exercise (which may be subsequently automatically checked). Furthermore eachannotated RISCAL specification may serve as a template that may be instantiatedwith other data to produce a set of exercise instances. The WebEx software ismostly independent of RISCAL; it may be also used to provide a web front end forother scientific software of a similar nature.},
year = {2018},
month = {October},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, logic, computer-supported education},
sponsor = {Austrian OEAD WTZ program and the Slovak SRDA agency contract SK 14/2018 SemTech and Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU},
length = {35}
}

### Unranked Second-Order Anti-Unification

#### Alexander Baumgartner, Temur Kutsia

Information and Computation 255(2), pp. 262-286. 2017. ISSN: 0890-5401. [url]
@article{RISC5192,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Unranked Second-Order Anti-Unification}},
language = {english},
journal = {Information and Computation},
volume = {255},
number = {2},
pages = {262--286},
isbn_issn = {ISSN: 0890-5401},
year = {2017},
refereed = {yes},
length = {25},
url = {http://doi.org/10.1016/j.ic.2017.01.005}
}