## Ongoing Projects

### Logic Technology for Computer Science Education [LOGTECHEDU]

### Combinatorics and Codes for Information Security [SBA-K1]

## Software

LogicGuard is a stream monitor specification language and system. ...

MiniMaple is a software for formal specification and verification of Maple programs. ...

The RISC ProgramExplorer is a computer-supported program reasoning environment for a simple imperative programming language "MiniJava"; it incorporates the RISC ProofNavigator as a semi-automatic proving assistant. The environment has been developed mainly for educational purposes (see this paper for a ...

The RISC ProofNavigator is an interactive proof assistant for supporting formal reasoning about computer programs and computing systems, see the README file and this short paper for the main ideas; it is the core reasoning component of the RISC ProgramExplorer. ...

### RISCAL

#### The RISC Algorithm Language: A Language and Associated Software System for Specifying and Verifying Mathematical Algorithms

The RISC Algorithm Language (RISCAL) is a specification language and associated software system for describing mathematical algorithms, formally specifying their behavior based on mathematical theories, and validating the correctness of algorithms, specifications, and theories by execution/evaluation. The software has been ...

## Publications

### 2020

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

}

### 2019

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

}

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

}

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

}

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

}

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

}

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

}

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

}

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

}

### On the Probabilistic Model Checking of a Retrial Queueing System with Unreliable Server, Collision, and Constant Time Impatience

#### Wolfgang Schreiner, János Sztrik

Technical report no. 19-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. July 2019. [pdf]**techreport**{RISC5984,

author = {Wolfgang Schreiner and János Sztrik},

title = {{On the Probabilistic Model Checking of a Retrial Queueing System with Unreliable Server, Collision, and Constant Time Impatience}},

language = {english},

abstract = {We report on initial experiments with the automated analysis of a finite-source queueingsystem with an unreliable server and collisions of service requests that cause clients to bemoved to an orbit until they can be served. However, clients remain in the obit only forsome maximum amount of time before they run out of patience and unsuccessfully aborttheir service request. In contrast to earlier investigations, the duration of their patience isnot exponentially distributed but constrained by a constant time bound, which imposes aproblem for both their manual and automatic analysis. In this paper we address how suchsystems can be nevertheless approximately analyzed to a certain extent with the help of theprobabilistic model checker PRISM.},

number = {19-11},

year = {2019},

month = {July},

keywords = {formal methods, model checking, performance analysis},

sponsor = {Supported by the Austrian-Hungarian Bilateral Cooperation in Science and Technology project 2017-2.2.4-TeT- AT-2017-00010 and the Aktion Österreich-Ungarn project 101öu7.},

length = {21},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

}

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

}

### Logic and Semantic Technologies for Computer Science Education

#### Wolfgang Schreiner

In: Informatics’2019, 2019 IEEE 15th International Scientific Conference on Informatics, Poprad, Slovakia, November 20–22, William Steingartner, Štefan Korecko, Anikó Szakál (ed.), pp. 7-12. 2019. IEEE, ISBN 978-1-7281-3178-8. invited paper.**inproceedings**{RISC5957,

author = {Wolfgang Schreiner},

title = {{Logic and Semantic Technologies for Computer Science Education}},

booktitle = {{Informatics’2019, 2019 IEEE 15th International Scientific Conference on Informatics, Poprad, Slovakia, November 20–22}},

language = {english},

abstract = {We report on some projects to develop software rooted in formal logic andsemantics in order to enhance education in computer science and mathematics.The goal is to let students actively engage with the course material bysolving concrete problems where the correctness of a solution isautomatically checked; furthermore, if a solution is not correct or thestudent gets stuck, the software shall provide additional insight and hintsthat aid the student towards the desired result. In particular, we describeour experience with the RISCAL software, a model checker for mathematicaltheories and algorithms, in university courses on logic, formal methods, andformal modeling.},

pages = {7--12},

publisher = {IEEE},

isbn_issn = {ISBN 978-1-7281-3178-8},

year = {2019},

note = {invited paper},

editor = {William Steingartner and Štefan Korecko and Anikó Szakál},

refereed = {no},

keywords = {logic, semantics, formal verification, model checking, reasoning about programs, computer science education},

length = {6}

}

### A Coalgebraic Operational Semantics for an Imperative Language

#### William Steingartner, Valerie Novitzká, Wolfgang Schreiner

Computing and Informatics, pp. -. 2019. ISSN 1335-9150. To appear.**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}

}

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

#### Wolfgang Schreiner, János Sztrik

Technical report no. 19-12 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. September 2019. [pdf]**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 = {19-12},

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}

}

### McCarthy-Kleene fuzzy automata and MSO logics

#### Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner

Information and Computation, pp. -. 2019. Elsevier, ISSN 0890-5401. In Press. [url]**article**{RISC6011,

author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},

title = {{McCarthy-Kleene fuzzy automata and MSO logics}},

language = {english},

abstract = {We introduce McCarthy-Kleene fuzzy automata (MK-fuzzy automata) over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Büchi type theorem.},

journal = {Information and Computation},

pages = {--},

publisher = {Elsevier},

isbn_issn = {ISSN 0890-5401},

year = {2019},

note = {In Press},

refereed = {yes},

keywords = {Bimonoids, McCarthy-Kleene logic, MK-fuzzy automata, MK-fuzzy MSO logic},

sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 “LogicGuard II”},

length = {23},

url = {https://doi.org/10.1016/j.ic.2019.104499}

}

### A Parallel, In-Place, Rectangular Matrix Transpose Algorithm

#### Stefan Amberger

Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. March 2019. [pdf]**misc**{RISC5916,

author = {Stefan Amberger},

title = {{A Parallel, In-Place, Rectangular Matrix Transpose Algorithm}},

language = {english},

abstract = {This thesis presents a novel algorithm for Transposing Rectangular matrices In-place and in Parallel(TRIP) including a proof of correctness and an analysis of work, span and parallelism.After almost 60 years since its introduction, the problem of in-place rectangular matrix transpositionstill does not have a satisfying solution. Increased concurrency in today's computers, and the need for low overhead algorithms to solve memory-intense challenges are motivating the development of algorithmslike TRIP. The algorithm is based on recursive splitting of the matrix into sub-matrices, independent, paralleltransposition of these sub-matrices, and subsequent combining of the results by a parallel, perfect shuffle.We prove correctness of the algorithm for different matrix shapes (ratios of dimensions), and analyzework and span . Compared to out-of-place algorithms, TRIP, implemented in Cilk, trades work-efficiency for parallelism and for being in-place.},

year = {2019},

month = {March},

translation = {0},

institution = {Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria},

keywords = {linear algebra, parallel computation},

length = {67}

}

### Migrating Mathematical Programs to Web Interface Frameworks

#### Hsuan-Ming Chen

Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis. April 2019. Internationaler Universitätslehrgang: Informatics: Engineering & Management. [pdf]**misc**{RISC5917,

author = {Hsuan-Ming Chen},

title = {{Migrating Mathematical Programs to Web Interface Frameworks}},

language = {english},

abstract = {A mathematical software system, the RISC Algorithm Language (RISCAL), has beenimplemented in Java; however, it can be only executed on the local machine of the user.The aim of this master thesis is to migrate RISCAL to the web, such that users can accessthe software via a conventional web browser without needing a local installation of thesoftware. In a preparatory phase, this thesis evaluates various web interface frameworksand how these can be executed on the web. Based in the result of this investigation whichcompares the advantages and disadvantages of the frameworks, one framework is selectedas the most promising candidate for future work. The core of the thesis is then themigration of RISCAL to the web on the basis of this framework and the subsequentevaluation of how the demands have been met and how well all of the RISCAL programsare working after the migration.},

year = {2019},

month = {April},

note = {Internationaler Universitätslehrgang: Informatics: Engineering & Management},

translation = {0},

institution = {Research Institute for Symbolic Computatation (RISC), Johannes Kepler University, Linz, Austria},

length = {85}

}

### 2018

### Idempotent Anti-unification

#### David M. Cerna, Temur Kutsia

RISC. Technical report, Feb. 2018. to appear in TOCL. [pdf]**techreport**{RISC5530,

author = {David M. Cerna and 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 = {to appear in TOCL},

institution = {RISC},

length = {32}

}

### Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models

#### Wolfgang Schreiner, Alexander Brunhuemer, Christoph Fürst

In: Post-Proceedings ThEdu'17, Pedro Quaresma and Walther Neuper (ed.), Proceedings of 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science (EPTCS) 267, pp. 120-139. 2018. Open Publishing Association, ISSN 2075-2180. [url] [pdf]**inproceedings**{RISC5531,

author = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph Fürst},

title = {{Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models}},

booktitle = {{Post-Proceedings ThEdu'17}},

language = {english},

abstract = {Education in the practical applications of logic and proving such as the formalspecification and verification of computer programs is substantially hampered bythe fact that most time and effort that is invested in proving is actuallywasted in vain: because of errors in the specifications respectively algorithmsthat students have developed, their proof attempts are often pointless (becausethe proposition proved is actually not of interest) or a priori doomed to fail(because the proposition to be proved does actually not hold); this is afrequent source of frustration and gives formal methods a bad reputation. RISCAL(RISC Algorithm Language) is a formal specification language and associatedsoftware system that attempts to overcome this problem by making logicformalization fun rather than a burden. To this end, RISCAL allows students toeasily validate the correctness of instances of propositions respectivelyalgorithms by automatically evaluating/executing and checking them on (small)finite models. Thus many/most errors can be quickly detected and subsequentproof attempts can be focused on propositions that are more/most likely to beboth meaningful and true.},

series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},

volume = {267},

pages = {120--139},

publisher = {Open Publishing Association},

isbn_issn = {ISSN 2075-2180},

year = {2018},

editor = {Pedro Quaresma and Walther Neuper},

refereed = {yes},

keywords = {formal methods, program specification and verification, model checking, computer science education, logic},

sponsor = {Supported by the Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU "Logic Technology for Computer Science Education"},

length = {20},

conferencename = {6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017},

url = {http://dx.doi.org/10.4204/EPTCS.267.8}

}