QuodLibet's,
CP's, and Friends'
Selected Publications by Subject
(chronological order;
TP = Theorem Proving; PNC = Positive/NegativeConditional)

Title and ... 
Contains Material on Subject ... 
Location 
"Specification" 
"Confluence Criteria" 
"TP" 
A Most Interesting Draft for Hilbert and Bernays' "Grundlagen der Mathematik"
That Never Found Its Way into Publication, and a CV of Hasenjaeger 



Barry Hartley Slater (19362016): A Logical Obituary 



The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating 

C[5] 

A Simplified and Improved FreeVariable 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] 
HumanOriented Inductive Theorem Proving by Descente Infinie
 a manifesto 


T[17] 
lim+, delta+, and Nonpermutability of betaSteps 


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] 

S[8] 

T[19] 
Thomas S. Kuhn: The Structure of Scientific Revolutions 
Zweisprachige Auszüge mit Deutschem Kommentar




A SelfContained Discussion of
Fermat's Only Explicitly Known Proof
by Descente Infinie 


T[18] 
Progress in ComputerAssisted Inductive Theorem Proving by HumanOrientedness
and Descente Infinie? 


T[17] 
Flexible Heuristic Control for Combining
Automation and UserInteraction
in Inductive Theorem Proving 


T[11,13,15,16] 



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] 


* 
* 


* 
* 
Descente Infinie + Deduction 


T[3,4,5,8] 
Proof Development with Omega 


T[7] 
A TacticBased 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 DexterBased Hypertext Reference Model 
S[5] 


Full FirstOrder Free Variable Sequents and Tableaus in Implicit Induction 


T[4] 
Full FirstOrder Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized deltaRule but Without Skolemization 


T[3] 

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

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



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] 



S[2] 



S[1] 
partly obsolete 
