SEKI REPORTS (ISSN 1437-4447) and
SEKI WORKING-PAPERS (ISSN 1860-5931)
(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
- Claus-Peter Wirth
- Abstract and Full Paper
- arXiv
- Cite as
- Bibtex Entry
- Copyright Owner
- SEKI
- Review
- by Wilfried Sieg
- Revised Journal Version in Siegener Beiträge zur Geschichte und Philosophie der Mathematik,
14:1-56 (2021)
- Gisbert Hasenjaeger and a Most Interesting Unpublished Draft for Hilbert and Bernays' Grundlagen der Mathematik
- Title
- The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating
- Authors
-
Claus-Peter 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. 527-547
- Cite improved version as
- Bibtex Entry Improved Version
- Title
- Herbrand's Fundamental Theorem --- an encyclopedia article
- Authors
-
Claus-Peter 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
-
Claus-Peter 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,
Claus-Peter 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. 1505-1634
- Cite journal version as
- Bibtex Entry Journal Version
- Title
- David Poole's Specificity Revised
- Authors
- Claus-Peter Wirth,
Frieder Stolzenburg
- Keywords
- Specificity, Logic Programming, Defeasible Reasoning,
Non-Monotonic 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, 20-24 July 2014, Vienna, pp. 168-177
- Slides
- Talk at KR2014
- Title
- A Simplified and Improved Free-Variable Framework
for Hilbert's epsilon as an Operator of Indefinite Committed Choice
- Authors
- Claus-Peter Wirth
- Keywords
- Logical Foundations; Theories of Truth and Validity; Formalized Mathematics; Human-Oriented Interactive Theorem Proving; Automated Theorem Proving; Hilbert's epsilon-Operator; 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. 435-526
- 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 Claus-Peter Wirth
- Title
- Granularity-Adaptive 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 Claus-Peter 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 Claus-Peter Wirth
- Title
- Lectures on Jacques Herbrand as a Logician
- Authors
- Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier
- Keywords
- Jacques Herbrand, History of Logic, Herbrand's Fundamental Theorem, Modus Ponens Elimination, Löwenheim-Skolem-Theorem, 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 e-Learning Perspective
- Authors
- Carlos Loria-Saenz
- Keywords
- Programming exercises, CS1, e-Learning, 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 LEO-II
- Authors
- Christoph Benzmüller
- Keywords
- Abstract and Full Paper
- arXiv
- Cite as
- Bibtex Entry
- Copyright Owner
- SEKI
- Review
- by Claus-Peter Wirth
- Title
- Thomas S. Kuhn: The Structure of Scientific Revolutions --- Zweisprachige Auszüge mit Deutschem Kommentar
- Authors
- Claus-Peter 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
Sigma-type 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
second-order (in the lambda-calculus 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 Self-Contained and Easily Accessible Discussion of the Method of Descente Infinie and Fermat's Only Explicitly Known Proof by Descente Infinie
- Authors
- Claus-Peter Wirth
- Keywords
- Abstract and Full Paper
- arXiv
- Cite as
- Bibtex Entry
- Copyright Owner
- SEKI
- Review
- by Paolo Bussotti
- Further Reading
-
- Title
- Progress in Computer-Assisted Inductive Theorem Proving by Human-Oriented Proof Construction and Descente Infinie?
- Authors
- Claus-Peter Wirth
- Keywords
- Abstract and Full Paper
- arXiv
- Cite as
- Bibtex Entry
- Copyright Owner
- SEKI
- Review
- by Dieter Hutter, Peter Padawitz, and Tobias Schmidt-Samoa
- Further Reading
-
- Related Talk: Ceterum censeo Descente Infinie esse disputandam
- Revised Journal version:
- Authors
- Claus-Peter Wirth
- Title
-
Human-Oriented 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
computer-assisted 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 human-orientedness and descente infinie
- Keywords
-
Automated Theorem Proving,
Human-Oriented 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
- Claus-Peter Wirth
- Keywords
- Hilbert's epsilon Operator, Logical Foundations, Theories of Truth and Validity, Formalized Mathematics, Human-Oriented 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. 287-317
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. 298-314, Springer
Bibtex Entry
- Full Paper
- Submitted version in .ps.gz
- Authors
- Christoph Benzmüller,
Chad E. Brown,
Michael Kohlhase
- Title
- Cut-Simulation in Impredicative Logics
- Copyright Owner
- SEKI
- Abstract
-
We investigate cut-elimination and cut-simulation in impredicative
(higher-order) logics.
We illustrate that adding simple axioms such as Leibniz equations
to a calculus for an impredicative logic---in our case a sequent calculus for
classical type theory---is 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 built-in
instead of being treated axiomatically.
- Review
- by Claus-Peter 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 Claus-Peter Wirth
- Authors
- Dominik Dietrich, Serge Autexier
- Title
- A Calculus-Independent 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 low-level 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
- Claus-Peter 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
- Claus-Peter Wirth
- Title
- Consistency of Recursive Definitions
via Shallow Confluence of
Non-Terminating Non-Orthogonal
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
left-linear conditional term rewriting systems,
provided that non-termination, non-trivial critical pairs,
and extra variables are admitted.
Confluence of such systems guarantees
the object-level 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 variable-declarations and constructor-matching
variable-introduction 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 non-termination; non-trivial critical pairs;
extra variables in right-hand-sides introduced by binding equations and
arbitrary extra variables in conditions; and
non-proper-orientation,
non-right-stability, and non-normality 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 Non-Permutability of beta-Steps
- Authors
- Claus-Peter Wirth
- Keywords
- Mathematics Assistance Systems,
Automated Theorem Proving,
Human-Oriented Computer-Assisted Proof Construction,
Formal Proofs of Standard Theorems,
Reductive Calculi (Sequent, Tableau, Matrix, Indexed Formula Tree),
\NonPermutability\ of Reductive Inference Rules,
Liberalized delta-rules,
deltaplus-rule,
Free-Variable 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
- Gender-Biased 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 cliche-based 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 Web-Based 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 multiple-strategy 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 Schmidt-Samoa
- Title
- The New Standard Tactics of the Inductive Theorem Prover QuodLibet
- Cite as
- Bibtex Entry
- Copyright Owner
- SEKI
- Abstract
- QuodLibet is a tactic-based inductive theorem prover for the verification
of algebraic specifications of algorithms in the style of abstract
data types with positive/negative-conditional 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
(QuodLibet-Meta-Language), 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 Claus-Peter 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 first-order logic over
an arbitrary but fixed term algebra to second-order monadic logic with 0 successor functions.
The decidability of second-order 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 proof-state 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 agent-based 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
first-order 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/Negative-Conditional Term Rewriting Systems
- Authors
- Claus-Peter 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, Claus-Peter Wirth
- Keywords
- Algebraic Specification
- Abstract and Full Paper
- arXiv
- Cite as
- Bibtex Entry
- Copyright Owner
- SEKI
- Review
- by Bernhard Gramlich
- Title
- Writing Positive/Negative-Conditional Equations Conveniently
- Authors
- Claus-Peter 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
- Claus-Peter Wirth,
Bernhard Gramlich,
Ulrich Kühler,
Horst Prote
- Keywords
- Positive/negative-conditional specification, partial specification, constructor-based semantics, initial model, free model, inductive validity, constructor variables, order-sorted algebras, consitent extension, positive/negative-conditional rewriting, confluence, termination.
- Abstract
- We study
algebraic
specifications given by finite sets \R\
of positive/negative-conditional equations
(i. e.
universally quantified first-order
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
constructor-based
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 sub-universe 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 ``constructor-preserving''.
A
reduction relation
for \R\
is defined,
which
allows to
generalize
the
fundamental
results for positive-conditional
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 critical-pair
test a la Knuth-Bendix
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, Knuth-Bendix ordering, Lexicographical ordering, Multiset ordering, Path of subterms ordering, Recursive decomposition ordering, Recursive path ordering, Simplification ordering, Status, Termination, Term rewriting system, Well-founded 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 Knuth-Bendix 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 well-known 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
Knuth-Bendix 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 !