QuodLibet's, CP's, and Friends'
Selected Publications by Subject

(chronological order; TP = Theorem Proving; PNC = Positive/Negative-Conditional)
Title and ... Contains Material on Subject ...
Location "Specification" "Confluence Criteria" "TP"

Lyonel Feininger's Process of Creation: from Thumbnail-Sketches without Nostalgia to Cubism in Umpferstedt, High Houses, and the Yellow Village Church
A Most Interesting Draft for Hilbert and Bernays' "Grundlagen der Mathematik"
that never found its way into any publication, and 2 CV of Gisbert Hasenjaeger
Barry Hartley Slater (1936--2016): A Logical Obituary
The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating C[5]

A Simplified and Improved Free-Variable Framework for
Hilbert's epsilon as an Operator of Indefinite Committed Choice

 		S[8,19] T[19,26]

A Series of Revisions of David Poole's Specificity

 S[25,28] T[25,28]
Herbrand's Fundamental Theorem --- an encyclopedia article T[24,27]

Herbrand's Fundamental Theorem:
The Historical Facts and their Streamlining

 		T[22,24]

Automation of Mathematical Induction as part of the History of Logic

 		S[26] T[26]
David Poole's Specificity Revised S[25] T[25]
Herbrand's Fundamental Theorem in the Eyes of Jean van Heijenoort T[22,24]

Human-Oriented Inductive Theorem Proving by Descente Infinie -- a manifesto

 T[17]

lim+, delta+, and Nonpermutability of beta-Steps

 T[12]

Hilbert, Bernays: Grundlagen der Mathematik

 		T[21]

Lectures on Jacques Herbrand as a Logician

 		T[20,22,23]

Shallow Confluence of Conditional Term Rewriting Systems

 S[10] C[1,2,4]
Jacques Herbrand: Life, Logic, and Automated Deduction T[20,22]

Hilbert's epsilon as an Operator of Indefinite Committed Choice

 S[8] T[19]
Thomas S. Kuhn: The Structure of Scientific Revolutions --- Zweisprachige Auszüge mit Deutschem Kommentar
A Self-Contained Discussion of Fermat's Only Explicitly Known Proof by Descente Infinie T[18]
Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie? T[17]
Flexible Heuristic Control for Combining Automation and User-Interaction in Inductive Theorem Proving T[11,13,15,16]

Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous

 T[13,15]
A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity T[14]
Mandatory versus Forbidden Literals in Simplification with Conditional Lemmas T[13]
An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving T[11]
The New Standard Tactics of the Inductive Theorem Prover QuodLibet T[10]
How to Prove Inductive Theorems? QuodLibet! S[1,2] T[9]
History and Future of Implicit and Inductionless Induction: Beware the old jade and the zombie! T[8]

A Systematic Study of Gröbner Basis Methods

 * *

On Gröbner Bases in Monoid and Group Rings

 * *

Descente Infinie + Deduction

 T[3,4,5,8]
Proof Development with Omega T[7]
A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations S[1,2] simplified and nice; S[7] C[2] simplified T[6]
Improving ASF+ S[6]
An Algebraic Dexter-Based Hypertext Reference Model S[5]
Full First-Order Free Variable Sequents and Tableaus in Implicit Induction T[4]
Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization T[3]

PNC Equations: A Constructor-Based Framework for Specification and Inductive TP

 S[1,2] with improved presentation and discussion C[1,2] simplified and improved T[1,2] with improved presentation and discussion

Conditional Equational Specifications of Data Types with Partial Operations for Inductive TP

 S[1,2] simplified and nice C[2] simplified

Confluence of Terminating Conditional Term Rewriting Systems Revisited

 C[1] simplified, complete proof
Inductive TP in Theories Specified by PNC Equations T[2] obsolete
Syntactic Confluence Criteria for PNC Term Rewriting Systems C[1,2,3]
very hard to read, complete proofs
Abstract Notions and Inference Systems for Proofs by Mathematical Induction T[1]
Writing PNC Equations Conveniently S[4]
ASF+   -   eine ASF-ähnliche Spezifikationssprache S[3]

On Notions of Inductive Validity for First-Order Equational Clauses

 S[2]

A Constructor-Based Approach for PNC Equational Specifications

 S[1] partly obsolete