KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Sat, 04 Mar 2000 00:00:00 +0200Sat, 04 Mar 2000 00:00:00 +0200Classification and Learning of Similarity Measures
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/331
The background of this paper is the area of case-based reasoning. This is a reasoning technique where one tries to use the solution of some problem which has been solved earlier in order to obta in a solution of a given problem. As example of types of problems where this kind of reasoning occurs very often is the diagnosis of diseases or faults in technical systems. In abstract terms this reduces to a classification task. A difficulty arises when one has not just one solved problem but when there are very many. These are called "cases" and they are stored in the case-base. Then one has to select an appropriate case which means to find one which is "similar" to the actual problem. The notion of similarity has raised much interest in this context. We will first introduce a mathematical framework and define some basic concepts. Then we will study some abstract phenomena in this area and finally present some methods developed and realized in a system at the University of Kaiserslautern.Michael M. Richterpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/331Mon, 03 Apr 2000 00:00:00 +0200A Guide to UNICOM, an Inductive Theorem Prover Based on Rewriting and Completion Techniques
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/332
We provide an overview of UNICOM, an inductive theorem prover for equational logic which isbased on refined rewriting and completion techniques. The architecture of the system as well as itsfunctionality are described. Moreover, an insight into the most important aspects of the internalproof process is provided. This knowledge about how the central inductive proof componentof the system essentially works is crucial for human users who want to solve non-trivial prooftasks with UNICOM and thoroughly analyse potential failures. The presentation is focussedon practical aspects of understanding and using UNICOM. A brief but complete description ofthe command interface, an installation guide, an example session, a detailed extended exampleillustrating various special features and a collection of successfully handled examples are alsoincluded.Bernhard Gramlich; Wolfgang Lindnerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/332Mon, 03 Apr 2000 00:00:00 +0200goal-driven similarity assessment
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/333
While most approaches to similarity assessment are oblivious of knowledge and goals, there is ample evidence that these elements of problem solving play an important role in similarity judgements. This paper is concerned with an approach for integrating assessment of similarity into a framework of problem solving that embodies central notions of problem solving like goals, knowledge and learning.Stefan Wess; Erica Melis; Dietmar Janetzkopreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/333Mon, 03 Apr 2000 00:00:00 +0200On the Representation of Mathematical Concepts and their Translation into First-Order Logic
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/334
To prove difficult theorems in a mathematical field requires substantial know-ledge of that field. In this thesis a frame-based knowledge representation formal-ism including higher-order sorted logic is presented, which supports a conceptualrepresentation and to a large extent guarantees the consistency of the built-upknowledge bases. In order to operationalize this knowledge, for instance, in anautomated theorem proving system, a class of sound morphisms from higher-orderinto first-order logic is given, in addition a sound and complete translation ispresented. The translations are bijective and hence compatible with a later proofpresentation.In order to prove certain theorems the comprehension axioms are necessary,(but difficult to handle in an automated system); such theorems are called trulyhigher-order. Many apparently higher-order theorems (i.e. theorems that arestated in higher-order syntax) however are essentially first-order in the sense thatthey can be proved without the comprehension axioms: for proving these theoremsthe translation technique as presented in this thesis is well-suited.Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/334Mon, 03 Apr 2000 00:00:00 +0200Tactics for the Improvement of Problem Formulation in Resolution-Based Theorem Proving
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/335
We transform a user-friendly formulation of aproblem to a machine-friendly one exploiting the variabilityof first-order logic to express facts. The usefulness of tacticsto improve the presentation is shown with several examples.In particular it is shown how tactical and resolution theoremproving can be combined.Manfred Kerber; Axel Präckleinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/335Mon, 03 Apr 2000 00:00:00 +0200Conditional semi-Thue Systems for Presenting Monoids
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/336
There are well known examples of monoids in literature which do not admit a finite andcanonical presentation by a semi-Thue system over a fixed alphabet, not even over an arbi-trary alphabet. We introduce conditional Thue and semi-Thue systems similar to conditionalterm rewriting systems as defined by Kaplan. Using these conditional semi-Thue systems wegive finite and canonical presentations of the examples mentioned above. Furthermore weshow, that each finitely generated monoid with decidable word problem is embeddable in amonoid which has a finite canonical conditional presentation.Thomas Deißpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/336Mon, 03 Apr 2000 00:00:00 +0200Analogical Reasoning with Typical Examples
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/337
Typical examples, that is, examples that are representative for a particular situationor concept, play an important role in human knowledge representation and reasoning.In real life situations more often than not, instead of a lengthy abstract characteriza-tion, a typical example is used to describe the situation. This well-known observationhas been the motivation for various investigations in experimental psychology, whichalso motivate our formal characterization of typical examples, based on a partial orderfor their typicality. Reasoning by typical examples is then developed as a special caseof analogical reasoning using the semantic information contained in the correspondingconcept structures. We derive new inference rules by replacing the explicit informa-tion about connections and similarity, which are normally used to formalize analogicalinference rules, by information about the relationship to typical examples. Using theseinference rules analogical reasoning proceeds by checking a related typical example,this is a form of reasoning based on semantic information from cases.Manfred Kerber; Erica Melis; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/337Mon, 03 Apr 2000 00:00:00 +0200Methods - The Basic Units for Planning and Verifying Proofs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/338
This paper concerns a knowledge structure called method , within a compu-tational model for human oriented deduction. With human oriented theoremproving cast as an interleaving process of planning and verification, the body ofall methods reflects the reasoning repertoire of a reasoning system. While weadopt the general structure of methods introduced by Alan Bundy, we make anessential advancement in that we strictly separate the declarative knowledgefrom the procedural knowledge. This is achieved by postulating some stand-ard types of knowledge we have identified, such as inference rules, assertions,and proof schemata, together with corresponding knowledge interpreters. Ourapproach in effect changes the way deductive knowledge is encoded: A newcompound declarative knowledge structure, the proof schema, takes the placeof complicated procedures for modeling specific proof strategies. This change ofparadigm not only leads to representations easier to understand, it also enablesus modeling the even more important activity of formulating meta-methods,that is, operators that adapt existing methods to suit novel situations. In thispaper, we first introduce briefly the general framework for describing methods.Then we turn to several types of knowledge with their interpreters. Finally,we briefly illustrate some meta-methods.Xiaorong Huang; Manfred Kerber; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/338Mon, 03 Apr 2000 00:00:00 +0200Integration of Rewriting, Narrowing, Compilation, and Heuristics for Equality Reasoning in Resolution-Based Theorem Proving
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/339
We present a framework for the integration of the Knuth-Bendix completion algorithm with narrowing methods, compiled rewrite rules, and a heuristic difference reduction mechanism for paramodulation. The possibility of embedding theory unification algorithms into this framework is outlined. Results are presented and discussed for several examples of equality reasoning problems in the context of an actual implementation of an automated theorem proving system (the Mkrp-system) and a fast C implementation of the completion procedure. The Mkrp-system is based on the clause graph resolution procedure. The thesis shows the indispensibility of the constraining effects of completion and rewriting for equality reasoning in general and quantifies the amount of speed-up caused by various enhancements of the basic method. The simplicity of the superposition inference rule allows to construct an abstract machine for completion, which is presented together with computation times for a concrete implementation.Axel Präckleinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/339Mon, 03 Apr 2000 00:00:00 +0200OMEGA MKRP - A Proof Development Environment
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/340
This report presents the main ideas underlyingtheOmegaGamma mkrp-system, an environmentfor the development of mathematical proofs. The motivation for the development ofthis system comes from our extensive experience with traditional first-order theoremprovers and aims to overcome some of their shortcomings. After comparing the benefitsand drawbacks of existing systems, we propose a system architecture that combinesthe positive features of different types of theorem-proving systems, most notably theadvantages of human-oriented systems based on methods (our version of tactics) andthe deductive strength of traditional automated theorem provers.In OmegaGamma mkrp a user first states a problem to be solved in a typed and sorted higher-order language (called POST ) and then applies natural deduction inference rules inorder to prove it. He can also insert a mathematical fact from an integrated data-base into the current partial proof, he can apply a domain-specific problem-solvingmethod, or he can call an integrated automated theorem prover to solve a subprob-lem. The user can also pass the control to a planning component that supports andpartially automates his long-range planning of a proof. Toward the important goal ofuser-friendliness, machine-generated proofs are transformed in several steps into muchshorter, better-structured proofs that are finally translated into natural language.This work was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D2, D3)Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/340Mon, 03 Apr 2000 00:00:00 +0200Notes on Transformation Orderings
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/341
An important property and also a crucial point ofa term rewriting system is its termination. Transformation or-derings, developed by Bellegarde & Lescanne strongly based on awork of Bachmair & Dershowitz, represent a general technique forextending orderings. The main characteristics of this method aretwo rewriting relations, one for transforming terms and the otherfor ensuring the well-foundedness of the ordering. The centralproblem of this approach concerns the choice of the two relationssuch that the termination of a given term rewriting system can beproved. In this communication, we present a heuristic-based al-gorithm that partially solves this problem. Furthermore, we showhow to simulate well-known orderings on strings by transformationorderings.Joachim Steinbachpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/341Mon, 03 Apr 2000 00:00:00 +0200Knowledge acquisition in the domain of CNC machining centers: the Moltke approach
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/342
MOLTKE is a research project dealing with a complex technical application. After describing the domain of CNCmachining centers and the applied KA methods, we summarize the concrete KA problems which we have to handle. Then we describe a KA mechanism which supports an engineer in developing a diagnosis system. In chapter 6 weintroduce learning techniques operating on diagnostic cases and domain knowledge for improving the diagnostic procedure of MOLTKE. In the last section of this chapter we outline some essential aspects of organizationalknowledge which is heavily applied by engineers for analysing such technical systems (Qualitative Engineering). Finally we give a short overview of the actual state of realization and our future plans.Klaus-Dieter Althoff; S. Kockskämper; R. Traphöner; W. Wernickepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/342Mon, 03 Apr 2000 00:00:00 +0200Canonical Conditional Rewrite Systems Containing Extra Variables
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/344
We study deterministic conditional rewrite systems, i.e. conditional rewrite systemswhere the extra variables are not totally free but 'input bounded'. If such a systemR is quasi-reductive then !R is decidable and terminating. We develop a critical paircriterion to prove confluence if R is quasi-reductive and strongly deterministic. In thiscase we prove that R is logical, i.e./!R==R holds. We apply our results to proveHorn clause programs to be uniquely terminating.This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314, Project D4Jürgen Avenhaus; Carlos Loría-Sáenzpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/344Mon, 03 Apr 2000 00:00:00 +0200The Presentation of Proofs at the Assertion Level
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/345
Most automated theorem provers suffer from the problem that theycan produce proofs only in formalisms difficult to understand even forexperienced mathematicians. Efforts have been made to transformsuch machine generated proofs into natural deduction (ND) proofs.Although the single steps are now easy to understand, the entire proofis usually at a low level of abstraction, containing too many tedioussteps. Therefore, it is not adequate as input to natural language gen-eration systems.To overcome these problems, we propose a new intermediate rep-resentation, called ND style proofs at the assertion level . After illus-trating the notion intuitively, we show that the assertion level stepscan be justified by domain-specific inference rules, and that these rulescan be represented compactly in a tree structure. Finally, we describea procedure which substantially shortens ND proofs by abstractingthem to the assertion level, and report our experience with furthertransformation into natural language.Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/345Mon, 03 Apr 2000 00:00:00 +0200Distributing equational theorem proving
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/346
In this paper we show that distributing the theorem proving task to several experts is a promising idea. We describe the team work method which allows the experts to compete for a while and then to cooperate. In the cooperation phase the best results derived in the competition phase are collected and the less important results are forgotten. We describe some useful experts and explain in detail how they work together. We establish fairness criteria and so prove the distributed system to be both, complete and correct. We have implementedour system and show by non-trivial examples that drastical time speed-ups are possible for a cooperating team of experts compared to the time needed by the best expert in the team.Jürgen Avenhaus; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/346Mon, 03 Apr 2000 00:00:00 +0200Change of Representation in Theorem Proving by Analogy
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/347
Constructing an analogy between a known and already proven theorem(the base case) and another yet to be proven theorem (the target case) oftenamounts to finding the appropriate representation at which the base and thetarget are similar. This is a well-known fact in mathematics, and it was cor-roborated by our empirical study of a mathematical textbook, which showedthat a reformulation of the representation of a theorem and its proof is in-deed more often than not a necessary prerequisite for an analogical inference.Thus machine supported reformulation becomes an important component ofautomated analogy-driven theorem proving too.The reformulation component proposed in this paper is embedded into aproof plan methodology based on methods and meta-methods, where the latterare used to change and appropriately adapt the methods. A theorem and itsproof are both represented as a method and then reformulated by the set ofmetamethods presented in this paper.Our approach supports analogy-driven theorem proving at various levels ofabstraction and in principle makes it independent of the given and often acci-dental representation of the given theorems. Different methods can representfully instantiated proofs, subproofs, or general proof methods, and hence ourapproach also supports these three kinds of analogy respectively. By attachingappropriate justifications to meta-methods the analogical inference can oftenbe justified in the sense of Russell.This paper presents a model of analogy-driven proof plan construction andfocuses on empirically extracted meta-methods. It classifies and formally de-scribes these meta-methods and shows how to use them for an appropriatereformulation in automated analogy-driven theorem proving.Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/347Mon, 03 Apr 2000 00:00:00 +0200On Gröbner Bases in Monoid and Group Rings
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/348
Following Buchberger's approach to computing a Gröbner basis of a poly-nomial ideal in polynomial rings, a completion procedure for finitely generatedright ideals in Z[H] is given, where H is an ordered monoid presented by a finite,convergent semi - Thue system (Sigma; T ). Taking a finite set F ' Z[H] we get a(possibly infinite) basis of the right ideal generated by F , such that using thisbasis we have unique normal forms for all p 2 Z[H] (especially the normal formis 0 in case p is an element of the right ideal generated by F ). As the orderingand multiplication on H need not be compatible, reduction has to be definedcarefully in order to make it Noetherian. Further we no longer have p Delta x ! p 0for p 2 Z[H]; x 2 H. Similar to Buchberger's s - polynomials, confluence criteriaare developed and a completion procedure is given. In case T = ; or (Sigma; T ) is aconvergent, 2 - monadic presentation of a group providing inverses of length 1 forthe generators or (Sigma; T ) is a convergent presentation of a commutative monoid ,termination can be shown. So in this cases finitely generated right ideals admitfinite Gröbner bases. The connection to the subgroup problem is discussed.Klaus Madlener; Birgit Reinertpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/348Mon, 03 Apr 2000 00:00:00 +0200Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/349
We investigate restricted termination and confluence properties of term rewritADing systems, in particular weak termination and innermost termination, and theirinterrelation. New criteria are provided which are sufficient for the equivalenceof innermost / weak termination and uniform termination of term rewriting sysADtems. These criteria provide interesting possibilities to infer completeness, i.e.termination plus confluence, from restricted termination and confluence properADties.Using these basic results we are also able to prove some new results aboutmodular termination of rewriting. In particular, we show that termination ismodular for some classes of innermost terminating and locally confluent termrewriting systems, namely for nonADoverlapping and even for overlay systems. Asan easy consequence this latter result also entails a simplified proof of the factthat completeness is a decomposable property of soADcalled constructor systems.Furthermore we show how to obtain similar results for even more general cases of(nonADdisjoint) combined systems with shared constructors and of certain hierarADchical combinations of systems with constructors. Interestingly, these modularityresults are obtained by means of a proof technique which itself constitutes a modADular approach.Bernhard Gramlichpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/349Mon, 03 Apr 2000 00:00:00 +0200Analogies between Proofs - A Case Study
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/351
This case study examines in detail the theorems and proofs that are shownby analogy in a mathematical textbook on semigroups and automata, thatis widely used as an undergraduate textbook in theoretical computer scienceat German universities (P. Deussen, Halbgruppen und Automaten, Springer1971). The study shows the important role of restructuring a proof for findinganalogous subproofs, and of reformulating a proof for the analogical trans-formation. It also emphasizes the importance of the relevant assumptions ofa known proof, i.e., of those assumptions actually used in the proof. In thisdocument we show the theorems, the proof structure, the subproblems andthe proofs of subproblems and their analogues with the purpose to providean empirical test set of cases for automated analogy-driven theorem proving.Theorems and their proofs are given in natural language augmented by theusual set of mathematical symbols in the studied textbook. As a first step weencode the theorems in logic and show the actual restructuring. Secondly, wecode the proofs in a Natural Deduction calculus such that a formal analysisbecomes possible and mention reformulations that are necessary in order toreveal the analogy.Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/351Mon, 03 Apr 2000 00:00:00 +0200Guiding equational proofs by attribute functions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/354
This report presents a methodology to guide equational reasoningin a goal directed way. Suggested by rippling methods developed inthe field of inductive theorem proving we use attributes of terms andheuristics to determine bridge lemmas, i.e. lemmas which have tobe used during the proof of the theorem. Once we have found sucha bridge lemma we use the techniques of difference unification andrippling to enable its use.Jürgen Cleve; Dieter Hutterpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/354Mon, 03 Apr 2000 00:00:00 +0200A Combinator-based order-sorted higher-order unification algorithm
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/355
This paper develops a sound and complete transformation-based algorithm forunification in an extensional order-sorted combinatory logic supporting constantoverloading and a higher-order sort concept. Appropriate notions of order-sortedweak equality and extensionality - reflecting order-sorted fij-equality in thecorresponding lambda calculus given by Johann and Kohlhase - are defined, andthe typed combinator-based higher-order unification techniques of Dougherty aremodified to accommodate unification with respect to the theory they generate. Thealgorithm presented here can thus be viewed as a combinatory logic counterpartto that of Johann and Kohlhase, as well as a refinement of that of Dougherty, andprovides evidence that combinatory logic is well-suited to serve as a framework forincorporating order-sorted higher-order reasoning into deduction systems aimingto capitalize on both the expressiveness of extensional higher-order logic and theefficiency of order-sorted calculi.Patricia Johannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/355Mon, 03 Apr 2000 00:00:00 +0200New Abstract Criteria for Termination and Confluence of Conditional Rewrite Systems
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/356
We consider the problem of verifying confluence and termination of conditionalterm rewriting systems (TRSs). For unconditional TRSs the critical pair lemmaholds which enables a finite test for confluence of (finite) terminating systems.And for ensuring termination of unconditional TRSs a couple of methods forconstructing appropiate well-founded term orderings are known. If however ter-mination is not guaranteed then proving confluence is much more difficult. Re-cently we have obtained some interesting results for unconditional TRSs whichprovide sufficient criteria for termination plus confluence in terms of restrictedtermination and confluence properties. In particular, we have shown that anyinnermost terminating and locally confluent overlay system is complete, i.e. ter-minating and confluent. Here we generalize our approach to the conditional caseand show how to solve the additional complications due to the presence of con-ditions in the rules. Our main result can be stated as follows: Any conditionalTRS which is an innermost terminating semantical overlay system such that all(conditional) critical pairs are joinable is complete.Bernhard Gramlichpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/356Mon, 03 Apr 2000 00:00:00 +0200On the Complexity of Simplification Orderings
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/357
Various methods for proving the termination of term rewriting systems havebeen suggested. Most of them are based on the notion of simplification ordering.In this paper, the theoretical time complexities (of the worst cases) of a collectionof well-known simplification orderings will be presented.Joachim Steinbachpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/357Mon, 03 Apr 2000 00:00:00 +0200About changing the ordering during Knuth-Bendix completion
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/358
We will answer a question posed in [DJK91], and will show that Huet's completion algorithm [Hu81] becomes incomplete, i.e. it may generate a term rewriting system that is not confluent, if it is modified in a way that the reduction ordering used for completion can be changed during completion provided that the new ordering is compatible with the actual rules. In particular, we will show that this problem may not only arise if the modified completion algorithm does not terminate: Even if the algorithm terminates without failure, the generated finite noetherian term rewriting system may be non-confluent. Most existing implementations of the Knuth-Bendix algorithm provide the user with help in choosing a reduction ordering: If an unorientable equation is encountered, then the user has many options, especially, the one to orient the equation manually. The integration of this feature is based on the widespread assumption that, if equations are oriented by hand during completion and the completion process terminates with success, then the generated finite system is a maybe non terminating but locally confluent system (see e.g. [KZ89]). Our examples will show that this assumption is not true.Andrea Sattler-Kleinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/358Mon, 03 Apr 2000 00:00:00 +0200Mechanization of Strong Kleene Logic for Partial Functions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/359
Even though it is not very often admitted, partial functions do play asignificant role in many practical applications of deduction systems. Kleenehas already given a semantic account of partial functions using three-valuedlogic decades ago, but there has not been a satisfactory mechanization. Recentyears have seen a thorough investigation of the framework of many-valuedtruth-functional logics. However, strong Kleene logic, where quantificationis restricted and therefore not truth-functional, does not fit the frameworkdirectly. We solve this problem by applying recent methods from sorted logics.This paper presents a resolution calculus that combines the proper treatmentof partial functions with the efficiency of sorted calculi.Manfred Kerber; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/359Mon, 03 Apr 2000 00:00:00 +0200