Automated Reasoning

At RISC we are devoted to the foundations, the design, and the implementation of software to generate mathematical proofs.

The main enterprise in the area of automated reasoning at RISC is the Theorema project. Theorema has been initiated around 1995 by Bruno Buchberger, who has led the project ever since. Some activities in the area of formal methods are tightly related to what we do in automated reasoning.

Software

Theorema

A Mathematical Assistant System implemented in Mathematica

The present prototype version of the Theorema software system is implemented in Mathematica . The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. ...

MoreSoftware Website

Publications

2023

[Buchberger]

Is ChatGPT Smarter Than Master’s Applicants?

Bruno Buchberger

Technical report no. 23-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). January 2023. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6684,
author = {Bruno Buchberger},
title = {{Is ChatGPT Smarter Than Master’s Applicants?}},
language = {English},
abstract = {During the selection procedure for a particular informatics fellowship program sponsored by Upper Austrian companies, I ask the applicants a couple of simple technical questions about programming, etc., in a Zoom meeting. I put the same questions to the dialogue system ChatGPT, [ChatGPT]. The result surprised me: Nearly all answers of ChatGPT were totally correct and nicely explained. Also, in the dialogues to clarify some critical points in the answers, the explanations by ChatGPT were amazingly clear and goal-oriented.In comparison: I tried out the same questions in the personal Zoom interviews with approximately 30 applicants from five countries. Only the top three candidates (with a GPA of 1.0, i.e., the highest possible GPA in their bachelor’s study) performed approximately equally well in the interview. All the others performed (far) worse than ChatGPT. And, of course, all answers from ChatGPT came within 1 to 10 seconds, whereas most of the human applicants' answers needed lengthy and arduous dialogues.I am particularly impressed by the ability of ChatGPT to extract meaningful and well-structured programs from problem specifications in natural language. In this experiment, I also added some questions that ask for proofs for simple statements in natural language, which I do not ask in the student's interviews. The performance of ChatGPT was quite impressive as far as formalization and propositional logic are concerned. In examples where predicate logic reasoning is necessary, the ChatGPT answers are not (yet?) perfect. I am pleased to see that ChatGPT tries to present the proofs in a “natural style” This is something that I had as one of my main goals when I initiated the Theorema project in 1995. I think we already achieved this in the early stage of Theorema, and we performed this slightly better and more systematically than ChatGPT does.I also tried to develop a natural language input facility for Theorema in 2017, i.e., a tool to formalize natural language statements in predicate logic. However, I could not continue this research for a couple of reasons. Now I see that ChatGPT achieved this goal. Thus, I think that the following combination of methods could result in a significant leap forward:- the “natural style” proving methods that we developed within Theorema (for the automated generation of programs from specifications, the automated verification of programs in the frame of knowledge, and the automated proof of theorems in theories), in particular, my “Lazy Thinking Method” for algorithm synthesis from specifications- and the natural language formalization techniques of ChatGPT.I propose this as a research project topic and invite colleagues and students to contact me and join me in this effort: Buchberger.bruno@gmail.com.},
number = {23-04},
year = {2023},
month = {January},
keywords = {ChatGPT, automated programming, program synthesis, automated proving, formalization of natural language, master's screening},
length = {30},
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)}
}
[Buchberger]

Automated Programming, Symbolic computation, Machine Learning: My Personal View

Bruno Buchberger

Ann. Math. Artif. Intell. 91(5), pp. 569-589. 2023. 1012-2443.
[bib]
@article{RISC6895,
author = {Bruno Buchberger},
title = {{Automated Programming, Symbolic computation, Machine Learning: My Personal View}},
language = {english},
journal = {Ann. Math. Artif. Intell.},
volume = {91},
number = {5},
pages = {569--589},
isbn_issn = {1012-2443},
year = {2023},
refereed = {yes},
length = {21}
}
[Buchberger]

International Young Talents Hotspot Austria

Bruno Buchberger

In: Ideen, die gehen!, W. Schüssel, G. Kneifel (ed.), pp. 37-39. 2023. Edition Kleine Zeitung, 20234.
[bib]
@incollection{RISC6896,
author = {Bruno Buchberger},
title = {{International Young Talents Hotspot Austria}},
booktitle = {{Ideen, die gehen!}},
language = {english},
pages = {37--39},
publisher = {Edition Kleine Zeitung},
isbn_issn = {20234},
year = {2023},
editor = {W. Schüssel and G. Kneifel},
refereed = {no},
length = {3}
}
[Buchberger]

Wissenschaft und Meditation: Auf dem Weg zur bewussten Naturgesellschaft

Bruno Buchberger

1st edition, December 2023. Amazon, 979-8868299117.
[bib]
@book{RISC6898,
author = {Bruno Buchberger},
title = {{Wissenschaft und Meditation: Auf dem Weg zur bewussten Naturgesellschaft}},
language = {german},
publisher = {Amazon},
isbn_issn = {979-8868299117},
year = {2023},
month = {December},
edition = {1st},
translation = {0},
length = {184}
}
[Cerna]

Anti-unification and Generalization: a Survey

David Cerna, Temur Kutsia

In: Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence, Edith Elkind (ed.), pp. 6563-6573. 2023. ijcai.org, ISBN 978-1-956792-03-4 . [doi]
[bib]
@inproceedings{RISC6743,
author = {David Cerna and Temur Kutsia},
title = {{Anti-unification and Generalization: a Survey}},
booktitle = {{Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence}},
language = {english},
pages = {6563--6573},
publisher = {ijcai.org},
isbn_issn = {ISBN 978-1-956792-03-4 },
year = {2023},
editor = {Edith Elkind},
refereed = {yes},
length = {11},
url = {https://doi.org/10.24963/ijcai.2023/736}
}
[Cerna]

Equational Anti-Unification over Absorption Theories

Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

arXiv:2310.11136. Technical report, 2023. [doi]
[bib]
@techreport{RISC6884,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-Unification over Absorption Theories}},
language = {english},
year = {2023},
institution = {arXiv:2310.11136},
length = {23},
url = {https://doi.org/10.48550/arXiv.2310.11136}
}
[Ehling]

Matching in Quantitative Equational Theories

Georg Ehling, Temur Kutsia

In: UNIF 2023 - 37th International Workshop on Unification, Veena Ravishankar and Christophe Ringeissen (ed.), pp. -. 2023. [url]
[bib]
@inproceedings{RISC6885,
author = {Georg Ehling and Temur Kutsia},
title = {{Matching in Quantitative Equational Theories}},
booktitle = {{UNIF 2023 - 37th International Workshop on Unification}},
language = {english},
pages = {--},
isbn_issn = { },
year = {2023},
editor = {Veena Ravishankar and Christophe Ringeissen},
refereed = {yes},
sponsor = {FWF},
length = {7},
url = {https://inria.hal.science/hal-04128216}
}
[Kutsia]

Nominal AC-Matching

Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, and Daniele Nantes-Sobrinho

In: Proceedings of the 16th International Conference on Intelligent Computer Mathematics, CICM 2023, Catherine Dubois and Manfred Kerber (ed.), Lecture Notes in Aritificial Intelligence 14101, pp. 53-68. 2023. Springer, ISBN 978-3-031-42752-7. [doi]
[bib]
@inproceedings{RISC6744,
author = {Mauricio Ayala-Rincón and Maribel Fernández and Gabriel Ferreira Silva and Temur Kutsia and and Daniele Nantes-Sobrinho},
title = {{Nominal AC-Matching}},
booktitle = {{Proceedings of the 16th International Conference on Intelligent Computer Mathematics, CICM 2023}},
language = {english},
series = {Lecture Notes in Aritificial Intelligence},
volume = {14101},
pages = {53--68},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-42752-7},
year = {2023},
editor = {Catherine Dubois and Manfred Kerber},
refereed = {yes},
length = {16},
url = {https://doi.org/10.1007/978-3-031-42753-4_4}
}
[Pau]

Enumerating All Maximal Clique-Partitions of an Undirected Graph

Mircea Marin, Temur Kutsia, Cleo Pau, Mikheil Rukhaia

In: Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Horatiu Cheval, Laurentiu Leustean, and Andrei Sipos (ed.), pp. 65-79. 2023. [doi]
[bib]
@inproceedings{RISC6882,
author = {Mircea Marin and Temur Kutsia and Cleo Pau and Mikheil Rukhaia},
title = {{Enumerating All Maximal Clique-Partitions of an Undirected Graph}},
booktitle = {{Proceedings 7th Symposium on Working Formal Methods, FROM 2023}},
language = {english},
pages = {65--79},
isbn_issn = { },
year = {2023},
editor = {Horatiu Cheval and Laurentiu Leustean and and Andrei Sipos},
refereed = {yes},
length = {15},
url = {https://doi.org/10.4204/EPTCS.389.6}
}
[Schreiner]

Concrete Abstractions

Wolfgang Schreiner

Texts & Monographs in Symbolic Computation 1st edition, 2023. Springer, Cham, Switzerland, Hardcover ISBN 978-3-031-24933-4, Softcover ISBN 978-3-031-24936-5, eBook ISBN 978-3-031-24934-1. [doi]
[bib]
@book{RISC6698,
author = {Wolfgang Schreiner},
title = {{Concrete Abstractions}},
language = {english},
series = {Texts & Monographs in Symbolic Computation},
publisher = {Springer},
address = {Cham, Switzerland},
isbn_issn = {Hardcover ISBN 978-3-031-24933-4, Softcover ISBN 978-3-031-24936-5, eBook ISBN 978-3-031-24934-1},
year = {2023},
edition = {1st},
translation = {0},
keywords = {logic in computer science, model checking, formal modeling and reasoning, program specification and verification, discrete structures and algorithms, nondeterminism and concurrency},
length = {270},
url = {https://doi.org/10.1007/978-3-031-24934-1}
}
[Schreiner]

The SLANG Semantics-Based Language Generator

Wolfgang Schreiner, William Steingartner

Technical report no. 23-13 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). September 2023. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6749,
author = {Wolfgang Schreiner and William Steingartner},
title = {{The SLANG Semantics-Based Language Generator}},
language = {english},
abstract = {This report documents the SLANG semantics-based language generator. SLANG is a software for generating rapid prototype implementations of programming languages from their formal specifications. Its input is a text file that describes the abstract syntax of a language and its concrete text representation; from this, a parser is generated (utilizing the ANTLR4 tool) that transforms the text representation of a program into its abstract syntax tree and a printer that generates from the abstract syntax tree its text representation. Furthermore, one can equip the language with a formal type system (by logical inference rules) from which a type checker is generated. Finally, one can give the language a formal semantics, in the denotational style (by function equations) and/or in the big-step operational style (by transition steps); from this, a language interpreter is generated. SLANG is implemented in Java and produces Java source code; it should be easy to extend the software also to other target languages.},
number = {23-13},
year = {2023},
month = {September},
keywords = {formal semantics of programming languages, denotational semantics, operational semantics, type systems, interpreters},
sponsor = {Supported by the Slovak Academic Information Agency SAIA project 2023-03-15-001 “Semantics-Based Rapid Prototyping of Domain-Specific Languages”},
length = {59},
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]

Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker

Joachim Borya

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Bachelor Thesis. May 2023. Also available as RISC Report 23-06. [doi] [pdf]
[bib]
@misc{RISC6707,
author = {Joachim Borya},
title = {{Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker}},
language = {english},
abstract = {The relational database model is based on the mathematical concept of relational algebra.Query languages have been developed to make data available quickly without creatingdedicated access procedures that depend on the internal representation of the data. SQL(structured query language) can be seen as a quasi-standard for this. This thesis dealswith the formalization and verification of relational algebra and a small but elementarysubset of SQL with the help of the RISCAL model checker, a software tool for the formalspecification and verification of mathematical theories and algorithms.},
year = {2023},
month = {May},
note = {Also available as RISC Report 23-06},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal methods, program verification, model checking, automated theorem proving},
length = {77},
url = {https://doi.org/10.35011/risc.23-06}
}
[STUDENT]

Model Checking Concurrent Systems Under Fairness Constraints in RISCAL

Ágoston Sütő

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis. May 2023. Also available as RISC Report 23-07. Master's thesis. [doi] [pdf]
[bib]
@misc{RISC6709,
author = {Ágoston Sütő},
title = {{Model Checking Concurrent Systems Under Fairness Constraints in RISCAL}},
language = {english},
abstract = {Model checking is a method for verifying that a program satisfies certain desirable properties formalised using mathematical logic. It is a rigorous method, similar to theorem proving, but it is generally applied when theorem proving would be too difficult due to the complexity of the algorithm, such as in concurrent systems. Model checking is used in the software industry. RISCAL (RISC Algorithm Language) is a language and software system that can be used to describe algorithms over a finite domain, specify their behaviour and then validate the specification. While it mainly focuses on deterministic algorithms, it has limited support for non-deterministic systems as well.The thesis extends the support for non-deterministic systems in RISCAL by allowing the user to specify complex properties about their behaviour in the language of Linear Temporal Logic (LTL) and then to validate them. The core contribution is a model checker implemented in Java using the so-called automaton-based explicit state model checking approach. The software is capable of verifying certain properties that could not be handled by a well-known model checker used in the industry. While in most cases it has underperformed its competitors, our implementation is promising, especially when it comes to properties with certain side conditions, called fairness constraints. The majority of the thesis is be concerned with the theoretical aspects of the automaton-based model checking approach, which is followed by a description of the implementation and various benchmarks.},
year = {2023},
month = {May},
note = {Also available as RISC Report 23-07},
translation = {0},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal methods, model checking, concurrent systems, nondeterminism, linear temporal logic},
sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},
length = {102},
url = {https://doi.org/10.35011/risc.23-07},
type = {Master's thesis}
}

2022

[Cerna]

Learning Higher-Order Programs without Meta-Interpretive Learning

Stanislav Purgal and David Cerna and Cezary Kalisyk

In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, Lud De Raedt (ed.), Proceedings of International Joint Conference on Artificial Intelligence, Main Track , pp. 2726-2733. july 2022. International Joint Conferences on Artificial Intelligence Organization, 10.24963/ijcai.2022/378. [doi]
[bib]
@inproceedings{RISC6646,
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
booktitle = {{Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22}},
language = {english},
abstract = {Learning complex programs through textit{inductive logic programming} (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile textit{Learning From Failures} paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higher-order definitions handled by our extension.},
series = {Main Track},
pages = {2726--2733},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
isbn_issn = {10.24963/ijcai.2022/378},
year = {2022},
month = {july},
editor = {Lud De Raedt},
refereed = {yes},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
conferencename = {International Joint Conference on Artificial Intelligence},
url = {https://doi.org/10.35011/risc.21-22}
}
[Dundua]

Unranked Nominal Unification

Besik Dundua, Temur Kutsia, Mikheil Rukhaia

In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Proceedings of 13th International Tbilisi Symposium on Logic, Language, and Computation, Lecture Notes in Computer Science 13206, pp. 279-296. 2022. Springer, ISBN 978-3-030-98478-6. [doi] [pdf]
[bib]
@inproceedings{RISC6498,
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {279--296},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {17},
conferencename = {13th International Tbilisi Symposium on Logic, Language, and Computation},
url = {https://doi.org/10.1007/978-3-030-98479-3_14}
}
[Kutsia]

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz

Fundamenta Informaticae 185(3), pp. 247-283. 2022. IOS Press, ISSN 1875-8681. [url]
[bib]
@article{RISC6506,
author = {Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz},
title = {{Nominal Unification and Matching of Higher Order Expressions with Recursive Let}},
language = {english},
journal = {Fundamenta Informaticae},
volume = {185},
number = {3},
pages = {247--283},
publisher = {IOS Press},
isbn_issn = {ISSN 1875-8681},
year = {2022},
refereed = {yes},
length = {37},
url = {https://arxiv.org/abs/2102.08146v4}
}
[Kutsia]

Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, CICM 2022 (Informal Proceedings)

Kevin Buzzard and Temur Kutsia

, 2022. [url] [pdf]
[bib]
@techreport{RISC6584,
author = {Kevin Buzzard and Temur Kutsia},
title = {{Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, CICM 2022 (Informal Proceedings)}},
language = {english},
year = {2022},
institution = { },
length = {77},
url = {https://cicm-conference.org/2022/cicm.php}
}
[Pau]

Matching and Generalization Modulo Proximity and Tolerance Relations

Temur Kutsia, Cleo Pau

In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Lecture Notes in Computer Science 13206, pp. 323-342. 2022. Springer, ISBN 978-3-030-98478-6. [doi] [pdf]
[bib]
@inproceedings{RISC6491,
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance Relations}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {323--342},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-030-98479-3_16}
}
[Pau]

A framework for approximate generalization in quantitative theories

Temur Kutsia, Cleo Pau

Technical report no. 22-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). May 2022. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6505,
author = {Temur Kutsia and Cleo Pau},
title = {{A framework for approximate generalization in quantitative theories}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into "proximal'' up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.},
number = {22-04},
year = {2022},
month = {May},
keywords = {Generalization, anti-unification, quantiative theories, fuzzy proximity relations},
length = {22},
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)}
}
[Pau]

A Framework for Approximate Generalization in Quantitative Theories

Temur Kutsia and Cleo Pau

In: Automated Reasoning, Jasmin Blanchette, Laura Kovács, and Dirk Pattinson (ed.), Proceedings of 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Lecture Notes in Artificial Intelligence 13385, pp. 578-596. 2022. Springer, ISBN 978-3-031-10768-9. [doi]
[bib]
@inproceedings{RISC6631,
author = {Temur Kutsia and Cleo Pau},
title = {{A Framework for Approximate Generalization in Quantitative Theories}},
booktitle = {{Automated Reasoning}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {13385},
pages = {578--596},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-10768-9},
year = {2022},
editor = {Jasmin Blanchette and Laura Kovács and and Dirk Pattinson},
refereed = {yes},
sponsor = {FWF},
length = {19},
conferencename = {11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022},
url = {https://doi.org/10.1007/978-3-031-10769-6}
}

Loading…