@techreport{RISC6272,
author = {J. Ablinger},
title = {{Extensions of the AZ-algorithm and the Package MultiIntegrate}},
language = {english},
abstract = {We extend the (continuous) multivariate Almkvist-Zeilberger algorithm inorder to apply it for instance to special Feynman integrals emerging in renormalizable Quantum field Theories. We will consider multidimensional integrals overhyperexponential integrals and try to find closed form representations in terms ofnested sums and products or iterated integrals. In addition, if we fail to computea closed form solution in full generality, we may succeed in computing the firstcoeffcients of the Laurent series expansions of such integrals in terms of indefnitenested sums and products or iterated integrals. In this article we present the corresponding methods and algorithms. Our Mathematica package MultiIntegrate,can be considered as an enhanced implementation of the (continuous) multivariateAlmkvist Zeilberger algorithm to compute recurrences or differential equations forhyperexponential integrands and integrals. Together with the summation packageSigma and the package HarmonicSums our package provides methods to computeclosed form representations (or coeffcients of the Laurent series expansions) of multidimensional integrals over hyperexponential integrands in terms of nested sums oriterated integrals.},
number = {21-02},
year = {2021},
month = {January},
keywords = {multivariate Almkvist-Zeilberger algorithm, hyperexponential integrals, iterated integrals, nested sums},
length = {25},
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{RISC6293,
author = {Tudor Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
language = {english},
abstract = {We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.},
number = {21-07},
year = {2021},
month = {April},
keywords = {Theorema, S-decomposition, automated theorem proving},
length = {29},
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{RISC6296,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},
language = {english},
abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},
number = {21-08},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},
length = {15},
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{RISC6297,
author = {Temur Kutsia and Cleo Pau},
title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},
number = {21-09},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},
length = {15},
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{RISC6328,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{Semantic Evaluation versus SMT Solving in the RISCAL Model Checker}},
language = {english},
abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion oftheir fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room forimprovements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},
number = {21-11},
year = {2021},
month = {June},
keywords = {model checking, satisfiability solving, formal specification, formal verficiation},
sponsor = {JKU Linz Institute of Technology (LIT) Project LOGTECHEDU, Aktion Österreich- Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255.},
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)}
}