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"
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


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


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


Hilbert, Bernays: Grundlagen der Mathematik


Lectures on Jacques Herbrand as a Logician


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

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

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


A Constructor-Based Approach for PNC Equational Specifications

S[1] partly obsolete