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

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