The QuodLibet Theorem Prover

Introduction

Originally, this page was only on the following joint paper, but now we have added some further material at the bottom.

Our joint paper on the first system demonstration on an international conference

Authors

Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth

Title

How to Prove Inductive Theorems? QuodLibet!

In

19th CADE 2003, LNAI 2741, pp. 328-333, Springer

Cite as

Bibtex Entry

Copyright Owner

Springer

Abstract

QuodLibet is a tactic-based inductive theorem proving system that meets today's standard requirements for theorem provers such as a command interpreter, a sophisticated graphical user interface, and a carefully programmed inference machine kernel that guarantees soundness. In essence, it is the synergetic combination of the features presented in the following sections that makes QuodLibet a system quite useful in practice; and we hope that it is actually as you like it, which is the Latin ``quod libet'' translated into English. We start by presenting some of the design goals that have guided the development of QuodLibet. Note that the system is not intended to pursue the push bottom technology for inductive theorem proving, but to manage more complicated proofs by an effective interplay between interaction and automation.

Full paper

• PDF
• PS.GZ

Orignal slides of the talk on QuodLibet at CADE, Miami, 2003

• Green background: PDF
• White background: PDF
• White background, but with overlays accumulated: PS.GZ

Slides of a QuodLibet Presentation in 2008

• Green background: PDF
• White background: PDF
• White background, but with overlays accumulated: PS.GZ

Further reading on QuodLibet (ordered by time of publication)

• The first confluence and consistency proof for what became QuodLibet's admissibility scheme for the definition of possibly partially specified and non-terminating functions via positive/negative-conditional equations:
  Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems
• Analysis of the logical design options for the later QuodLibet system:
  Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving
• The admissibility scheme for partial and non-terminating inductive function definitions:
  Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving
• The first QuodLibet theorem prover:
  A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations
• Assessment of the historical background of QuodLibet in Implicit Induction:
  History and Future of Implicit and Inductionless Induction: Beware the old jade and the zombie!
• The first refinement of QuodLibet:
  The New Standard Tactics of the Inductive Theorem Prover QuodLibet
• The closest integration of Linear Arithmetic into inductive theorem proving:
  An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving
• Most powerful lemma application control in automated inductive theorem proving:
  Flexible Heuristics for Simplification with Conditional Lemmas by Marking Formulas as Forbidden, Mandatory, Obligatory, and Generous
• The system state with its most flexible control and efficient user interaction, where the system stopped to ask the user most of the time at the points where the semantic knowledge of the users was most helpful to guide the proof, typically by providing the missing lemma:
  Flexible Heuristic Control for Combining Automation and User-Interaction in Inductive Theorem Proving
• On further progress over inductive theorem provers such as QuodLibet and ACL2:
  Progress in Computer-Assisted Inductive Theorem Proving by Human-Oriented Proof Construction and Descente Infinie?
• The hard induction proof (14 years after its first publication) of confluence and consistency of the even further extended admissibility scheme for inductive function definitions in QuodLibet, the most powerful function definition scheme that comes with fully automatic admissibility checking, admitting monotonic extension of partial and non-terminating function definitions:
  Shallow Confluence of Term Rewriting Systems
• The history of the automation of mathematical induction from NQTHM over ACL2 to QuodLibet:
  Automation of Mathematical Induction as part of the History of Logic

Screenshots and Photos

• QuodLibet Screenshot: PDF
• Jürgen Avenhaus at his emeritation party, 2003?: JPG
• Claus-Peter Wirth and Ulrich Kühler in the meeting room of the AG Avenhaus/Madlener, 1995?: JPG
• Tobias Schmidt-Samoa and Claus-Peter Wirth, 2003?: JPG