arXiv subjects

Sarah Winkler

Publications and source records attributed to Sarah Winkler.

25 records · Page 2Linked to original sources

arXiv2020

Tools in Term Rewriting for Education

Term rewriting is a Turing complete model of computation. When taught to students of computer science, key properties of computation as well as techniques to analyze programs on an abstract level are conveyed. This paper gives a swift introduction to term rewriting and presents several automatic tools to analyze term rewrite systems which were developed by the Computational Logic Group at the University of Innsbruck. These include the termination tool TTT2, the confluence prover CSI, the completion tools mkbTT and KBCV, the complexity tool TcT, the strategy tool AutoStrat, as well as FORT, an implementation of the decision procedure for the first-order theory for a decidable class of rewrite systems. Besides its applications in research, this software pool has also proved invaluable for teaching, e.g., in multiple editions of the International Summer School on Rewriting.

cs.LO↗

arXiv2020

Smarter Features, Simpler Learning?

Earlier work on machine learning for automated reasoning mostly relied on simple, syntactic features combined with sophisticated learning techniques. Using ideas adopted in the software verification community, we propose the investigation of more complex, structural features to learn from. These may be exploited to either learn beneficial strategies for tools, or build a portfolio solver that chooses the most suitable tool for a given problem. We present some ideas for features of term rewrite systems and theorem proving problems.

cs.LO↗

arXiv2019

Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements

These are the post-proceedings of the second ARCADE workshop, which took place on the 26th August 2019 in Natal, Brazil, colocated with CADE-27. ARCADE stands for Automated Reasoning: Challenges, Applications, Directions, Exemplary achievements. The goal of this workshop was to bring together key people from various sub-communities of automated reasoning--such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving---to discuss the present, past, and future of the field.

cs.LO↗

arXiv2019

Abstract Completion, Formalized

Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.

cs.LO↗

arXiv2018

Certified Ordered Completion

On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we give an Isabelle/HOL formalization of ordered rewriting and completion that comes with a formally verified certifier for ordered completion proofs. By validating generated proof certificates, our certifier increases the reliability of ordered completion tools.

cs.LO↗

arXiv2015

AC-KBO Revisited

Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this paper we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful version, and we modify the latter to amend its lack of monotonicity on non-ground terms. We further present new complexity results. An extension reflecting the recent proposal of subterm coefficients in standard Knuth-Bendix orders is also given. The various orders are compared on problems in termination and completion.

cs.LO↗

arXiv2012

CeTA - A Tool for Certified Termination Analysis

Since the first termination competition in 2004 it is of great interest, whether a proof that has been automatically generated by a termination tool, is indeed correct. The increasing number of termination proving techniques as well as the increasing complexity of generated proofs (e.g., combinations of several techniques, exhaustive labelings, tree automata, etc.), make certifying (i.e., checking the correctness of) such proofs more and more tedious for humans. Hence the interest in automated certification of termination proofs. This led to the general approach of using proof assistants (like Coq and Isabelle) for certification. We present the latest developments for IsaFoR/CeTA (version 1.03) which is the certifier CeTA, based on the Isabelle/HOL formalization of rewriting IsaFoR.

cs.LO↗