SEKI REPORTS (ISSN 1437-4447) and
SEKI WORKING-PAPERS (ISSN 1860-5931)
(listing, complete since 2003)



SEKI Report SR-2015-02

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

SEKI Report SR-2015-01

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

SEKI Report SR-2014-01

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

SEKI Report SR-2013-02

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

SEKI Report SR-2013-01

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

SEKI Report SR-2011-01

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

SEKI Working-Paper SWP-2009-02

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

SEKI Working-Paper SWP-2009-01

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

SEKI Report SR-2009-02

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

SEKI Report SR-2009-01

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

SEKI Working-Paper SWP-2008-01

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

SEKI Report SR-2008-01

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

SEKI Working-Paper SWP-2007-01

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

SEKI Working-Paper SWP-2006-03

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

SEKI Working-Paper SWP-2006-02

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

SEKI Working-Paper SWP-2006-01

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

SEKI Report SR-2006-02

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

SEKI Report SR-2006-01

Authors
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
Title
Cut-Simulation in Impredicative Logics
Cite as
Bibtex Entry
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.

SEKI Working-Paper SWP-2005-01

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

SEKI Report SR-2005-03

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

SEKI Report SR-2005-02

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.

SEKI Report SR-2005-01

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!NEW!

SEKI Report SR-2004-06

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

SEKI Report SR-2004-05

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

SEKI Report SR-2004-04

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

SEKI Report SR-2004-03

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

SEKI Report SR-2004-02

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

SEKI Report SR-2004-01

Authors
Tobias Schmidt-Samoa
Title
The New Standard Tactics of the Inductive Theorem Prover QuodLibet

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

SEKI Report SR-2003-06

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

SEKI Report SR-2003-05

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

SEKI Report SR-2003-04

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

SEKI Report SR-2003-03

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

SEKI Report SR-2003-02

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

SEKI Report SR-2003-01

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

SEKI Report SR-95-05

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

SEKI Working-Paper SWP-94-05

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

SEKI Working-Paper SWP-94-04

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

SEKI Report SR-93-05

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

SEKI Report SR-88-12

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 !