Arrow Research search

Author name cluster

Claus-Peter Wirth

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers
1 author row

Possible papers

5

FLAP Journal 2017 Journal Article

A Simplified and Improved Free-variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice.

  • Claus-Peter Wirth

Free variables occur frequently in mathematics and computer science with ad hoc and altering semantics. We present here the most recent version of our freevariable framework for two-valued logics with properly improved functionality, but only two kinds of free variables left (instead of three): implicitly universally and implicitly existentially quantified ones, now simply called “free atoms” and “free variables”, respectively. The quantificational expressiveness and the problem-solving facilities of our framework exceed standard first-order logic and even higher-order modal logics, and directly support Fermat’s descente infinie. With the improved version of our framework, we can now model also Henkin quantification, neither using any binders (such as quantifiers or epsilons) nor raising (Skolemization). Based only on the traditional ε-formula of Hilbert–Bernays, we present our flexible and elegant semantics for Hilbert’s ε as a choice operator with the following features: We avoid overspecification (such as right-uniqueness), but admit indefinite choice, committed choice, and classical logics. Moreover, our semantics for the ε supports reductive proof search optimally.

PDF Details

FLAP Journal 2017 Journal Article

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

  • Claus-Peter Wirth

We investigate the elimination of quantifiers in first-order formulas via Hilbert’s epsilon-operator (or -binder), following Bernays’ explicit definitions of the existential and the universal quantifier symbol by means of epsilon-terms. This elimination has its first explicit occurrence in the proof of the first epsilon-theorem in Hilbert–Bernays in 1939. We think that there is a lacuna in this proof w.r.t. this elimination, related to the erroneous assumption that explicit definitions always terminate. Surprisingly, to the best of our knowledge, nobody ever published a confluence or termination proof for this elimination procedure; and even myths on non-confluence and the openness of the termination problem are circulating. We show confluence and termination of this elimination procedure by means of a direct, straightforward, and easily verifiable proof, based on a theorem on how to obtain termination from weak normalization.

PDF Details

KR Conference 2014 Conference Paper

David Poole's Specificity Revised

  • Claus-Peter Wirth
  • Frieder Stolzenburg

David Poole (1985) has sketched such a notion as a binary relation on arguments and evaluated its intuitive validity with some examples. Poole’s notion of specificity was given a more appropriate formalization in (Simari and Loui 1992). The properties of this formalization were examined in detail in (Stolzenburg et al. 2003). In the middle of the 1980s, David Poole introduced a semantical, model-theoretic notion of specificity to the artificialintelligence community. Since then it has found further applications in non-monotonic reasoning, in particular in defeasible reasoning. Poole’s notion, however, turns out to be intricate and problematic, which — as we show — can be overcome to some extent by a closer approximation of the intuitive human concept of specificity. Besides the intuitive advantages of our novel specificity ordering over Poole’s specificity relation in the classical examples of the literature, we also report some hard mathematical facts: Contrary to what was claimed before, we show that Poole’s relation is not transitive. Our new notion of specificity is transitive and also monotonic w. r. t. conjunction.