Open_Induction Dependents

2018

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Nov 23

2015

Decreasing Diagrams II

by Bertram Felgenhauer

Aug 20

2012

Well-Quasi-Orders

by Christian Sternagel

Apr 13

2011

The Myhill-Nerode Theorem Based on Regular Expressions

by Chunhan Wu, Xingyuan Zhang and Christian Urban

Aug 26