SEKI REPORTS (ISSN 14374447) and
SEKI WORKINGPAPERS (ISSN 18605931)
(listing, complete since 2003)
 Title
 A Most Interesting Draft for Hilbert and Bernays'
"Grundlagen der Mathematik"
that never found its way into any publication,
and 2 CV of Gisbert Hasenjaeger
 Authors
 ClausPeter Wirth
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Wilfried Sieg
 Title
 The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating
 Authors

ClausPeter Wirth
 Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 IfCoLog J. of Logics and their Applications
 Improved Version
 IfCoLog J. of Logics and their Applications, 2017, Vol. 4, pp. 527547
 Cite improved version as
 Bibtex Entry Improved Version
 Title
 Herbrand's Fundamental Theorem  an encyclopedia article
 Authors

ClausPeter Wirth
 Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 Michael Nedo
 Title
 Herbrand's Fundamental Theorem: The Historical Facts and their Streamlining
 Authors

ClausPeter Wirth
 Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 Logica Universalis
 Title
 Automation of Mathematical Induction as part of the History of Logic
 Authors

J Strother Moore,
ClausPeter Wirth
 Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 Alan Bundy,
Bernhard Gramlich
 Journal Version
 IfCoLog J. of Logics and their Applications, 2017, Vol. 4, pp. 15051634
 Cite journal version as
 Bibtex Entry Journal Version
 Title
 David Poole's Specificity Revised
 Authors
 ClausPeter Wirth,
Frieder Stolzenburg
 Keywords
 Specificity, Logic Programming, Defeasible Reasoning,
NonMonotonic Reasoning
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Frieder Stolzenburg
 Short Version
 Proc.
KR 2014: 14th International Conference on Principles of Knowledge Representation and Reasoning, 2024 July 2014, Vienna, pp. 168177
 Slides
 Talk at KR2014
 Title
 A Simplified and Improved FreeVariable Framework
for Hilbert's epsilon as an Operator of Indefinite Committed Choice
 Authors
 ClausPeter Wirth
 Keywords
 Logical Foundations; Theories of Truth and Validity; Formalized Mathematics; HumanOriented Interactive Theorem Proving; Automated Theorem Proving; Hilbert's epsilonOperator; Henkin Quantification; Fermat's Descente Infinie
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Murdoch J. Gabbay
 Further Reading

 Journal Version
 IfCoLog J. of Logics and their Applications, 2017, Vol. 4, pp. 435526
 Cite journal version as
 Bibtex Entry Journal Version
 Title
 Automating Quantified Multimodal Logics in Simple Type Theory  A Case Study
 Authors
 Christoph Benzmüller
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by ClausPeter Wirth
 Title
 GranularityAdaptive Proof Presentation
 Authors
 Marvin Schiller and Christoph Benzmüller
 Keywords
 Adaptive proof presentation, proof tutoring, automated reasoning, machine learning, granularity
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by ClausPeter Wirth
 Title
 Quantified Multimodal Logics in Simple Type Theory
 Authors
 Christoph Benzmüller and Lawrence C. Paulson
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by ClausPeter Wirth
 Title
 Lectures on Jacques Herbrand as a Logician
 Authors
 ClausPeter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier
 Keywords
 Jacques Herbrand, History of Logic, Herbrand's Fundamental Theorem, Modus Ponens Elimination, LöwenheimSkolemTheorem, Falsehood in an infinite domain, Consistency of Arithmetic, Recursive Functions, Unification Algorithm
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Irving H. Anellis, Paolo Bussotti, and Lawrence C. Paulson
 Title
 On Requirements for Programming Exercises from an eLearning Perspective
 Authors
 Carlos LoriaSaenz
 Keywords
 Programming exercises, CS1, eLearning, ActivMath, Bloom's Taxonomy
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Jörg Siekmann
 Title
 Automating Access Control Logics in Simple Type Theory with LEOII
 Authors
 Christoph Benzmüller
 Keywords
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by ClausPeter Wirth
 Title
 Thomas S. Kuhn: The Structure of Scientific Revolutions  Zweisprachige Auszüge mit Deutschem Kommentar
 Authors
 ClausPeter Wirth
 Keywords
 Abstract
 Although Kuhn's s essay ``The Structure of Scientific Revolutions'' may well be the most important text in theory of science, today's scientists still tend to know only some catchwords from it, and methodological education of scientists hardly goes beyond Popper's Critical Rationalism. The reason for this poor state of affairs may be the length and lack of structure of Kuhn's essay, and the occasional difficulty to understand it. We present a arranged set of German comments and bilingual quotations from Kuhn's original essay in English and German. This compilation aims at delivering the essence of the essay, and thereby filling the gap of an easy, straightforward, and efficient accessibility of the subject.
 Zusammenfassung
 Obwohl Kuhns Essay ``Die Struktur wissenschaftlicher Revolutionen'' vielleicht den wichtigsten Text der Wissenschaftstheorie darstellt, kennen die heutigen Wissenschaftler meist nur ein paar Schlagworte daraus, und die methodologische Erziehung von Wissenschaftlern geht kaum über den Kritischen Rationalismus Poppers hinaus. Die Ursache für diesen Missstand dürfte in der Länge und der Unstrukturiertheit von Kuhns Essay liegen, sowie in dessen gelegentlicher Schwerverständlichkeit. Wir legen hier eine Sammlung von Deutschen Kommentaren und zweisprachigen Originalzitaten aus Kuhns Essay in Englisch und Deutsch vor. Diese Zusammenstellung hat das Ziel, eine Essenz des Essays abzuliefern und dabei dem Mangel an leichter, direkter und effizienter Zugänglichkeit des Themas abzuhelfen.
 Full Paper
 PDF
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Paolo Bussotti and Marvin Schiller
 Authors
 Chad E. Brown
 Title
 Dependently Typed Set Theory
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Abstract
 Dependently Typed Set Theory (DeTSeT) is untyped set theory encoded in a
dependent type theory.
The dependent type theory includes proof irrelevance and a special
Sigmatype between objects and proofs. This allows one to create a ``class
type''
from any predicate on the untyped universe of sets.
Given this rich type structure, one can represent partial functions as total
functions
on the appropriately restricted domain.
Set theory can be encoded as a finite signature in the type theory.
Furthermore, the signature is essentially
secondorder (in the lambdacalculus sense).
We develop the basic theory of DeTSeT and a signature for mathematics.
 Review
 Serge Autexier
 Full paper



 Format
 all.ps.gz
 Size
 .3 Mbytes

 Format
 all.dvi.gz
 Size
 .1 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 pdf.pdf
 Size
 .4 Mbytes
 Title
 A SelfContained and Easily Accessible Discussion of the Method of Descente Infinie and Fermat's Only Explicitly Known Proof by Descente Infinie
 Authors
 ClausPeter Wirth
 Keywords
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Paolo Bussotti
 Further Reading

 Title
 Progress in ComputerAssisted Inductive Theorem Proving by HumanOriented Proof Construction and Descente Infinie?
 Authors
 ClausPeter Wirth
 Keywords
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Dieter Hutter, Peter Padawitz, and Tobias SchmidtSamoa
 Further Reading

 Related Talk: Ceterum censeo Descente Infinie esse disputandam
 Revised Journal version:
 Authors
 ClausPeter Wirth
 Title

HumanOriented Inductive Theorem Proving by Descente Infinie  a manifesto
 In
 Logic J. of the IGPL.
http://dx.doi.org/10.1093/jigpal/jzr048
 Abstract

In this position paper, we briefly review the development
of automated inductive theorem proving and
computerassisted mathematical induction.
We think that the
current low expectations on progress in this field result
from a faulty projection.
On an abstract but hopefully sufficiently
descriptive level, we explain
why we believe that future progress in the field is to result
from humanorientedness and descente infinie
 Keywords

Automated Theorem Proving,
HumanOriented Theorem Proving,
Mathematical Induction,
Fermat's Descente Infinie,
Recursion Analysis,
Rippling,
Proof Planning
 Title
 Hilbert's epsilon as an Operator of Indefinite Committed Choice
 Authors
 ClausPeter Wirth
 Keywords
 Hilbert's epsilon Operator, Logical Foundations, Theories of Truth and Validity, Formalized Mathematics, HumanOriented Interactive Theorem Proving, Automated Theorem Proving, Formal Philosophy of Language, Computational Linguistics
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 Complete summary of anonymous review of a short version for TABLEAU 2002
 Journal Version

 Cite as
 Journal of Applied Logic 6 (2008), pp. 287317
Bibtex Entry
 Permanent URL
 http://dx.doi.org/10.1016/j.jal.2007.07.009
 Short version

 Cite as
 11th TABLEAU 2002, LNAI 2381, pp. 298314, Springer
Bibtex Entry
 Full Paper
 Submitted version in .ps.gz
 Authors
 Christoph Benzmüller,
Chad E. Brown,
Michael Kohlhase
 Title
 CutSimulation in Impredicative Logics
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Abstract

We investigate cutelimination and cutsimulation in impredicative
(higherorder) logics.
We illustrate that adding simple axioms such as Leibniz equations
to a calculus for an impredicative logicin our case a sequent calculus for
classical type theoryis like adding cut.
The phenomenon equally applies to prominent axioms like Boolean
and functional extensionality, induction, choice, and description.
This calls for the development of calculi where these principles are builtin
instead of being treated axiomatically.
 Review
 by ClausPeter Wirth
 Full paper

We have removed this paper from the WWW because the journal version
of this paper renders this paper obsolete.
 Title
 Designing a GUI for Proofs  Evaluation of an HCI Experiment
 Authors
 Martin Homik, Andreas Meier
 Abstract and Full Paper
 arXiv
 Copyright Owner
 SEKI
 Review
 Reviewed by Chad E. Brown and ClausPeter Wirth
 Authors
 Dominik Dietrich, Serge Autexier
 Title
 A CalculusIndependent Proof Data Structure
 Copyright Owner
 SEKI
 Abstract

A practically useful mathematics assistance system requires the
sophisticated combination of interaction and automation. Central in
such a system is the proof data structure, which has to maintain the
current proof state and which has to allow the flexible interplay of
various components including the human user. We describe a
parameterized proof data structure for the management of proofs,
which includes our experience with the development of two proof
assistants. It supports and bridges the gap between
abstract level proof explanation and lowlevel proof verification.
The proof data structure enables, in particular, the flexible
handling of lemmas, the maintenance of different proof alternatives,
and the representation of different granularities of proof attempts.
 Review
 ClausPeter Wirth
 Full paper



 Format
 all.ps.gz
 Size
 .6 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .6 Mbytes
 Authors
 ClausPeter Wirth
 Title
 Consistency of Recursive Definitions
via Shallow Confluence of
NonTerminating NonOrthogonal
Conditional Term Rewriting Systems
with any kind of Extra Variables
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Abstract
 Recursive definitions can be adequately and conveniently modeled with
leftlinear conditional term rewriting systems,
provided that nontermination, nontrivial critical pairs,
and extra variables are admitted.
Confluence of such systems guarantees
the objectlevel consistency of the underlying data types.
We present a novel sufficient criterion for shallow confluence,
a property which is logically stronger than level confluence and confluence,
and which is not only needed as a generalization for the hard inductive
proof of the sufficiency of the criterion,
but has other applications also, e.g. in functional logic programming.
By restricting the introduction of extra variables to binding equations that
mirror local variabledeclarations and constructormatching
variableintroduction constructs in programming languages
(such as let and case in ml),
and by requiring the critical pairs to have somehow complementary
literals in their conditions, we arrive at the first decidable
confluence criterion with which we can write
recursive function definitions adequately and conveniently:
It admits nontermination; nontrivial critical pairs;
extra variables in righthandsides introduced by binding equations and
arbitrary extra variables in conditions; and
nonproperorientation,
nonrightstability, and nonnormality of conditional equations.
 Full paper
 We have removed this paper from the WWW because the journal version
of this paper is such a huge improvement that it
renders this paper obsolete.
 Title
 lim+, delta+, and NonPermutability of betaSteps
 Authors
 ClausPeter Wirth
 Keywords
 Mathematics Assistance Systems,
Automated Theorem Proving,
HumanOriented ComputerAssisted Proof Construction,
Formal Proofs of Standard Theorems,
Reductive Calculi (Sequent, Tableau, Matrix, Indexed Formula Tree),
\NonPermutability\ of Reductive Inference Rules,
Liberalized deltarules,
deltaplusrule,
FreeVariable Calculi,
MSC 03F07,
MSC 03A99
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Chad E. Brown
 Journal Version
 Thoroughly revised!
 Authors
 Mark Buckley, Christoph Benzmüller
 Title
 A Diaologue Manager for the DIALOG Demonstrator
 Copyright Owner
 SEKI
 Abstract

The DIALOG project investigates flexible natural language tutorial dialogue in mathematics,
and as such it is essential that the system includes a dedicated module to facilitate and control
interaction with the tutor. In this report we present the design and implementation of the dialogue
manager for the demonstrator system of the DIALOG project. We begin with a brief survey of some
approaches to dialogue management, followed by an overview of the system and a description of the
modules which are part of the demonstrator. The dialogue manager is an information state update based
manager built on a platform for dialogue management applications called Rubin. We describe the
functionality of the Rubin platform before giving the specification of the dialogue manager itself,
including its input rules and the structure of the information state. Finally we discuss some aspects
of the system, its implementation, and the pros and cons of using the Rubin platform.
 Review
 Reviewed by Dimitra Tsovaltzi
 Full paper


 Format
 .ps.gz
 Size
 .28 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .04 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .58 Mbytes
 Authors
 Erica Melis, Carsten Ullrich
 Title
 GenderBiased Adaptations in Educational Adaptive Hypermedia
 Copyright Owner
 SEKI
 Abstract

Studies show that there is a statistically significant gender
difference regarding computer usage. For instance, a majority of female
users expect less success from an interaction with a computer and are
more likely to blame themselves in case something goes wrong. As a
result, women considerably less often use a computer as a tool than men
do. Now, if women do not use a computer as much as men do, they will
not profit as much from the advantages of computational systems as they
potentially could. That's why this paper reviews work about the causes
of this problem, investigates an extended model, and develops possible
preventions and reactions to it. Appropriate adaptivity cannot,
however, be based on mere gender information which represents a bias
only and may imply cliches and discrimination. Adapting a system solely
depending on the sex of the user could have the effect all users  men
and women  will feel discriminated by facing a system that embodies a
cliche. We think that an adaptive system with an appropriate user model
can help to avoid a clichebased treatment: the sex of a student is
only used to initialize the user model and as soon as more detailed
information about the aptitudes of the user is gained from his/her
interaction, the initial values of the user model are refined.
Moreover, the user should be in control about the behavior of the
system at any time.
 Review
 Third International Conference on Adaptive Hypermedia and Adaptive WebBased Systems;
Eindhoven, Netherlands
 Full paper


 Format
 .ps.gz
 Size
 .12 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .02 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .20 Mbytes
 Authors
 Andreas Meier, Erica Melis
 Title
 Proof Planning Limit Problems with Multiple Strategies
 Copyright Owner
 SEKI
 Abstract

The development of proof planning in the OMEGA system was and is strongly
influenced by the still ongoing case study on limit problems. In this report
we describe the application of OMEGA's recent proof planning approach, which is
called proof planning with multiple strategies, to problems from the limit
domain. In particular, we point out how drawbacks we encountered with the previous
proof planner of OMEGA when applied to limit problems motivated and influenced
the development of proof planning with multiple strategies.
 Review
 Reviewed by Martin Pollet
 Full paper


 Format
 .ps.gz
 Size
 .34 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .10 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .56 Mbytes
 Authors
 Andreas Meier
 Title
 The Proof Planners of OMEGA: A Technical Description
 Copyright Owner
 SEKI
 Abstract

The OMEGA proof development system employs proof planning for
automated proof construction at the abstract level of methods.
In this report we discuss the technical concepts underlying
proof planning in OMEGA and five detailed descriptions of the
algorithms of the two proof planners of the OMEGA system: PLAN
which performs simple proof planning with methods and MULTI which
performs multiplestrategy proof planning.
 Review
 Reviewed by Erica Melis
 Full paper


 Format
 .ps.gz
 Size
 .43 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .15 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 1.19 Mbytes
 Author
 Jessi Lynn Berkelhammer
 Title
 A Proof Representation
 Copyright Owner
 SEKI
 Abstract

We present a proof presentation language to be used by the mediator
between an environment for writing mathematical documents and proof
assistants.
 Review
 Reviewed by Christoph Benzmüller
 Full paper


 Format
 .ps.gz
 Size
 .07 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .01 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .16 Mbytes
 Authors
 Tobias SchmidtSamoa
 Title
 The New Standard Tactics of the Inductive Theorem Prover QuodLibet
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Abstract
 QuodLibet is a tacticbased inductive theorem prover for the verification
of algebraic specifications of algorithms in the style of abstract
data types with positive/negativeconditional equations.
Its core system consists of a small inference machine kernel that
merely acts as a proof checker.
Automation is achieved with tactics written in QML
(QuodLibetMetaLanguage), an adapted imperative programming language.
In this paper, we describe QuodLibet's new standard tactics, a pool of
general purpose tactics provided with the core system that support
the user in proving inductive theorems.
We aim at clarifying the underlying ideas as well as explaining the
parameters with which the user can influence the behavior of the
tactics during the proof process.
One of the major achievements of this paper is the application of
conditional lemmas controlled by obligatory and mandatory literals.
This has drastically improved the degree of automation without
increasing the runtime significantly as will be illustrated by the
case studies.
Nevertheless, the degree of automation depends on the specification
style used.
Thus, we will also give some guidelines how to write specifications
and how to use the new tactics efficiently.
 Review
 Reviewed by ClausPeter Wirth
 Full paper



 Format
 all.ps.gz
 Size
 .3 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .5 Mbytes
 Authors
 Serge Autexier, Carsten Schürmann
 Title
 Disproving False Conjectures
 Copyright Owner
 SEKI
 Abstract

For automatic theorem provers it is as important to disprove false conjectures as
it is to prove true ones, especially if it is not known ahead of time if a formula
is derivable inside a particular inference system. Situations of this kind occur
frequently in inductive theorem proving systems where failure is a common mode of
operation. This paper describes an abstraction mechanism for firstorder logic over
an arbitrary but fixed term algebra to secondorder monadic logic with 0 successor functions.
The decidability of secondorder monadic logic together with our notion of abstraction
yields an elegant criterion that characterizes a subclass of unprovable conjectures.
 Review
 LPAR
 Full paper



 Format
 .ps.gz
 Size
 .15 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .03 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .20 Mbytes
 Authors
 Christoph Benzmüller (ed.)
 Title
 Systems for Integrated Computation and Deduction
 Interim Report of the Calculemus IHP Network
 Copyright Owner
 SEKI
 Abstract

Research on automated and interactive theorem proving aims at the
mechanization of logical reasoning. Aside from the development of logic
calculi it became rapidly apparent that the organization of proof
search on top of the calculi is an essential task in the design of
powerful theorem proving systems. Different paradigms of how to
organize proof search have emerged in that area of research, the
most prominent representatives are generally described by the
buzzwords: automated theorem proving, tactical theorem
proving and proof planning. Despite their paradigmatic
differences, all approaches share a common goal: to find a proof for
a given conjecture.
In this paper we start with a rational reconstruction of proof search
paradigms in the area of proof planning and tactical theorem proving.
Guided by similarities between software engineering and proof construction
we develop a uniform view that accommodates the various proof search
methodologies and eases their comparison. Based on this view, we propose
a unified framework that enables the combination of different
methodologies for proof construction to take advantage of their individual virtues
within specific phases of a proof construction.
 Review
 None.
 Full paper


 Format
 .pdf
 Size
 .99 Mbytes
 Authors
 Malte Hübner
 Title
 Interactive Theorem Proving with Indexed Formulas
 Copyright Owner
 SEKI
 Abstract

Since more than two decades research in interactive theorem proving (ITP)
has attracted growing interest. The primary application domains for ITPs range
from hard and software verification tools to mathematical tutor systems. To
support communication with the user in an adequate way these systems depend
on calculi that allow for the construction of human understandable and readable
proofs. However, most calculi that are used in current ITPs fall still short of
supporting the user in an optimal way. The reason is that they enforce the user
to construct proofs at a level that is far more detailed than the one that can be
found in human constructed proofs.Autexier [autexier03] has recently proposed
a new theorem proving framework that allows to model different logics and calculi
in an uniform way. In CORE, a proofstate is always represented as a single formula
that can be manipulated by the application of replacement rules that are generated
from the logical context of the subformula under transformation. This approach also
facilitates proof construction at the assertion level which is considered as more
closely matching the level at which humans construct proofs (see for instance [huang94]).
Together with CORE window inference technique this makes CORE a potentially well
suited basis for interactive theorem proving.This thesis tries to excerpt CORE potential
for interactive theorem proving by mapping important concepts of the established proof
syste OMEGA to CORE. A task structure is developed to present the context of a
subformula in an intuitive way to the user and to assist him in structuring proofs.
The development of a method interpreter makes it possible to specify abstract inference
steps declaratively and to encode proof strategies for the use in CORE. The adaptation
of OMEGA agentbased suggestion mechanism Oants to CORE helps the user with the
identification of applicable methods and replacement rules.
 Review
 Reviewed by Chris Benzmüller.
 Full paper


 Format
 .ps.gz
 Size
 .11 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .11 Mbytes
 Authors
 Carsten Ullrich
 Title
 Pedagogical Rules in ACTIVEMATH and their Pedagogical Foundations
 Copyright Owner
 SEKI
 Abstract

One added value an intelligent learning environment
offers over traditional learning
media is adaptivity to the individual needs of the user. ACTIVEMATH offers
adaptivity by dynamically assembling learning materials to a course
individually tailored to the learner's needs.
Its course generation uses pedagogical rules that declaratively
represent instructional knowledge. These rules are based on
instructional design theories, learning outcomes, and individual
differences.
This technical report serves to explain the pedagogical principles
behind the currently available rules and to describe the instantiation of
these principles
in the rules of ACTIVEMATH.
 Review
 Reviewed by Erica Melis.
 Full paper


 Format
 .ps.gz
 Size
 .11 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .02 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .11 Mbytes
 Authors
 Serge Autexier, C. Benzmüller, Dieter Hutter
 Title
 Towards a Framework to Integrate Proof Search Paradigms
 Copyright Owner
 SEKI
 Abstract

Research on automated and interactive theorem proving aims at the
mechanization of logical reasoning. Aside from the development of logic
calculi it became rapidly apparent that the organization of proof
search on top of the calculi is an essential task in the design of
powerful theorem proving systems. Different paradigms of how to
organize proof search have emerged in that area of research, the
most prominent representatives are generally described by the
buzzwords: automated theorem proving, tactical theorem
proving and proof planning. Despite their paradigmatic
differences, all approaches share a common goal: to find a proof for
a given conjecture.
In this paper we start with a rational reconstruction of proof search
paradigms in the area of proof planning and tactical theorem proving.
Guided by similarities between software engineering and proof construction
we develop a uniform view that accommodates the various proof search
methodologies and eases their comparison. Based on this view, we propose
a unified framework that enables the combination of different methodologies
for proof construction to take advantage of their individual virtues within
specific phases of a proof construction.
 Review
 None.
 Full paper


 Format
 .ps.gz
 Size
 .15 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .03 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .18 Mbytes
 Authors
 Quoc Bao Vo, Christoph Benzmüller and Serge Autexier
 Title
 An Approach to Assertion Application via Generalised Resolution
 Copyright Owner
 SEKI
 Abstract

In this paper we address assertion retrieval and application in
theorem proving systems or proof planning systems for classical
firstorder logic. Due to Huang the notion of assertion comprises
mathematical knowledge such as definitions, theorems, and axioms.
We propose a distributed mediator module between a mathematical
knowledge base KB and a theorem proving system TP which is
independent of the particular proof representation format of TP
and which applies generalised resolution in order to analyze the
logical consequences of arbitrary assertions for a proof context at
hand. Our approach is applicable also to the assumptions which are
dynamically created during a proof search process. It therefore
realises a crucial first step towards full automation of assertion
level reasoning. We discuss the benefits and connection of our
approach to proof planning and motivate an application in a project
aiming at a tutorial dialogue system for mathematics.
 Review
 None.
 Full paper


 Format
 .ps.gz
 Size
 .18 Mbytes
 The titlepage does not work in the following dvi version!
 Format
 .dvi.gz
 Size
 .04 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .27 Mbytes
 Title
 Syntactic Confluence Criteria for Positive/NegativeConditional Term Rewriting Systems
 Authors
 ClausPeter Wirth
 Keywords
 Shallow Confluence, Level Confluence
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Bernhard Gramlich
 Title
 ASF+  eine ASFähnliche Spezifikationssprache
 Authors
 Rüdiger Lunde, ClausPeter Wirth
 Keywords
 Algebraic Specification
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Bernhard Gramlich
 Title
 Writing Positive/NegativeConditional Equations Conveniently
 Authors
 ClausPeter Wirth, Rüdiger Lunde
 Keywords
 Algebraic Specification
 Abstract and Full Paper
 arXiv
 Cite as
 Bibtex Entry
 Copyright Owner
 SEKI
 Review
 by Bernhard Gramlich
 Title
 Authors
 ClausPeter Wirth,
Bernhard Gramlich,
Ulrich Kühler,
Horst Prote
 Keywords
 Positive/negativeconditional specification, partial specification, constructorbased semantics, initial model, free model, inductive validity, constructor variables, ordersorted algebras, consitent extension, positive/negativeconditional rewriting, confluence, termination.
 Abstract
 We study
algebraic
specifications given by finite sets \R\
of positive/negativeconditional equations
(i. e.
universally quantified firstorder
implications with a single equation in
the succedent and a conjunction of positive
and negative (i. e. negated)
equations in the antecedent).
The class of models of such a specification
\R\
does not
contain
in general
a minimum model
in the sense that it can be mapped to any
other model by some homomorphism.
We present a
constructorbased
approach
for assigning appropriate semantics
to such specifications.
We
introduce two
syntactic
restrictions:
firstly,
for a condition to be fulfilled we
require the evaluation values
of the terms of the negative equations
to be
in the
constructor subuniverse which contains the
set of evaluation
values of all constructor
ground terms;
secondly,
we restrict
the constructor equations
to have ``Horn''form
and to be ``constructorpreserving''.
A
reduction relation
for \R\
is defined,
which
allows to
generalize
the
fundamental
results for positiveconditional
rewrite systems,
which does not need to be noetherian
or restricted to ground terms,
and which is monotonic w. r. t.
consistent extension of the specification.
Under the assumption of confluence,
the factor algebra of the
ground term algebra modulo the congruence of
the reduction relation
is a minimal model which is
(beyond that)
the minimum of all models
that do not identify more
constructor ground terms than necessary.
To achieve decidability of reducibility
we define several kinds of compatibility
of \R\ with a reduction ordering
and
present a complete criticalpair
test a la KnuthBendix
for the
confluence of the reduction relation.
 Cite as
 Bibtex Entry
 Full Paper
 PDF (25MB)
 Copyright Owner
 SEKI
 Title
 Term Orderings With Status
 Authors
 Joachim Steinbach
 Keywords
 Homeomorphic embedding, Incrementality, KnuthBendix ordering, Lexicographical ordering, Multiset ordering, Path of subterms ordering, Recursive decomposition ordering, Recursive path ordering, Simplification ordering, Status, Termination, Term rewriting system, Wellfounded ordering.
 Abstract
 The effective calculation with term rewriting systems presumes termination. Orderings on terms are
able to guarantee termination. This report deals with some of those term orderings : Several path and
decomposition orderings and the KnuthBendix ordering. We pursue three aims : Firstly, known
orderings will get new definitions. In the second place, new ordering methods will be introduced :
We will extend existing orderings by adding the principle of status ([KL80]). Thirdly, the
comparison of the power as well as the time behaviour of all orderings will be presented.
More precisely, after some preliminary remarks to termination of rewrite systems we present the
ordering methods. All orderings are connected by an essential characteristic : Each operator
has a status that determines the order according to which the subterms are compared. We
will present the following wellknown orderings : The recursive path ordering with status (tKL80l),
the path of subterms ordering (tRu87l) and another path ordering with status (tKNSSsl). A new
recursive decomposition ordering with status will lead the catalogue of orderings introduced here. It
is different from that of [e84]. Moreover, we give a new definition based on decompositions of the
path of subterms ordering (see [St88a]). An extension by incorporating status to this ordering as
well as to the improved recursive decomposition ordering (cf. [Ru87]) will be a part of the paper. All
orderings based on decompositions will be presented in a new and simple style : The decomposition
of a term consists of terms only. The original definitions take tuples composed of three (or even
four) components. Additionally to path and decomposition orderings, we deal with the weight
oriented ordering (tKB7Ol) and incorporate status. Finally, important properties (simplification
ordering, stability w.r.t. substitutions, etc.) of the newly introduced orderings will be listed.
Besides the introduction of new orderings, another main point of this report is the comparison of the
power of these orderings, i.e. we will compare the sets of comparable terms for each combination of
two orderings. It turned out that the new version with status of the improved recursive
decomposition ordering (equivalent to the path ordering with status of tKNSS5l) is the most
powerful ordering of the class of path and decomposition orderings presented. This ordering and the
KnuthBendix ordering with status overlap.
The orderings are implemented in our algebraic specification laboratory TRSPEC and the completion
system COMTES. A series of experiments has been conducted to study the time behaviour of the
orderings. An evaluation of these chronometries concludes the paper.
 Cite as
 Bibtex Entry
 Full Paper
 PDF (62MB)
 Copyright Owner
 SEKI
If you find any bugs on this page, please do contact
the editor wirth(at)logic.at !