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

2022

[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}
}
[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)}
}
[Schreiner]

The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)

Wolfgang Schreiner

Technical report no. 22-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2022. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6517,
author = {Wolfgang Schreiner},
title = {{The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)}},
language = {english},
abstract = {This report documents the RISCTP theorem proving interface. RISCTP consists of alanguage for specifying proof problems and of an associated software for solving theseproblems. The RISCTP language is a typed variant of first-order logic whose level ofabstraction is between that of higher level formal specification languages (such as thelanguage of the RISCAL model checker) and lower level theorem proving languages (such asthe language SMT-LIB supported by various satisfiability modulo theories solvers such as Z3).Thus the RISCTP language can serve as an intermediate layer that simplifies the connectionof specification and verification systems to theorem provers; in fact, it was developed toequip the RISCAL model checker with theorem proving capabilities. The RISCTP softwareis implemented in Java with an API that enables the implementation of such connections;however, RISCTP also provides a text-based frontend that allows its use as a theorem proveron its own. RISCTP already implements a backend that translates a proving problem intoSMT-LIB and solves it by the "black box" application of Z3; in the future, RISCTP shall alsoprovide built-in proving capabilities with greater transparency.},
number = {22-07},
year = {2022},
month = {June},
keywords = {automated reasoning, theorem proving, model checking, first-order logic, RISCAL, SMT-LIB, Z3},
length = {31},
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)}
}
[Windsteiger]

Learning to Reason Assisted by Automated Reasoning

W. Windsteiger

In: Intelligent Computer Mathematics: 15th International Conference, K. Buzzard and T. Kutsia (ed.), Proceedings of CICM 2022, Lecture Notes in Computer Science , pp. ??-??. 2022. Springer, ???. Accepted for publication. [pdf]
[bib]
@inproceedings{RISC6530,
author = {W. Windsteiger},
title = {{Learning to Reason Assisted by Automated Reasoning}},
booktitle = {{Intelligent Computer Mathematics: 15th International Conference}},
language = {english},
abstract = {We report on using logic software in a novel course-format for an undergraduate logic course for studentsin computer science or artificial intelligence. Although being designed as the students' basic introduction tothe field of logic, the course features a novel structure and it adds some modern content, such as SATand SMT solving, to the traditional and established topics, such as propositional logicand first order predicate logic. The novel course design is characterized by, among others, the integration ofexisting logic software into the teaching of logic.In this paper we focus on the module on first-order predicate logic and the use of the Theorema system as a proof-tutor for the students. We report on statistical evaluation of data collected over two consecutiveyears of teaching this course. On the one hand, we asked for feedback of students on howhelpful they felt the software support was. On the other hand, we evaluated their results in the exams during thecourse and their development over the entire teaching period. The performance in exams is then correlated withstudents'' own perception of the helpfulness of software.},
series = {Lecture Notes in Computer Science},
pages = {??--??},
publisher = {Springer},
isbn_issn = {???},
year = {2022},
note = {Accepted for publication},
editor = {K. Buzzard and T. Kutsia},
refereed = {yes},
length = {16},
conferencename = {CICM 2022}
}

2021

[Cerna]

A Special Case of Schematic Syntactic Unification

David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]
[bib]
@techreport{RISC6349,
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}
[Cerna]

Learning Higher-Order Programs without Meta-Interpretive Learning

Stanislav Purgal and David Cerna and Cezary Kalisyk

Technical report no. 21-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6393,
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
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.},
number = {21-22},
year = {2021},
month = {December},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
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)}
}
[Dramnesc]

AlCons: Deductive Synthesis of Sorting Algorithms in Theorema

I. Dramnesc, T. Jebelean

In: Theoretical Aspects of Computing - ICTAC 2021, A. Cerone, P. Csaba Ölveczky (ed.), Proceedings of 18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan, LNCS 12819, pp. 314-333. September 2021. Springer, 978-3-030-85315-0. [pdf]
[bib]
@inproceedings{RISC6478,
author = {I. Dramnesc and T. Jebelean},
title = {{AlCons: Deductive Synthesis of Sorting Algorithms in Theorema}},
booktitle = {{Theoretical Aspects of Computing - ICTAC 2021}},
language = {english},
abstract = {We describe the principles and the implementation of AlCons (em Algorithm Constructor), a system for the automatic proof--based synthesis of sorting algorithms on lists and on binary trees, in the frame of the Theorema system. The core of the system is a dedicated prover based on specific inference rules and strategies for constructive proofs over the domains of lists and of binary trees, aimed at the automatic synthesis of sorting algorithms and their auxiliary functions from logical specifications. The specific distinctive feature of our approach is the use of multisets for expressing the fact that two lists (trees) have the same elements. This allows a more natural expression of the properties related to sorting, compared to the classical approach using the permutation relation (a list is a permutation of another). Moreover, the use of multisets leads to special inference rules and strategies which make the proofs more efficient, as for instance: expand/compress multiset terms and solve meta-variables using multiset equalities. Additionally we use a Noetherian induction strategy based on the relation induced by the strict inclusion of multisets, which facilitates the synthesis of arbitrary recursion structures, without having to indicate the recursion schemes in advance. The necessary auxiliary algorithms (like, e.g., for insertion and merging) are generated by the same principles from the synthesis conjectures that are automatically produced during the main proof, using a ``cascading" method, which in fact contributes to the automation of theory exploration. The prover is implemented in the frame of the Theorema system and works in natural style, while the generated algorithms can be immediately tested in the same system.},
series = {LNCS},
volume = {12819},
pages = {314--333},
publisher = {Springer},
isbn_issn = {978-3-030-85315-0},
year = {2021},
month = {September },
editor = {A. Cerone and P. Csaba Ölveczky},
refereed = {yes},
length = {20},
conferencename = {18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan}
}
[Dundua]

Variadic equational matching in associative and commutative theories

Besik Dundua, Temur Kutsia, Mircea Marin

Journal of Symbolic Computation 106, pp. 78-109. 2021. Elsevier, ISSN 0747-7171. [doi] [pdf]
[bib]
@article{RISC6260,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic equational matching in associative and commutative theories}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {106},
pages = {78--109},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1016/j.jsc.2021.01.001}
}
[Jebelean]

A Heuristic Prover for Elementary Analysis in Theorema

Tudor Jebelean

Technical report no. 21-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@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)}
}
[Jebelean]

A Heuristic Prover for Elementary Analysis in Theorema

T. Jebelean

In: Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania, F. Kamaredine, C. Sacerdoti Coen (ed.), Proceedings of Intelligent Computer Mathematics, 14th International Conference, CICM 2021, LNAI 12833, pp. 130-134. July 2021. Springer, 978-3-030-81096-2. [pdf]
[bib]
@inproceedings{RISC6477,
author = {T. Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
booktitle = {{Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania}},
language = {english},
abstract = { We present a plug-in to the Theorema system, which generates proofs similar to those produced by humans for theorems in elementary analysis and is based on heuristic techniques combining methods from automated reasoning and computer algebra. The prover is able to construct automatically natural-style proofs for various examples related to convergence of sequences as well as to limits, continuity, and uniform continuity of functions. Additionally to general inference rules for predicate logic, the techniques used are: the S-decomposition method for formulae with alternating quantifiers, use of 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 admissibility of solutions to the metavariables. The problem of proving such theorems directly without using refutation and clausification is logically equivalent to the problem of satisfiability modulo the theory of real numbers, thus these techniques are relevant for SMT solving also.},
series = {LNAI},
volume = {12833},
pages = {130--134},
publisher = {Springer},
isbn_issn = {978-3-030-81096-2},
year = {2021},
month = {July},
editor = {F. Kamaredine and C. Sacerdoti Coen},
refereed = {yes},
keywords = {Satisfiability Checking, Natural-style Proofs, Computer Algebra, Symbolic Computation, Satisfiability Modulo Theories},
length = {5},
conferencename = {Intelligent Computer Mathematics, 14th International Conference, CICM 2021}
}
[Kutsia]

9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), short and work-in-progress papers

Temur Kutsia (editor)

Technical report no. 21-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6359,
author = {Temur Kutsia (editor)},
title = {{9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), short and work-in-progress papers}},
language = {english},
abstract = {This collection contains short and work-in-progress papers presented at the 9th International Symposium on Symbolic Computation in Software Science, SCSS 2021.},
number = {21-16},
year = {2021},
month = {August},
keywords = {Symbolic computation, software science, artificial intelligence},
length = {56},
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)}
}
[Maletzky]

A generic and executable formalization of signature-based Gröbner basis algorithms

Alexander Maletzky

J. Symb. Comput. 106, pp. 23-47. 2021. Elsevier, ISSN 0747-7171. arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001. [url]
[bib]
@article{RISC6225,
author = {Alexander Maletzky},
title = {{A generic and executable formalization of signature-based Gröbner basis algorithms}},
language = {english},
journal = {J. Symb. Comput.},
volume = {106},
pages = {23--47},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
note = {arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001},
refereed = {yes},
length = {25},
url = {https://arxiv.org/abs/2012.02239}
}
[Pau]

Proximity-Based Unification and Matching for Full Fuzzy Signatures

Temur Kutsia, Cleo Pau

Technical report no. 21-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@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)}
}
[Pau]

Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures

Temur Kutsia, Cleo Pau

Technical report no. 21-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@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)}
}
[Pau]

Proximity-Based Unification and Matching for Fully Fuzzy Signatures

Cleo Pau, Temur Kutsia

In: Proceedings of the 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021, , pp. 1-6. 2021. IEEE, isbn 978-1-6654-4407-1. [doi] [pdf]
[bib]
@inproceedings{RISC6369,
author = {Cleo Pau and Temur Kutsia},
title = {{Proximity-Based Unification and Matching for Fully Fuzzy Signatures}},
booktitle = {{Proceedings of the 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021}},
language = {english},
pages = {1--6},
publisher = {IEEE},
isbn_issn = {isbn 978-1-6654-4407-1},
year = {2021},
editor = { },
refereed = {yes},
length = {6},
url = {https://doi.org/10.1109/FUZZ45933.2021.9494438}
}
[Reichl]

Semantic Evaluation versus SMT Solving in the RISCAL Model Checker

Wolfgang Schreiner, Franz-Xaver Reichl

Technical report no. 21-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@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)}
}
[Reichl]

First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving

Wolfgang Schreiner, Franz-Xaver Reichl

In: Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021, Temur Kutsia (ed.), Electronic Proceedings in Theoretical Computer Science 342, pp. 99-113. September 2021. ISSN 2075-2180. [doi]
[bib]
@inproceedings{RISC6361,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving}},
booktitle = {{Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021}},
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 approach of semantic evaluation (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation of the two approaches and a discussion of their 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, we identify classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room for improvements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {342},
pages = {99--113},
isbn_issn = {ISSN 2075-2180},
year = {2021},
month = {September},
editor = {Temur Kutsia},
refereed = {yes},
keywords = {model checking, SMT solving, first-order logic, automated reasoning, formal methods},
sponsor = {e JKU Linz LIT Project LOGTECHEDU, Aktion Österreich-Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255},
length = {15},
url = {https://doi.org/10.4204/EPTCS.342.9}
}
[Schreiner]

Thinking Programs

Wolfgang Schreiner

Texts & Monographs in Symbolic Computation 1st edition, 2021. Springer, Cham, Switzerland, Hardcover ISBN 978-3-030-80506-7, Softcover ISBN 978-3-030-80509-8, eBook ISBN 978-3-030-80507-4. [doi]
[bib]
@book{RISC6371,
author = {Wolfgang Schreiner},
title = {{Thinking Programs}},
language = {english},
series = {Texts & Monographs in Symbolic Computation},
publisher = {Springer},
address = {Cham, Switzerland},
isbn_issn = {Hardcover ISBN 978-3-030-80506-7, Softcover ISBN 978-3-030-80509-8, eBook ISBN 978-3-030-80507-4},
year = {2021},
edition = {1st},
translation = {0},
length = {636},
url = {https://doi.org/10.1007/978-3-030-80507-4}
}

Loading…