Automated Reasoning

@techreport{RISC7141,
author = {Besik Dundua and Temur Kutsia},
title = {{Higher-Order Pattern Unification Modulo Similarity Relations}},
language = {english},
abstract = {The combination of higher-order theories and fuzzy logic can be useful in decision-making tasks that involve reasoning across abstract functions and predicates, where exact matches are often rare or unnecessary. Developing efficient reasoning and computational techniques for such a combined formalism presents a significant challenge. In this paper, we adopt a more straightforward approach aiming at integrating two well-established and computationally well-behaving components: higher-order patterns on one side and fuzzy equivalences expressed through similarity relations based on minimum T-norm on the other. We propose a unification algorithm for higher-order patterns modulo these similarity relations and prove its termination, soundness, and completeness. This unification problem, like its crisp counterpart, is unitary. The algorithm computes the most general unifier with the highest degree of approximation when the given terms are unifiable.},
number = {25-03},
year = {2025},
month = {February},
keywords = {Unification, higher-order patterns, fuzzy similarity relations},
length = {20},
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)}
}

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

@techreport{RISC7153,
author = {Jack Heseltine},
title = {{Theorema Project: Document Processing}},
language = {english},
abstract = {This work explores the Wolfram Language as a Software Engineering tool, with a particular focus on the Theorema mathematical software package, in combination with the LATEX typesetting system. It delves into the advanced functionalities and paradigms of Wolfram Language, including high-level programming, functional programming, and pattern matching, to showcase these capabilities beyond object oriented programming languages in particular, as applied to mathematical document transformation. Through Theorema, package development using Wolfram Language is demonstrated from conception through execution to the point that the new package can be easily integrated with the existing Theorema system: the associated analysis touches on the workings of Theorema but the focus is on an implementational bridge between computational mathematics and document preparation, aiming to provide easy extensibility and delivering on further Software Engineering principles to make for a rounded Wolfram Language and Theorema package, as the final project output.The thesis also addresses the challenges and methodologies associated with the LATEX typesetting of mathematical content, emphasizing the transformation of Wolfram Language/Theorema notebooks using a Wolfram-Language-native approach. This includes an examination of first-order predicate logic symbols, to ensure coverage at the output side, and the role of (mathematical) expressions in Wolfram Language, the input side, showcasing back-and-forth between typesetting and (symbolic) computational languages, and particularly, recursive parsing of entire notebook expressions as the basic working principle in this approach.},
number = {25-06},
year = {2025},
month = {March 02},
note = {Bachelor Thesis at University of Applied Sciences Hagenberg, bachelor program Software Engineering},
keywords = {Theorema, LaTeX},
length = {76},
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)}
}

@techreport{RISC7056,
author = {G. Ehling and T. Kutsia},
title = {{Solving Quantitative Equations}},
language = {english},
abstract = {Quantitative equational reasoning provides a framework that extends equality to an abstract notion of proximity by endowing equations with an element of a quantale. In this paper, we discuss the unification problem for a special class of shallow subterm-collapse-free quantitative equational theories. We outline rule-based algorithms for solving such equational unification problems over generic as well as idempotent Lawvereian quantales and study their properties.},
number = {24-03},
year = {2024},
month = {April},
keywords = {quantitative equational reasoning, Lawvereian quantales, equational unification},
length = {23},
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)}
}