A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications. - Claus-Peter Wirth; Bernhard Gramlich (CTRS, 1992)

On Notions of Inductive Validity for First-Oder Equational Clauses. - Claus-Peter Wirth; Bernhard Gramlich (CADE, 1994)

Abstract Notions and Inference Systems for Proofs by Mathematical Induction. - Claus-Peter Wirth; Klaus Becker 002 (CTRS, 1994)

A Constructor-Based Approach to Positive/Negative-Conditional Equational Specifications. - Claus-Peter Wirth; Bernhard Gramlich (J. Symb. Comput., 1994)

Confluence of Terminating Conditional Rewrite Systems Revisited. - Bernhard Gramlich; Claus-Peter Wirth (RTA, 1996)

Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. - Ulrich Kühler; Claus-Peter Wirth (RTA, 1997)

Positive negative conditional equations: a constructor-based framework for specification and inductive theorem proving. - Claus-Peter Wirth (Kovač, 1997)

Full First-Order Sequent and Tableau Calculi with Preservation of Solutions and the Liberalized delta-Rule but without Skolemization. - Claus-Peter Wirth (FTP (LNCS Selection), 1998)

Full First-Order Free Variable Sequents and Tableaux in Implicit Induction. - Claus-Peter Wirth (TABLEAUX, 1999)

Proof Development with OMEGA. - Jörg H. Siekmann; Christoph Benzmüller; Vladimir Brezhnev; Lassaad Cheikhrouhou; Armin Fiedler; Andreas Franke 001; Helmut Horacek; Michael Kohlhase; Andreas Meier 002; Erica Melis; Markus Moschner; Immanuel Normann; et al. (CADE, 2002)

A New Indefinite Semantics for Hilbert's Epsilon. - Claus-Peter Wirth (TABLEAUX, 2002)

How to Prove Inductive Theorems? QUODLIBET! - Jürgen Avenhaus; Ulrich Kühler; Tobias Schmidt-Samoa; Claus-Peter Wirth (CADE, 2003)

Descente Infinie + Deduction. - Claus-Peter Wirth (Log. J. IGPL, 2004)

History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie! - Claus-Peter Wirth (Mechanizing Mathematical Reasoning, 2005)

A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. - Serge Autexier; Christoph Benzmüller; Dominik Dietrich; Andreas Meier 002; Claus-Peter Wirth (MKM, 2005)

Hilbert's epsilon as an operator of indefinite committed choice. - Claus-Peter Wirth (J. Appl. Log., 2008)

Writing Positive/Negative-Conditional Equations Conveniently - Claus-Peter Wirth; Rüdiger Lunde (CoRR, 2009)

ASF+ — eine ASF-aehnliche Spezifikationssprache - Rüdiger Lunde; Claus-Peter Wirth (CoRR, 2009)

Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie? - Claus-Peter Wirth (CoRR, 2009)

Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems - Claus-Peter Wirth (CoRR, 2009)

A Self-Contained and Easily Accessible Discussion of the Method of Descente Infinie and Fermat's Only Explicitly Known Proof by Descente Infinie - Claus-Peter Wirth (CoRR, 2009)

lim+, delta+, and Non-Permutability of beta-Steps - Claus-Peter Wirth (CoRR, 2009)

An Algebraic Dexter-Based Hypertext Reference Model - Volker Mattick; Claus-Peter Wirth (CoRR, 2009)

Lectures on Jacques Herbrand as a Logician - Claus-Peter Wirth; Jörg H. Siekmann; Christoph Benzmüller; Serge Autexier (CoRR, 2009)

Shallow confluence of conditional term rewriting systems. - Claus-Peter Wirth (J. Symb. Comput., 2009)

Jacques Herbrand: Life, Logic, and Automated Deduction. - Claus-Peter Wirth; Jörg H. Siekmann; Christoph Benzmüller; Serge Autexier (Logic from Russell to Church, 2009)

Computer-assisted human-oriented inductive theorem proving by descente infinie - a manifesto. - Claus-Peter Wirth (Log. J. IGPL, 2012)

lim+, δ+, and Non-Permutability of β-Steps. - Claus-Peter Wirth (J. Symb. Comput., 2012)

HERBRAND's Fundamental Theorem in the Eyes of JEAN VAN HEIJENOORT. - Claus-Peter Wirth (Logica Universalis, 2012)

David Poole's Specifity Revised. - Claus-Peter Wirth; Frieder Stolzenburg (CoRR, 2013)

David Poole's Specificity Revised. - Claus-Peter Wirth; Frieder Stolzenburg (KR, 2014)

Herbrand's Fundamental Theorem: The Historical Facts and their Streamlining. - Claus-Peter Wirth (CoRR, 2014)

The RatioLog Project: Rational Extensions of Logical Reasoning. - Ulrich Furbach; Claudia Schon; Frieder Stolzenburg; Karl-Heinz Weis; Claus-Peter Wirth (Künstliche Intell., 2015)

Quantifiers in logic and proof-search using permissive-nominal terms and sets. - Murdoch James Gabbay; Claus-Peter Wirth (J. Log. Comput., 2015)

A series of revisions of David Poole's specificity. - Claus-Peter Wirth; Frieder Stolzenburg (Ann. Math. Artif. Intell., 2016)

Automation of Mathematical Induction as part of the History of Logic. - J Strother Moore; Claus-Peter Wirth (FLAP, 2017)

Barry Hartley Slater (1936-2016): A Logical Obituary. - Claus-Peter Wirth (FLAP, 2017)

A Simplified and Improved Free-variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice. - Claus-Peter Wirth (FLAP, 2017)

The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating. - Claus-Peter Wirth (FLAP, 2017)