14 citations · 60 across the 17 of their papers we have counts for
8 papers · 2 filters
Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization
Claus-Peter Wirth
We present a combination of raising, explicit variable dependency representation, the liberalized delta-rule, and preservation of solutions for first-order deductive theorem provin…
An Algebraic Dexter-Based Hypertext Reference Model
Volker Mattick, Claus-Peter Wirth
We present the first formal algebraic specification of a hypertext reference model. It is based on the well-known Dexter Hypertext Reference Model and includes modifications with r…
lim+, delta+, and Non-Permutability of beta-Steps
Claus-Peter Wirth
Using a human-oriented formal example proof of the (lim+) theorem, i.e. that the sum of limits is the limit of the sum, which is of value for reference on its own, we exhibit a non…
Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems
Claus-Peter Wirth
We study the combination of the following already known ideas for showing confluence of unconditional or conditional term rewriting systems into practically more useful confluence…
Writing Positive/Negative-Conditional Equations Conveniently
Claus-Peter Wirth, Ruediger Lunde
We present a convenient notation for positive/negative-conditional equations. The idea is to merge rules specifying the same function by using case-, if-, match-, and let-expressio…
Hilbert's epsilon as an Operator of Indefinite Committed Choice
Claus-Peter Wirth
Paul Bernays and David Hilbert carefully avoided overspecification of Hilbert's epsilon-operator and axiomatized only what was relevant for their proof-theoretic investigations. Se…