Ongoing Projects
Integration of Symbolic and Subsymbolic AI for Industry [InProSSA]
Project Lead: Wolfgang Schreiner
Software
LogicGuard is a stream monitor specification language and system. ...
Authors: Wolfgang Schreiner
MoreSoftware WebsiteMiniMaple is a software for formal specification and verification of Maple programs. ...
Authors: Wolfgang Schreiner, Muhammad Taimoor Khan
MoreThe 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 ...
Authors: Wolfgang Schreiner
MoreSoftware WebsiteThe 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. ...
Authors: Wolfgang Schreiner
MoreSoftware WebsiteRISCAL
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 ...
Authors: Wolfgang Schreiner
MoreSoftware WebsitePublications
2027
[Schreiner]
A Visualization Framework for Semantics of a Concatenative Compositional Language
William Steingartner, Martin Mormák, Wolfgang Schreiner
In: New Trends in Database and Information Systems, Genoveva Vargas Solar, Kostas Stefanidis, Themis Palpanas, Patrick Marcel, Mirian Halfeld-Ferrari, Panos Vassiliadis, Tatjana Welzer, Enrico Gallinucci, Veronika Peralta (ed.), Proceedings of ADBIS 2026: European Conference on Advances in Databases and Information Systems, Orléans, France, September 28 – October 1, 2026, Communications in Computer and Information Science 3175, pp. 332-347. 2027. Springer, Cham, ISBN 978-3-032-39822-2. [doi]@inproceedings{RISC7279,
author = {William Steingartner and Martin Mormák and Wolfgang Schreiner},
title = {{A Visualization Framework for Semantics of a Concatenative Compositional Language}},
booktitle = {{New Trends in Database and Information Systems}},
language = {english},
abstract = {Concatenative programming languages represent an interesting learning environment for teaching formal semantics, stack-based computations, and higher-order programming constructs. However, students often have difficulty understanding the relationship between formal semantic rules and concrete program execution because intermediate states of computation are not directly observable.This paper presents a visualization framework for the KKJ language based on executable semantics. Semantic rules specified in the SLANG language generate execution traces consisting of successive program configurations that are subsequently visualized. The proposed approach transforms formal semantic specifications into observable execution behavior and allows users to observe the evolution of the stack, quotations, and higher-order operations during program execution. The resulting framework establishes a link between formal semantics, executable semantics, and program visualization, thereby supporting the conceptual understanding of stack-based and higher-order computations in concatenative languages. Unlike existing visualization tools, the proposed framework visualizes semantic transitions directly derived from executable semantic specifications, rather than from implementation-level execution.},
series = {Communications in Computer and Information Science},
volume = {3175},
pages = {332--347},
publisher = {Springer},
address = {Cham},
isbn_issn = {ISBN 978-3-032-39822-2},
year = {2027},
editor = {Genoveva Vargas Solar and Kostas Stefanidis and Themis Palpanas and Patrick Marcel and Mirian Halfeld-Ferrari and Panos Vassiliadis and Tatjana Welzer and Enrico Gallinucci and Veronika Peralta},
refereed = {yes},
keywords = {computer science education, concatenative languages, executable semantics, execution trace, formal semantics, program visualization, stack-based computation},
sponsor = {KEGA project 028TUKE-4/2026 – “Innovative approaches to teaching and researching formal methods in the context of modern software engineering”},
length = {16},
conferencename = {ADBIS 2026: European Conference on Advances in Databases and Information Systems, Orléans, France, September 28 – October 1, 2026},
url = {https://doi.org/10.1007/978-3-032-39823-9_31}
}
author = {William Steingartner and Martin Mormák and Wolfgang Schreiner},
title = {{A Visualization Framework for Semantics of a Concatenative Compositional Language}},
booktitle = {{New Trends in Database and Information Systems}},
language = {english},
abstract = {Concatenative programming languages represent an interesting learning environment for teaching formal semantics, stack-based computations, and higher-order programming constructs. However, students often have difficulty understanding the relationship between formal semantic rules and concrete program execution because intermediate states of computation are not directly observable.This paper presents a visualization framework for the KKJ language based on executable semantics. Semantic rules specified in the SLANG language generate execution traces consisting of successive program configurations that are subsequently visualized. The proposed approach transforms formal semantic specifications into observable execution behavior and allows users to observe the evolution of the stack, quotations, and higher-order operations during program execution. The resulting framework establishes a link between formal semantics, executable semantics, and program visualization, thereby supporting the conceptual understanding of stack-based and higher-order computations in concatenative languages. Unlike existing visualization tools, the proposed framework visualizes semantic transitions directly derived from executable semantic specifications, rather than from implementation-level execution.},
series = {Communications in Computer and Information Science},
volume = {3175},
pages = {332--347},
publisher = {Springer},
address = {Cham},
isbn_issn = {ISBN 978-3-032-39822-2},
year = {2027},
editor = {Genoveva Vargas Solar and Kostas Stefanidis and Themis Palpanas and Patrick Marcel and Mirian Halfeld-Ferrari and Panos Vassiliadis and Tatjana Welzer and Enrico Gallinucci and Veronika Peralta},
refereed = {yes},
keywords = {computer science education, concatenative languages, executable semantics, execution trace, formal semantics, program visualization, stack-based computation},
sponsor = {KEGA project 028TUKE-4/2026 – “Innovative approaches to teaching and researching formal methods in the context of modern software engineering”},
length = {16},
conferencename = {ADBIS 2026: European Conference on Advances in Databases and Information Systems, Orléans, France, September 28 – October 1, 2026},
url = {https://doi.org/10.1007/978-3-032-39823-9_31}
}
2026
[Baumgartner]
Quantitative Generalization for Variadic Nominal Terms
Alexander Baumgartner, Temur Kutsia
In: Proceedings of the 40th International Workshop on Unification (UNIF 2026), Silvio Ghilardi and Cleo Pau (ed.), RISC Report Series 26-10, pp. 24-31. 2026. RISC, Johannes Kepler University Linz, ISSN: 2791-4267. [doi]@inproceedings{RISC7268,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Quantitative Generalization for Variadic Nominal Terms}},
booktitle = {{Proceedings of the 40th International Workshop on Unification (UNIF 2026)}},
language = {english},
series = {RISC Report Series},
volume = {26-10},
pages = {24--31},
publisher = {RISC, Johannes Kepler University Linz},
isbn_issn = {ISSN: 2791-4267},
year = {2026},
editor = {Silvio Ghilardi and Cleo Pau},
refereed = {yes},
length = {8},
url = {https://doi.org/10.35011/risc.26-10}
}
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Quantitative Generalization for Variadic Nominal Terms}},
booktitle = {{Proceedings of the 40th International Workshop on Unification (UNIF 2026)}},
language = {english},
series = {RISC Report Series},
volume = {26-10},
pages = {24--31},
publisher = {RISC, Johannes Kepler University Linz},
isbn_issn = {ISSN: 2791-4267},
year = {2026},
editor = {Silvio Ghilardi and Cleo Pau},
refereed = {yes},
length = {8},
url = {https://doi.org/10.35011/risc.26-10}
}
[Buchberger]
Nakano’s Light Puzzle: A Correctness Proof for a Greedy Algorithm
Bruno Buchberger
Technical report no. 26-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). RISC Report, May 2026. Licensed under CC BY 4.0 International. [doi] [pdf]@techreport{RISC7250,
author = {Bruno Buchberger},
title = {{Nakano’s Light Puzzle: A Correctness Proof for a Greedy Algorithm}},
language = {english},
abstract = {We consider Nakano’s Problem: Give a (simple and algorithmic) necessary and sufficient conditionfor a configuration of lights (on/off) in a cube to be transformable to the all-off configuration bycertain touches on the faces of the cube. In this paper, we provide a detailed correctness proof for a“greedy” algorithm for Nakano’s problem. With the same proof technique, we also get anotheralgorithmic criterion for Nakano’s problem, which is based on the notion of “parity of box sums”.We discuss the relevance of such proofs for the recent research on automating mathematicalinvention by a combination of Automated Reasoning techniques and Automated Search of Rele-vant Mathematical Literature through Machine Learning.},
number = {26-05},
year = {2026},
month = {May},
howpublished = {RISC Report},
keywords = {Nakano's problem, light puzzle problem, greedy algorithm, correctness proof, automated mathematical invention, canonical simplification, parity lemma, THEOREMA},
length = {58},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {Bruno Buchberger},
title = {{Nakano’s Light Puzzle: A Correctness Proof for a Greedy Algorithm}},
language = {english},
abstract = {We consider Nakano’s Problem: Give a (simple and algorithmic) necessary and sufficient conditionfor a configuration of lights (on/off) in a cube to be transformable to the all-off configuration bycertain touches on the faces of the cube. In this paper, we provide a detailed correctness proof for a“greedy” algorithm for Nakano’s problem. With the same proof technique, we also get anotheralgorithmic criterion for Nakano’s problem, which is based on the notion of “parity of box sums”.We discuss the relevance of such proofs for the recent research on automating mathematicalinvention by a combination of Automated Reasoning techniques and Automated Search of Rele-vant Mathematical Literature through Machine Learning.},
number = {26-05},
year = {2026},
month = {May},
howpublished = {RISC Report},
keywords = {Nakano's problem, light puzzle problem, greedy algorithm, correctness proof, automated mathematical invention, canonical simplification, parity lemma, THEOREMA},
length = {58},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Cerna]
On Completeness of Absorptive Anti-Unification
Marcos Mercandeli-Rodrigues, Andrés Felipe González Barragan, David M. Cerna, Temur Kutsia and Mauricio Ayala-Rincón
In: Proceedings of the 40th International Workshop on Unification (UNIF 2026), Silvio Ghilardi and Cleo Pau (ed.), RISC Report Series 26-10, pp. 55-62. 2026. RISC, Johannes Kepler University Linz, ISSN: 2791-4267. [doi]@inproceedings{RISC7267,
author = {Marcos Mercandeli-Rodrigues and Andrés Felipe González Barragan and David M. Cerna and Temur Kutsia and Mauricio Ayala-Rincón},
title = {{On Completeness of Absorptive Anti-Unification}},
booktitle = {{Proceedings of the 40th International Workshop on Unification (UNIF 2026)}},
language = {english},
series = {RISC Report Series},
volume = {26-10},
pages = {55--62},
publisher = {RISC, Johannes Kepler University Linz},
isbn_issn = {ISSN: 2791-4267},
year = {2026},
editor = {Silvio Ghilardi and Cleo Pau},
refereed = {yes},
length = {8},
url = {https://doi.org/10.35011/risc.26-10}
}
author = {Marcos Mercandeli-Rodrigues and Andrés Felipe González Barragan and David M. Cerna and Temur Kutsia and Mauricio Ayala-Rincón},
title = {{On Completeness of Absorptive Anti-Unification}},
booktitle = {{Proceedings of the 40th International Workshop on Unification (UNIF 2026)}},
language = {english},
series = {RISC Report Series},
volume = {26-10},
pages = {55--62},
publisher = {RISC, Johannes Kepler University Linz},
isbn_issn = {ISSN: 2791-4267},
year = {2026},
editor = {Silvio Ghilardi and Cleo Pau},
refereed = {yes},
length = {8},
url = {https://doi.org/10.35011/risc.26-10}
}
[Schreiner]
Building a Logical Agent with LangChain ... and Quite Some Vibe Coding
Wolfgang Schreiner
Technical report no. 26-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). March 2026. Licensed under CC BY 4.0 International. [doi] [pdf]@techreport{RISC7237,
author = {Wolfgang Schreiner},
title = {{Building a Logical Agent with LangChain ... and Quite Some Vibe Coding}},
language = {english},
abstract = {This document reports on our experience of building an “agentic AI” (Artificial Intelligence) that helps a human to answer logical questions in a trustworthy way. This agent combines a Large Language Model (LLM) (which interacts with the human in natural language) with a logical software (which automatically proves formal theorems). The LLM engages in a dialogue with the human in order to translate their logical question from natural language to a formal proof problem. Once the human is satisfied with the formalization, the LLM invokes the prover to automatically solve the problem and thus answer the question; then the LLM also offers the user the possibility to inspect the successful proof or the unsuccessful proof attempt by calling the prover in an interactive mode. Furthermore, we describe how much of the source code (which is based on on the agent construction framework LangChain) has been “vibe coded”, i.e., itself generated with the help of an LLM.},
number = {26-02},
year = {2026},
month = {March},
keywords = {large language models, automated theorem proving, agentic AI, logical formalization, vibe coding},
length = {73},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {Wolfgang Schreiner},
title = {{Building a Logical Agent with LangChain ... and Quite Some Vibe Coding}},
language = {english},
abstract = {This document reports on our experience of building an “agentic AI” (Artificial Intelligence) that helps a human to answer logical questions in a trustworthy way. This agent combines a Large Language Model (LLM) (which interacts with the human in natural language) with a logical software (which automatically proves formal theorems). The LLM engages in a dialogue with the human in order to translate their logical question from natural language to a formal proof problem. Once the human is satisfied with the formalization, the LLM invokes the prover to automatically solve the problem and thus answer the question; then the LLM also offers the user the possibility to inspect the successful proof or the unsuccessful proof attempt by calling the prover in an interactive mode. Furthermore, we describe how much of the source code (which is based on on the agent construction framework LangChain) has been “vibe coded”, i.e., itself generated with the help of an LLM.},
number = {26-02},
year = {2026},
month = {March},
keywords = {large language models, automated theorem proving, agentic AI, logical formalization, vibe coding},
length = {73},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Schreiner]
An Intermediate Representation Format for Industrial Optimization Problems - The Translation of OptDSL to MiniZinc
Tereso del Río, Wolfgang Schreiner, Martina Seidl, Temur Kutsia, Wolfgang Windsteiger
Technical report no. 26-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2026. Licensed under CC BY 4.0 International. [doi] [pdf]@techreport{RISC7239,
author = {Tereso del Río and Wolfgang Schreiner and Martina Seidl and Temur Kutsia and Wolfgang Windsteiger },
title = {{An Intermediate Representation Format for Industrial Optimization Problems - The Translation of OptDSL to MiniZinc}},
language = {english},
abstract = {This report presents the implementation of OptDSL, a Python-inspired domain-specific language for describing optimisation problems. The implementation is based on the translationof a high-level OptDSL formulation of the problem to an intermediate representation in the constraint modelling language MiniZinc, which can be used by multiple state-of-the-art solvers. The report also describes the translation software, illustrates its use on a simplified industrial example, discusses selected implementation details, and suggests directions for further development.},
number = {26-04},
year = {2026},
month = {April},
keywords = {industrial optimization, domain-specific languages, constraint solving, formal languages, translation},
sponsor = {Supported by the FFG project FO999923579 “InProSSA: Industrial Problem Solving Using Symbolic and Subsymbolic AI”},
length = {88},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {Tereso del Río and Wolfgang Schreiner and Martina Seidl and Temur Kutsia and Wolfgang Windsteiger },
title = {{An Intermediate Representation Format for Industrial Optimization Problems - The Translation of OptDSL to MiniZinc}},
language = {english},
abstract = {This report presents the implementation of OptDSL, a Python-inspired domain-specific language for describing optimisation problems. The implementation is based on the translationof a high-level OptDSL formulation of the problem to an intermediate representation in the constraint modelling language MiniZinc, which can be used by multiple state-of-the-art solvers. The report also describes the translation software, illustrates its use on a simplified industrial example, discusses selected implementation details, and suggests directions for further development.},
number = {26-04},
year = {2026},
month = {April},
keywords = {industrial optimization, domain-specific languages, constraint solving, formal languages, translation},
sponsor = {Supported by the FFG project FO999923579 “InProSSA: Industrial Problem Solving Using Symbolic and Subsymbolic AI”},
length = {88},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Schreiner]
On the Rapid Prototyping of a Logical Agent
Wolfgang Schreiner
In: SCML-2026: International Conference on Symbolic Computation and Machine Learning - Extended Abstracts, Bruno Buchberger, François Charton, Matthew England, Cezary Kaliszyk, Manuel Kauers, Hiroshi Kera, Temur Kutsia, Bernhard Moser, Markus Schedl, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteiger (ed.), RISC Proceedings on Symbolic Computation and Machine Learning 3, pp. 78-79. 2026. SCML, https://scml.risc.jku.at/, ISSN XXXX. [doi]@inproceedings{RISC7244,
author = {Wolfgang Schreiner},
title = {{On the Rapid Prototyping of a Logical Agent}},
booktitle = {{SCML-2026: International Conference on Symbolic Computation and Machine Learning - Extended Abstracts}},
language = {english},
abstract = {We report on our experience with the rapid prototyping of an “agentic AI” that helps a human to answer logical questions in a trustworthy way. This agent combines a Large Language Model (LLM) (which interacts with the human in natural language) with a logical software (which automatically proves formal theorems). The LLM engages in a dialogue with the human in order to translate their logical question from natural language to a formal proof problem. Once the human is satisfied with the formalization, the LLM invokes the prover to automatically solve the problem and thus answer the question; then the LLM also offers the user the possibility to inspect the successful proof or the unsuccessful proof attempt by calling the prover in an interactive mode. Furthermore, we describe how much of the source code (which is based on on the agent construction framework LangChain) has been “vibe coded”, i.e., itself generated with the help of an LLM.},
series = {RISC Proceedings on Symbolic Computation and Machine Learning},
number = {3},
pages = {78--79},
publisher = {SCML},
address = {https://scml.risc.jku.at/},
isbn_issn = {ISSN XXXX},
year = {2026},
editor = {Bruno Buchberger and François Charton and Matthew England and Cezary Kaliszyk and Manuel Kauers and Hiroshi Kera and Temur Kutsia and Bernhard Moser and Markus Schedl and Wolfgang Schreiner and Martina Seidl and Wolfgang Windsteiger},
refereed = {no},
keywords = {large language models, automated theorem proving, agentic AI, logical formalization, vibe coding},
length = {2},
url = {https://www.doi.org/doi.org/10.35011/risc-proceedings-scml.3}
}
author = {Wolfgang Schreiner},
title = {{On the Rapid Prototyping of a Logical Agent}},
booktitle = {{SCML-2026: International Conference on Symbolic Computation and Machine Learning - Extended Abstracts}},
language = {english},
abstract = {We report on our experience with the rapid prototyping of an “agentic AI” that helps a human to answer logical questions in a trustworthy way. This agent combines a Large Language Model (LLM) (which interacts with the human in natural language) with a logical software (which automatically proves formal theorems). The LLM engages in a dialogue with the human in order to translate their logical question from natural language to a formal proof problem. Once the human is satisfied with the formalization, the LLM invokes the prover to automatically solve the problem and thus answer the question; then the LLM also offers the user the possibility to inspect the successful proof or the unsuccessful proof attempt by calling the prover in an interactive mode. Furthermore, we describe how much of the source code (which is based on on the agent construction framework LangChain) has been “vibe coded”, i.e., itself generated with the help of an LLM.},
series = {RISC Proceedings on Symbolic Computation and Machine Learning},
number = {3},
pages = {78--79},
publisher = {SCML},
address = {https://scml.risc.jku.at/},
isbn_issn = {ISSN XXXX},
year = {2026},
editor = {Bruno Buchberger and François Charton and Matthew England and Cezary Kaliszyk and Manuel Kauers and Hiroshi Kera and Temur Kutsia and Bernhard Moser and Markus Schedl and Wolfgang Schreiner and Martina Seidl and Wolfgang Windsteiger},
refereed = {no},
keywords = {large language models, automated theorem proving, agentic AI, logical formalization, vibe coding},
length = {2},
url = {https://www.doi.org/doi.org/10.35011/risc-proceedings-scml.3}
}
[STUDENT]
Formal Modelling of Channel- and Source-Coding Algorithms from Coding Theory
Thomas Michlmayr
Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Bachelor Thesis. September 2026. Also available as RISC Report 26-15. [doi] [pdf]@misc{RISC7277,
author = {Thomas Michlmayr},
title = {{Formal Modelling of Channel- and Source-Coding Algorithms from Coding Theory}},
language = {english},
abstract = {This bachelor’s thesis aims to mathematically specify and implement selected concepts and techniques from information theory in the language of the mathematical model checker RISCAL (RISC Algorithm Language). To this end, techniques from channel coding for the detection and correction of errors in transmitted digital messages, as well as techniques from source coding for data compression, are considered. The developed algorithms and their properties are formally specified and verified in RISCAL using finite data types. RISCAL enables the exhaustive verification of all possible input parameters and provides counterexamples if a specified property is violated. Using various channel- and source-coding techniques, this thesis demonstrates how concepts from coding theory can be formally modelled and verified in RISCAL.},
year = {2026},
month = {September},
note = {Also available as RISC Report 26-15},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal specification and verification, model checking, encoding, decoding, compression, decompression},
length = {93},
url = {https://doi.org/10.35011/risc.26-15}
}
author = {Thomas Michlmayr},
title = {{Formal Modelling of Channel- and Source-Coding Algorithms from Coding Theory}},
language = {english},
abstract = {This bachelor’s thesis aims to mathematically specify and implement selected concepts and techniques from information theory in the language of the mathematical model checker RISCAL (RISC Algorithm Language). To this end, techniques from channel coding for the detection and correction of errors in transmitted digital messages, as well as techniques from source coding for data compression, are considered. The developed algorithms and their properties are formally specified and verified in RISCAL using finite data types. RISCAL enables the exhaustive verification of all possible input parameters and provides counterexamples if a specified property is violated. Using various channel- and source-coding techniques, this thesis demonstrates how concepts from coding theory can be formally modelled and verified in RISCAL.},
year = {2026},
month = {September},
note = {Also available as RISC Report 26-15},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal specification and verification, model checking, encoding, decoding, compression, decompression},
length = {93},
url = {https://doi.org/10.35011/risc.26-15}
}
2025
[Baumgartner]
Equational Generalization Problems with Atom-Variables
Alexander Baumgartner, Temur Kutsia, Daniele Nantes-Sobrinho, Manfred Schmidt-Schauss
In: Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings, Valeria de Paiva and Peter Koepke (ed.), Lecture Notes in Computer Science 16136, pp. 133-151. 2025. Springer, ISBN 978-3-032-07020-3. [doi]@inproceedings{RISC7188,
author = {Alexander Baumgartner and Temur Kutsia and Daniele Nantes-Sobrinho and Manfred Schmidt-Schauss},
title = {{Equational Generalization Problems with Atom-Variables}},
booktitle = {{Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {16136},
pages = {133--151},
publisher = {Springer},
isbn_issn = {ISBN 978-3-032-07020-3},
year = {2025},
editor = {Valeria de Paiva and Peter Koepke},
refereed = {yes},
length = {19},
url = {https://doi.org/10.1007/978-3-032-07021-0_8}
}
author = {Alexander Baumgartner and Temur Kutsia and Daniele Nantes-Sobrinho and Manfred Schmidt-Schauss},
title = {{Equational Generalization Problems with Atom-Variables}},
booktitle = {{Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {16136},
pages = {133--151},
publisher = {Springer},
isbn_issn = {ISBN 978-3-032-07020-3},
year = {2025},
editor = {Valeria de Paiva and Peter Koepke},
refereed = {yes},
length = {19},
url = {https://doi.org/10.1007/978-3-032-07021-0_8}
}
[Baumgartner]
Quantitative generalization of variadic structures with binders
Alexander Baumgartner, Temur Kutsia
Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Technical report, 2025. [pdf]@techreport{RISC7231,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Quantitative generalization of variadic structures with binders}},
language = {english},
year = {2025},
institution = {Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria},
length = {25}
}
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Quantitative generalization of variadic structures with binders}},
language = {english},
year = {2025},
institution = {Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria},
length = {25}
}
[Cerna]
Combining Generalization Algorithms in Regular Collapse-Free Theories
Mauricio Ayala-Rincón, David Cerna, Temur Kutsia, Christophe Ringeissen
In: Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), Maribel Fernandez (ed.), LIPIcs - Leibniz International Proceedings in Informatics 337, pp. 7:1-7:18. 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, ISBN 978-3-95977-374-4. [doi]@inproceedings{RISC7156,
author = {Mauricio Ayala-Rincón and David Cerna and Temur Kutsia and Christophe Ringeissen},
title = {{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
booktitle = {{Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)}},
language = {english},
series = {LIPIcs - Leibniz International Proceedings in Informatics},
volume = {337},
pages = {7:1--7:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-374-4},
year = {2025},
editor = {Maribel Fernandez},
refereed = {yes},
length = {0},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2025.7}
}
author = {Mauricio Ayala-Rincón and David Cerna and Temur Kutsia and Christophe Ringeissen},
title = {{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
booktitle = {{Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)}},
language = {english},
series = {LIPIcs - Leibniz International Proceedings in Informatics},
volume = {337},
pages = {7:1--7:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-374-4},
year = {2025},
editor = {Maribel Fernandez},
refereed = {yes},
length = {0},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2025.7}
}
[Schreiner]
Semantics-Based Rapid Prototyping of a Subset of SQL
Wolfgang Schreiner, William Steingartner
Technical report no. 25-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). February 2025. Licensed under CC BY 4.0 International. [doi] [pdf]@techreport{RISC7136,
author = {Wolfgang Schreiner and William Steingartner},
title = {{Semantics-Based Rapid Prototyping of a Subset of SQL}},
language = {english},
abstract = {This report documents the application of our semantics-based language generator SLANG to developing a rapid prototype of a non-trivial domain-specific language, a substantial subset of the Structured Query Language SQL that we have named SubSQL. After developing a mathematical/logical formulation of the language’s abstract syntax, formal type system, and denotational semantics, we have translated this formulation into a SLANG specification from which the SLANG software generates Java code that implements a parser, a printer, a type-checker, and an executor of the language. This implementation is based on several manually created Java classes that implement the mathematical domains and operations used in the formalization, a simple persistent database, and a high-level application programming interface that allows to execute complete SubSQL scripts from file or individual SubSQL commands within Java programs. The results represent a blueprint for the semantics-based development of other domain-specific languages of similar complexity.},
number = {25-02},
year = {2025},
month = {February},
keywords = {formal semantics of programming languages, domain specific languages, rapid prototyping, interpreters},
sponsor = {Aktion Österreich–Slowakei project 2024-05-15-001, KEGA project 030TUKE-4/2023},
length = {179},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {Wolfgang Schreiner and William Steingartner},
title = {{Semantics-Based Rapid Prototyping of a Subset of SQL}},
language = {english},
abstract = {This report documents the application of our semantics-based language generator SLANG to developing a rapid prototype of a non-trivial domain-specific language, a substantial subset of the Structured Query Language SQL that we have named SubSQL. After developing a mathematical/logical formulation of the language’s abstract syntax, formal type system, and denotational semantics, we have translated this formulation into a SLANG specification from which the SLANG software generates Java code that implements a parser, a printer, a type-checker, and an executor of the language. This implementation is based on several manually created Java classes that implement the mathematical domains and operations used in the formalization, a simple persistent database, and a high-level application programming interface that allows to execute complete SubSQL scripts from file or individual SubSQL commands within Java programs. The results represent a blueprint for the semantics-based development of other domain-specific languages of similar complexity.},
number = {25-02},
year = {2025},
month = {February},
keywords = {formal semantics of programming languages, domain specific languages, rapid prototyping, interpreters},
sponsor = {Aktion Österreich–Slowakei project 2024-05-15-001, KEGA project 030TUKE-4/2023},
length = {179},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Schreiner]
Executable Semantics for Teaching Concatenative Stack-Based DSLs: The Case of StackLang
William Steingartner, Wolfgang Schreiner
In: New Trends in Database and Information Systems, ADBIS 2025 Short Papers, Doctoral Consortium and Tutorials, Tampere, Finland, September 23-26, 2025, Proceedings, Panos K. Chrysanthis, Kjetil Nørvåg, Kostas Stefanidis, Zheying Zhang, Elisa Quintarelli, Ester Zumpano (ed.), Communications in Computer and Information Science (CCIS) 2676, pp. 248-263. 2025. Springer, Cham, Switzerland, ISBN 978-3-032-05726-6. [doi]@inproceedings{RISC7155,
author = {William Steingartner and Wolfgang Schreiner},
title = {{Executable Semantics for Teaching Concatenative Stack-Based DSLs: The Case of StackLang}},
booktitle = {{New Trends in Database and Information Systems, ADBIS 2025 Short Papers, Doctoral Consortium and Tutorials, Tampere, Finland, September 23-26, 2025, Proceedings}},
language = {english},
abstract = {In the context of teaching computer science, many domain-specific languages (DSLs) used for data manipulation and transformation follow imperative paradigms, yet their semantics remain informal or tool-dependent. This paper proposes a pedagogical framework based on executable formal semantics to improve conceptual understanding and practical competence in such DSLs. Using a minimal imperative DSL developed as a teaching tool to illustrate arithmetic and data transformations, we define its syntax and semantics using denotational semantics and develop an executable interpreter directly derived from the formal rules. The framework enables students to explore and visualize the effects of each language construct, reason about program behavior, and verify correctness properties. We present a case study in which we focus on the gradual use of cross-curricular relationships and gradually build a comprehensive package for students that draws on knowledge from several courses focused on formal methods in software engineering. The paper concludes with a discussion of the potential of this methodology to bridge the gap between formal methods and practical education in the field of computer science.},
series = {Communications in Computer and Information Science (CCIS)},
volume = {2676},
pages = {248--263},
publisher = {Springer},
address = {Cham, Switzerland},
isbn_issn = {ISBN 978-3-032-05726-6},
year = {2025},
editor = {Panos K. Chrysanthis and Kjetil Nørvåg and Kostas Stefanidis and Zheying Zhang and Elisa Quintarelli and Ester Zumpano},
refereed = {yes},
keywords = {formal semantics, domain-specific languages, computer science education},
sponsor = {Aktion Österreich–Slowakei project 2024-05-15-001, KEGA project 030TUKE-4/2023},
length = {15},
url = {https://doi.org/10.1007/978-3-032-05727-3_23}
}
author = {William Steingartner and Wolfgang Schreiner},
title = {{Executable Semantics for Teaching Concatenative Stack-Based DSLs: The Case of StackLang}},
booktitle = {{New Trends in Database and Information Systems, ADBIS 2025 Short Papers, Doctoral Consortium and Tutorials, Tampere, Finland, September 23-26, 2025, Proceedings}},
language = {english},
abstract = {In the context of teaching computer science, many domain-specific languages (DSLs) used for data manipulation and transformation follow imperative paradigms, yet their semantics remain informal or tool-dependent. This paper proposes a pedagogical framework based on executable formal semantics to improve conceptual understanding and practical competence in such DSLs. Using a minimal imperative DSL developed as a teaching tool to illustrate arithmetic and data transformations, we define its syntax and semantics using denotational semantics and develop an executable interpreter directly derived from the formal rules. The framework enables students to explore and visualize the effects of each language construct, reason about program behavior, and verify correctness properties. We present a case study in which we focus on the gradual use of cross-curricular relationships and gradually build a comprehensive package for students that draws on knowledge from several courses focused on formal methods in software engineering. The paper concludes with a discussion of the potential of this methodology to bridge the gap between formal methods and practical education in the field of computer science.},
series = {Communications in Computer and Information Science (CCIS)},
volume = {2676},
pages = {248--263},
publisher = {Springer},
address = {Cham, Switzerland},
isbn_issn = {ISBN 978-3-032-05726-6},
year = {2025},
editor = {Panos K. Chrysanthis and Kjetil Nørvåg and Kostas Stefanidis and Zheying Zhang and Elisa Quintarelli and Ester Zumpano},
refereed = {yes},
keywords = {formal semantics, domain-specific languages, computer science education},
sponsor = {Aktion Österreich–Slowakei project 2024-05-15-001, KEGA project 030TUKE-4/2023},
length = {15},
url = {https://doi.org/10.1007/978-3-032-05727-3_23}
}
[Schreiner]
Thinking Programs
Wolfgang Schreiner
Texts & Monographs in Symbolic Computation 2nd edition, 2025. Springer, Cham, Switzerland, Hardcover ISBN 978-3-031-99704-4, Softcover ISBN 978-3-031-99707-5, eBook ISBN 978-3-031-99705-1. [doi]@book{RISC7179,
author = {Wolfgang Schreiner},
title = {{Thinking Programs}},
language = {english},
series = {Texts & Monographs in Symbolic Computation},
publisher = {Springer, Cham, Switzerland},
isbn_issn = {Hardcover ISBN 978-3-031-99704-4, Softcover ISBN 978-3-031-99707-5, eBook ISBN 978-3-031-99705-1},
year = {2025},
edition = {2nd},
translation = {0},
length = {641},
url = {https://doi.org/10.1007/978-3-031-99705-1}
}
author = {Wolfgang Schreiner},
title = {{Thinking Programs}},
language = {english},
series = {Texts & Monographs in Symbolic Computation},
publisher = {Springer, Cham, Switzerland},
isbn_issn = {Hardcover ISBN 978-3-031-99704-4, Softcover ISBN 978-3-031-99707-5, eBook ISBN 978-3-031-99705-1},
year = {2025},
edition = {2nd},
translation = {0},
length = {641},
url = {https://doi.org/10.1007/978-3-031-99705-1}
}
[Schreiner]
A DSL for Specifying a Class of Industrial Optimisation Problems
Tereso del Rio, Wolfgang Schreiner, Martina Seidl, Temur Kutsia, Wolfgang Windsteiger
Technical report no. 25-12 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2025. Licensed under CC BY 4.0 International. [doi] [pdf]@techreport{RISC7224,
author = {Tereso del Rio and Wolfgang Schreiner and Martina Seidl and Temur Kutsia and Wolfgang Windsteiger},
title = {{A DSL for Specifying a Class of Industrial Optimisation Problems}},
language = {english},
abstract = {This report documents a newdomain-specific language (DSL) designed to express industrial optimisation problems in a Pythonic and procedural way. This language allows users to describe optimisation models using familiar programming tools such as variables, loops, and conditional statements, instead of low-level mathematical formulations.},
number = {25-12},
year = {2025},
month = {December},
keywords = {industrial optimization, constraint solving, domain-specific languages},
sponsor = {Supported by FFG project 59218671 “InProSSA: Industrial Problem Solving Using Symbolic and Subsymbolic AI”},
length = {19},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {Tereso del Rio and Wolfgang Schreiner and Martina Seidl and Temur Kutsia and Wolfgang Windsteiger},
title = {{A DSL for Specifying a Class of Industrial Optimisation Problems}},
language = {english},
abstract = {This report documents a newdomain-specific language (DSL) designed to express industrial optimisation problems in a Pythonic and procedural way. This language allows users to describe optimisation models using familiar programming tools such as variables, loops, and conditional statements, instead of low-level mathematical formulations.},
number = {25-12},
year = {2025},
month = {December},
keywords = {industrial optimization, constraint solving, domain-specific languages},
sponsor = {Supported by FFG project 59218671 “InProSSA: Industrial Problem Solving Using Symbolic and Subsymbolic AI”},
length = {19},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[STUDENT]
A Saturation-Based Automated Theorem Prover for RISCAL
Viktoria Langenreither
Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. December 2025. Also available as RISC report no. 25-11. [doi] [pdf]@misc{RISC7222,
author = {Viktoria Langenreither},
title = {{A Saturation-Based Automated Theorem Prover for RISCAL}},
language = {english},
abstract = {The aim of this thesis is to integrate a automated theorem prover for first-order logic with equality in the RISC theorem proving (RISCTP) software. The software currently already provides a built-in first-order prover. The MESON prover (model-elimination, subgoaloriented) follows a goal oriented approach. The idea is to provide a different procedure (knowledge-based) to further extend the functionality of RISCTP, since different prove designs lead to a fast proof search for different examples. One way to achieve this is by using the saturation principle, i. e. the prover generates from a set of first-order clauses in a systematic way all logical consequences until a refutation (empty clause) is found.In this thesis we give a throughout theoretical representation of different techniques for first-order provers, based on a comprehensive literature research. In accordance to this, we developed the design of our prover. As most state of the art provers, it is based of the give-clause-algorithm using the DISCOUNT loop to organize the proof search. The inference system is based on a variation of the superposition calculus, using the so-called pure superposition for the equality reasoning (all literals represent equalities). To further extend this prover an interface to an external SMT solver is integrated as well as axioms encoding the special theories of integers and arrays. The implementation of this prover is done as an extension of the RISCTP software using the Java programming language. To evaluate the prover, we used examples that were already defined for evaluating the MESON prover.},
year = {2025},
month = {December},
note = {Also available as RISC report no. 25-11},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {automated reasoning, formal methods, program verification},
length = {108},
url = {https://doi.org/10.35011/risc.25-11}
}
author = {Viktoria Langenreither},
title = {{A Saturation-Based Automated Theorem Prover for RISCAL}},
language = {english},
abstract = {The aim of this thesis is to integrate a automated theorem prover for first-order logic with equality in the RISC theorem proving (RISCTP) software. The software currently already provides a built-in first-order prover. The MESON prover (model-elimination, subgoaloriented) follows a goal oriented approach. The idea is to provide a different procedure (knowledge-based) to further extend the functionality of RISCTP, since different prove designs lead to a fast proof search for different examples. One way to achieve this is by using the saturation principle, i. e. the prover generates from a set of first-order clauses in a systematic way all logical consequences until a refutation (empty clause) is found.In this thesis we give a throughout theoretical representation of different techniques for first-order provers, based on a comprehensive literature research. In accordance to this, we developed the design of our prover. As most state of the art provers, it is based of the give-clause-algorithm using the DISCOUNT loop to organize the proof search. The inference system is based on a variation of the superposition calculus, using the so-called pure superposition for the equality reasoning (all literals represent equalities). To further extend this prover an interface to an external SMT solver is integrated as well as axioms encoding the special theories of integers and arrays. The implementation of this prover is done as an extension of the RISCTP software using the Java programming language. To evaluate the prover, we used examples that were already defined for evaluating the MESON prover.},
year = {2025},
month = {December},
note = {Also available as RISC report no. 25-11},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {automated reasoning, formal methods, program verification},
length = {108},
url = {https://doi.org/10.35011/risc.25-11}
}
2024
[AUTHOR]
A Formalization of the General Theory of Quaternions
Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón
In: Leibniz International Proceedings in Informatics (LIPIcs), Yves Bertot, Temur Kutsia, and Michael Norrish (ed.), pp. 11:1-11:18. 2024. ISSN 1868-8969.@inproceedings{RISC7108,
author = {Thaynara Arielly de Lima and André Luiz Galdino and Bruno Berto de Oliveira Ribeiro and and Mauricio Ayala-Rincón},
title = {{A Formalization of the General Theory of Quaternions}},
booktitle = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
language = {english},
pages = {11:1--11:18},
isbn_issn = {ISSN 1868-8969},
year = {2024},
editor = {Yves Bertot and Temur Kutsia and and Michael Norrish},
refereed = {yes},
length = {18}
}
author = {Thaynara Arielly de Lima and André Luiz Galdino and Bruno Berto de Oliveira Ribeiro and and Mauricio Ayala-Rincón},
title = {{A Formalization of the General Theory of Quaternions}},
booktitle = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
language = {english},
pages = {11:1--11:18},
isbn_issn = {ISSN 1868-8969},
year = {2024},
editor = {Yves Bertot and Temur Kutsia and and Michael Norrish},
refereed = {yes},
length = {18}
}
[Buchberger]
Science and Meditation: Creating the Future (English Translation of "Wissenschaft und Meditation")
Bruno Buchberger
1st edition, 2024. Amazon, 979-8332230837.@book{RISC7102,
author = {Bruno Buchberger},
title = {{Science and Meditation: Creating the Future (English Translation of "Wissenschaft und Meditation")}},
language = {english},
publisher = {Amazon},
isbn_issn = { 979-8332230837},
year = {2024},
edition = {1st},
translation = {0},
length = {153}
}
author = {Bruno Buchberger},
title = {{Science and Meditation: Creating the Future (English Translation of "Wissenschaft und Meditation")}},
language = {english},
publisher = {Amazon},
isbn_issn = { 979-8332230837},
year = {2024},
edition = {1st},
translation = {0},
length = {153}
}
[Cerna]
Equational Anti-unification over Absorption Theories
Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia
In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 317-337. 2024. Springer, ISBN 978-3-031-63500-7. [doi]@inproceedings{RISC7064,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-unification over Absorption Theories}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {317--337},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {21},
url = {https://doi.org/10.1007/978-3-031-63501-4_17}
}
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-unification over Absorption Theories}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {317--337},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {21},
url = {https://doi.org/10.1007/978-3-031-63501-4_17}
}
[de Lima]
A Formalization of the General Theory of Quaternions
de Lima Thaynara Arielly, Galdino André Luiz, de Oliveira Ribeiro Bruno Berto, Ayala-Rincón Mauricio Bertot, Yves and Kutsia, Temur and Norrish, Michael
In: 15th International Conference on Interactive Theorem Proving (ITP 2024), Bertot, Yves and Kutsia, Temur and Norrish, Michael (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 309, pp. 11:1-11:18. 2024. Dagstuhl, Germany, ISBN 978-3-95977-337-9 ISSN 1868-8969. [url]@inproceedings{RISC7110,
author = {de Lima Thaynara Arielly and Galdino André Luiz and de Oliveira Ribeiro Bruno Berto and Ayala-Rincón Mauricio Bertot and Yves and Kutsia and Temur and Norrish and Michael},
title = {{A Formalization of the General Theory of Quaternions}},
booktitle = {{15th International Conference on Interactive Theorem Proving (ITP 2024)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {309},
pages = {11:1--11:18},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-337-9 ISSN 1868-8969},
year = {2024},
annote = {Keywords: Theory of quaternions, Hamilton’s quaternions, Algebraic formalizations, PVS},
editor = {Bertot and Yves and Kutsia and Temur and Norrish and Michael},
refereed = {yes},
length = {0},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.11}
}
author = {de Lima Thaynara Arielly and Galdino André Luiz and de Oliveira Ribeiro Bruno Berto and Ayala-Rincón Mauricio Bertot and Yves and Kutsia and Temur and Norrish and Michael},
title = {{A Formalization of the General Theory of Quaternions}},
booktitle = {{15th International Conference on Interactive Theorem Proving (ITP 2024)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {309},
pages = {11:1--11:18},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-337-9 ISSN 1868-8969},
year = {2024},
annote = {Keywords: Theory of quaternions, Hamilton’s quaternions, Algebraic formalizations, PVS},
editor = {Bertot and Yves and Kutsia and Temur and Norrish and Michael},
refereed = {yes},
length = {0},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.11}
}
