default search action
Claus-Peter Wirth
Person information
- affiliation: Saarland University, Saarbrücken, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 1997
- [b1]Claus-Peter Wirth:
Positive negative conditional equations: a constructor-based framework for specification and inductive theorem proving. University of Kaiserslautern, Kovač 1997, ISBN 3-86064-551-X, pp. 1-246
Journal Articles
- 2017
- [j14]Claus-Peter Wirth:
Barry Hartley Slater (1936-2016): A Logical Obituary. FLAP 4(2) (2017) - [j13]Claus-Peter Wirth:
A Simplified and Improved Free-variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice. FLAP 4(2) (2017) - [j12]Claus-Peter Wirth:
The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating. FLAP 4(2) (2017) - [j11]J Strother Moore, Claus-Peter Wirth:
Automation of Mathematical Induction as part of the History of Logic. FLAP 4(5) (2017) - 2016
- [j10]Claus-Peter Wirth, Frieder Stolzenburg:
A series of revisions of David Poole's specificity. Ann. Math. Artif. Intell. 78(3-4): 205-258 (2016) - 2015
- [j9]Ulrich Furbach, Claudia Schon, Frieder Stolzenburg, Karl-Heinz Weis, Claus-Peter Wirth:
The RatioLog Project: Rational Extensions of Logical Reasoning. Künstliche Intell. 29(3): 271-277 (2015) - [j8]Murdoch James Gabbay, Claus-Peter Wirth:
Quantifiers in logic and proof-search using permissive-nominal terms and sets. J. Log. Comput. 25(2): 473-523 (2015) - 2012
- [j7]Claus-Peter Wirth:
Computer-assisted human-oriented inductive theorem proving by descente infinie - a manifesto. Log. J. IGPL 20(6): 1046-1063 (2012) - [j6]Claus-Peter Wirth:
lim+, δ+, and Non-Permutability of β-Steps. J. Symb. Comput. 47(9): 1109-1135 (2012) - [j5]Claus-Peter Wirth:
HERBRAND's Fundamental Theorem in the Eyes of JEAN VAN HEIJENOORT. Logica Universalis 6(3-4): 485-520 (2012) - 2009
- [j4]Claus-Peter Wirth:
Shallow confluence of conditional term rewriting systems. J. Symb. Comput. 44(1): 60-98 (2009) - 2008
- [j3]Claus-Peter Wirth:
Hilbert's epsilon as an operator of indefinite committed choice. J. Appl. Log. 6(3): 287-317 (2008) - 2004
- [j2]Claus-Peter Wirth:
Descente Infinie + Deduction. Log. J. IGPL 12(1): 1-96 (2004) - 1994
- [j1]Claus-Peter Wirth, Bernhard Gramlich:
A Constructor-Based Approach to Positive/Negative-Conditional Equational Specifications. J. Symb. Comput. 17(1): 51-90 (1994)
Conference and Workshop Papers
- 2014
- [c13]Claus-Peter Wirth, Frieder Stolzenburg:
David Poole's Specificity Revised. KR 2014 - 2005
- [c12]Claus-Peter Wirth:
History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie! Mechanizing Mathematical Reasoning 2005: 192-203 - [c11]Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth:
A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. MKM 2005: 126-142 - 2003
- [c10]Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth:
How to Prove Inductive Theorems? QUODLIBET! CADE 2003: 328-333 - 2002
- [c9]Jörg H. Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer:
Proof Development with OMEGA. CADE 2002: 144-149 - [c8]Claus-Peter Wirth:
A New Indefinite Semantics for Hilbert's Epsilon. TABLEAUX 2002: 298-314 - 1999
- [c7]Claus-Peter Wirth:
Full First-Order Free Variable Sequents and Tableaux in Implicit Induction. TABLEAUX 1999: 293-307 - 1998
- [c6]Claus-Peter Wirth:
Full First-Order Sequent and Tableau Calculi with Preservation of Solutions and the Liberalized delta-Rule but without Skolemization. FTP (LNCS Selection) 1998: 282-297 - 1997
- [c5]Ulrich Kühler, Claus-Peter Wirth:
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. RTA 1997: 38-52 - 1996
- [c4]Bernhard Gramlich, Claus-Peter Wirth:
Confluence of Terminating Conditional Rewrite Systems Revisited. RTA 1996: 245-259 - 1994
- [c3]Claus-Peter Wirth, Bernhard Gramlich:
On Notions of Inductive Validity for First-Oder Equational Clauses. CADE 1994: 162-176 - [c2]Claus-Peter Wirth, Klaus Becker:
Abstract Notions and Inference Systems for Proofs by Mathematical Induction. CTRS 1994: 353-373 - 1992
- [c1]Claus-Peter Wirth, Bernhard Gramlich:
A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications. CTRS 1992: 198-212
Reference Works
- 2009
- [r1]Claus-Peter Wirth, Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier:
Jacques Herbrand: Life, Logic, and Automated Deduction. Logic from Russell to Church 2009: 195-254
Informal and Other Publications
- 2016
- [i16]Claus-Peter Wirth:
The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating. CoRR abs/1611.06389 (2016) - 2015
- [i15]Ulrich Furbach, Claudia Schon, Frieder Stolzenburg, Karl-Heinz Weis, Claus-Peter Wirth:
The RatioLog Project - Rational Extensions of Logical Reasoning. CoRR abs/1503.06087 (2015) - 2014
- [i14]Claus-Peter Wirth:
Herbrand's Fundamental Theorem: The Historical Facts and their Streamlining. CoRR abs/1405.6317 (2014) - 2013
- [i13]Claus-Peter Wirth, Frieder Stolzenburg:
David Poole's Specifity Revised. CoRR abs/1308.4943 (2013) - [i12]J Strother Moore, Claus-Peter Wirth:
Automation of Mathematical Induction as part of the History of Logic. CoRR abs/1309.6226 (2013) - 2011
- [i11]Claus-Peter Wirth:
A Simplified and Improved Free-Variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice. CoRR abs/1104.2444 (2011) - 2009
- [i10]Claus-Peter Wirth, Rüdiger Lunde:
Writing Positive/Negative-Conditional Equations Conveniently. CoRR abs/0902.2975 (2009) - [i9]Rüdiger Lunde, Claus-Peter Wirth:
ASF+ --- eine ASF-aehnliche Spezifikationssprache. CoRR abs/0902.2995 (2009) - [i8]Claus-Peter Wirth:
Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie? CoRR abs/0902.3294 (2009) - [i7]Claus-Peter Wirth:
Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems. CoRR abs/0902.3614 (2009) - [i6]Claus-Peter Wirth:
A Self-Contained and Easily Accessible Discussion of the Method of Descente Infinie and Fermat's Only Explicitly Known Proof by Descente Infinie. CoRR abs/0902.3623 (2009) - [i5]Claus-Peter Wirth:
lim+, delta+, and Non-Permutability of beta-Steps. CoRR abs/0902.3635 (2009) - [i4]Volker Mattick, Claus-Peter Wirth:
An Algebraic Dexter-Based Hypertext Reference Model. CoRR abs/0902.3648 (2009) - [i3]Claus-Peter Wirth:
Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization. CoRR abs/0902.3730 (2009) - [i2]Claus-Peter Wirth:
Hilbert's epsilon as an Operator of Indefinite Committed Choice. CoRR abs/0902.3749 (2009) - [i1]Claus-Peter Wirth, Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier:
Lectures on Jacques Herbrand as a Logician. CoRR abs/0902.4682 (2009)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-25 05:59 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint