Logic/Rewriting

Subject Classification

ACM: Theory of computation~Equational logic and rewriting

2023

A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann and Elias Wenninger

Jun 01

2022

Reducing Rewrite Properties to Properties on Ground Terms

by Alexander Lochmann

Jun 02

The Generalized Multiset Ordering is NP-Complete

by René Thiemann and Lukas Schmidinger

Apr 20

First-Order Theory of Rewriting

by Alexander Lochmann and Bertram Felgenhauer

Feb 02

2021

A Formalization of Weighted Path Orders and Recursive Path Orders

by Christian Sternagel, René Thiemann and Akihisa Yamada

Sep 16

2020

A Formalization of Knuth–Bendix Orders

by Christian Sternagel and René Thiemann

May 13

Implementing the Goodstein Function in λ-Calculus

by Bertram Felgenhauer

Feb 21

2019

A Verified Code Generator from Isabelle/HOL to CakeML

by Lars Hupel

Jul 08

2018

Graph Saturation

by Sebastiaan J. C. Joosten

Nov 23

Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms

by Alexander Bentkamp

Oct 19

First-Order Terms

by Christian Sternagel and René Thiemann

Feb 06

2017

Monad normalisation

by Joshua Schneider, Manuel Eberl and Andreas Lochbihler

May 05

2016

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel

Nov 12

Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms

by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Nov 12

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Sep 23

The Z Property

by Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel

Jun 30

2015

Decreasing Diagrams II

by Bertram Felgenhauer

Aug 20

2013

Decreasing Diagrams

by Harald Zankl

Nov 01

2010

Abstract Rewriting

by Christian Sternagel and René Thiemann

Jun 14