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

QuodLibet's, CP's, and Friends' Selected Publications by Subject (chronlogical order; TP = Theorem Proving; PNC = Positive/Negative-Conditional)
Title and ...	Contains Material on Subject ...
Location	"Specification"	"Confluence Criteria"	"TP"
Human-Oriented Inductive Theorem Proving by Descente Infinie -- a manifesto			T[17]
lim+, delta+, and Nonpermutability of beta-Steps			T[12]
A Simplified and Improved Free-Variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice			T[19]
Hilbert, Bernays: Grundlagen der Mathematik			T[21]
Lectures on Jacques Herbrand as a Logician			T[20]
Shallow Confluence of Conditional Term Rewriting Systems		C[1,2,4]
Jacques Herbrand: Life, Logic, and Automated Deduction			T[20]
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

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

Descente Infinie + Deduction

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