KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Mon, 03 Apr 2000 00:00:00 +0200Mon, 03 Apr 2000 00:00:00 +0200The Adaption of Proof Methods by Reformulation
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/63
Manfred Kerber; Xiaorong Huang; Lassaad Cheikhrouhouarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/63Mon, 03 Apr 2000 00:00:00 +0200Reuse of Proofs by Meta-Methods
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/250
This paper describes a declarative approach forencoding the plan operators in proof planning,the so-called methods. The notion of methodevolves from the much studied concept of a tac-tic and was first used by A. Bundy. Signific-ant deductive power has been achieved withthe planning approach towards automated de-duction; however, the procedural character ofthe tactic part of methods hinders mechanicalmodification. Although the strength of a proofplanning system largely depends on powerfulgeneral procedures which solve a large class ofproblems, mechanical or even automated modi-fication of methods is necessary, since methodsdesigned for a specific type of problems willnever be general enough. After introducing thegeneral framework, we exemplify the mechan-ical modification of methods via a particularmeta-method which modifies methods by trans-forming connectives to quantifiers.Manfred Kerber; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/250Mon, 03 Apr 2000 00:00:00 +0200Die Beweisentwicklungsumgebung Omega-MKRK
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/251
Die Beweisentwicklungsumgebung Omega-Mkrp soll Mathematiker bei einer ihrer Haupttätigkeiten, nämlich dem Beweisen mathematischer Theoreme unterstützen. Diese Unterstützung muß so komfortabel sein, daß die Beweise mit vertretbarem Aufwand formal durchgeführt werden können und daß die Korrektheit der so erzeugten Beweise durch das System sichergestellt wird. Ein solches System wird sich nur dann wirklich durchsetzen, wenn die rechnergestützte Suche nach formalen Beweisen weniger aufwendig und leichter ist, als ohne das System. Um dies zu erreichen, ergeben sich verschiedene Anforderungen an eine solche Entwicklungsumgebung, die wir im einzelnen beschreiben. Diese betreffen insbesondere die Ausdruckskraft der verwendeten Objektsprache, die Möglichkeit, abstrakt über Beweispläne zu reden, die am Menschen orientierte Präsentation der gefundenen Beweise, aber auch die effiziente Unterstützung beim Füllen von Beweislücken. Das im folgenden vorgestellte Omega-Mkrp-System ist eine Synthese der Ansätze des vollautomatischen, des interaktiven und des planbasierten Beweisens und versucht erstmalig die Ergebnisse dieser drei Forschungsrichtungen in einem System zu vereinigen. Dieser Artikel soll eine Übersicht über unsere Arbeit an diesem System geben.Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/251Mon, 03 Apr 2000 00:00:00 +0200A Test for Evaluating the Practical Usefulness of Deduction Systems
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/252
Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Dan Nesmith; Jörn Richtspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/252Mon, 03 Apr 2000 00:00:00 +0200Guaranteeing Correctness through the Communication of Checkable Proofs(or: Would You Really Trust an Automated Reasoning System?)
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/254
Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Dan Nesmith; Jörn Richtspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/254Mon, 03 Apr 2000 00:00:00 +0200Adapting Methods to Novel Tasks in Proof Planning ?
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/255
In this paper we generalize the notion of method for proofplanning. While we adopt the general structure of methods introducedby Alan Bundy, we make an essential advancement in that we strictlyseparate the declarative knowledge from the procedural knowledge. Thischange of paradigm not only leads to representations easier to under-stand, it also enables modeling the important activity of formulatingmeta-methods, that is, operators that adapt the declarative part of exist-ing methods to suit novel situations. Thus this change of representationleads to a considerably strengthened planning mechanism.After presenting our declarative approach towards methods we describethe basic proof planning process with these. Then we define the notion ofmeta-method, provide an overview of practical examples and illustratehow meta-methods can be integrated into the planning process.Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Jörn Richtsarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/255Mon, 03 Apr 2000 00:00:00 +0200Adapting the Diagonalization Method by Reformulations
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/257
Extending the planADbased paradigm for auto-mated theorem proving, we developed in previ-ous work a declarative approach towards rep-resenting methods in a proof planning frame-work to support their mechanical modification.This paper presents a detailed study of a classof particular methods, embodying variations ofa mathematical technique called diagonaliza-tion. The purpose of this paper is mainly two-fold. First we demonstrate that typical math-ematical methods can be represented in ourframework in a natural way. Second we illus-trate our philosophy of proof planning: besidesplanning with a fixed repertoire of methods,metaADmethods create new methods by modify-ing existing ones. With the help of three differ-ent diagonalization problems we present an ex-ample trace protocol of the evolution of meth-ods: an initial method is extracted from a par-ticular successful proof. This initial method isthen reformulated for the subsequent problems,and more general methods can be obtained byabstracting existing methods. Finally we comeup with a fairly abstract method capable ofdealing with all the three problems, since it cap-tures the very key idea of diagonalization.Manfred Kerber; Xiaorong Huang; Lassaad Cheikhrouhouarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/257Mon, 03 Apr 2000 00:00:00 +0200A Tableau Calculus for Partial Functions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/265
Even though it is not very often admitted, partial functionsdo play a significant role in many practical applications of deduction sys-tems. Kleene has already given a semantic account of partial functionsusing a three-valued logic decades ago, but there has not been a satisfact-ory mechanization. Recent years have seen a thorough investigation ofthe framework of many-valued truth-functional logics. However, strongKleene logic, where quantification is restricted and therefore not truth-functional, does not fit the framework directly. We solve this problemby applying recent methods from sorted logics. This paper presents atableau calculus that combines the proper treatment of partial functionswith the efficiency of sorted calculi.Michael Kohlhase; Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/265Mon, 03 Apr 2000 00:00:00 +0200A Resolution Calculus for Presuppositions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/266
The semantics of everyday language and the semanticsof its naive translation into classical first-order language consider-ably differ. An important discrepancy that is addressed in this paperis about the implicit assumption what exists. For instance, in thecase of universal quantification natural language uses restrictions andpresupposes that these restrictions are non-empty, while in classi-cal logic it is only assumed that the whole universe is non-empty.On the other hand, all constants mentioned in classical logic arepresupposed to exist, while it makes no problems to speak about hy-pothetical objects in everyday language. These problems have beendiscussed in philosophical logic and some adequate many-valuedlogics were developed to model these phenomena much better thanclassical first-order logic can do. An adequate calculus, however, hasnot yet been given. Recent years have seen a thorough investigationof the framework of many-valued truth-functional logics. UnfortuADnately, restricted quantifications are not truth-functional, hence theydo not fit the framework directly. We solve this problem by applyingrecent methods from sorted logics.Manfred Kerber; Michael Kohlhasearticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/266Mon, 03 Apr 2000 00:00:00 +0200Mechanising Partiality without Re-Implementation
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/267
Even though it is not very often admitted, partial functionsdo play a significant role in many practical applications of deduction sys-tems. Kleene has already given a semantic account of partial functionsusing a three-valued logic decades ago. This approach allows rejectingcertain unwanted formulae as faulty, which the simpler two-valued onesaccept. We have developed resolution and tableau calculi for automatedtheorem proving that take the restrictions of the three-valued logic intoaccount, which however have the severe drawback that existing theo-rem provers cannot directly be adapted to the technique. Even recentlyimplemented calculi for many-valued logics are not well-suited, since inthose the quantification does not exclude the undefined element. In thiswork we show, that it is possible to enhance a two-valued theorem proverby a simple strategy so that it can be used to generate proofs for the the-orems of the three-valued setting. By this we are able to use an existingtheorem prover for a large fragment of the language.Manfred Kerber; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/267Mon, 03 Apr 2000 00:00:00 +0200Using Exemplary Knowledge for Justified Analogical Reasoning
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/269
Typical instances, that is, instances that are representative for a particular situ-ation or concept, play an important role in human knowledge representationand reasoning, in particular in analogical reasoning. This wellADknown obser-vation has been a motivation for investigations in cognitive psychology whichprovide a basis for our characterization of typical instances within conceptstructures and for a new inference rule for justified analogical reasoning withtypical instances. In a nutshell this paper suggests to augment the proposi-tional knowledge representation system by a non-propositional part consistingof concept structures which may have directly represented instances as ele-ments. The traditional reasoning system is extended by a rule for justifiedanalogical inference with typical instances using information extracted fromboth knowledge representation subsystems.Manfred Kerber; Erica Melisarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/269Mon, 03 Apr 2000 00:00:00 +0200Two Kinds of Non-Monotonic Analogical Inference ?
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/270
This paper addresses two modi of analogical reasoning. Thefirst modus is based on the explicit representation of the justificationfor the analogical inference. The second modus is based on the repre-sentation of typical instances by concept structures. The two kinds ofanalogical inferences rely on different forms of relevance knowledge thatcause non-monotonicity. While the uncertainty and non-monotonicity ofanalogical inferences is not questioned, a semantic characterization ofanalogical reasoning has not been given yet. We introduce a minimalmodel semantics for analogical inference with typical instances.Manfred Kerber; Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/270Mon, 03 Apr 2000 00:00:00 +0200Analogical Reasoning with a Hybrid Knowledge Base
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/271
Manfred Kerber; Erica Melis; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/271Mon, 03 Apr 2000 00:00:00 +0200Reformulating Resolution Problems by Tactics
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/272
A straightforward formulation of a mathematical problem is mostly not ad-equate for resolution theorem proving. We present a method to optimize suchformulations by exploiting the variability of first-order logic. The optimizingtransformation is described as logic morphisms, whose operationalizations aretactics. The different behaviour of a resolution theorem prover for the sourceand target formulations is demonstrated by several examples. It is shown howtactical and resolution-style theorem proving can be combined.Manfred Kerber; Axel Präckleinarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/272Mon, 03 Apr 2000 00:00:00 +0200Beherrschbarkeit von Computersystemen
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/273
Manfred Kerber; Axel Präckleinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/273Mon, 03 Apr 2000 00:00:00 +0200Deduktionssysteme
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/274
Manfred Kerber; Christoph Weidenbacharticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/274Mon, 03 Apr 2000 00:00:00 +0200Sortenlogiken und ihre Automatisierung
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/275
Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/275Mon, 03 Apr 2000 00:00:00 +0200Mehrwertige Logiken in der KI
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/276
Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/276Mon, 03 Apr 2000 00:00:00 +0200Planverfahren
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/277
Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/277Mon, 03 Apr 2000 00:00:00 +0200On the Representation of Mathematical Knowledge in Frames and its Consistency
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/278
We show how to buildup mathematical knowledge bases usingframes. We distinguish three differenttypes of knowledge: axioms, definitions(for introducing concepts like "set" or"group") and theorems (for relating theconcepts). The consistency of such know-ledge bases cannot be proved in gen-eral, but we can restrict the possibilit-ies where inconsistencies may be impor-ted to very few cases, namely to the oc-currence of axioms. Definitions and the-orems should not lead to any inconsisten-cies because definitions form conservativeextensions and theorems are proved to beconsequences.Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/278Mon, 03 Apr 2000 00:00:00 +0200On the Translation of Higher-Order Problems into First-Order Logic
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/279
In most cases higher-order logic is based on the (gamma)-calculus in order to avoid the infinite set of so-called comprehension axioms. However, there is a price to be paid, namelyan undecidable unification algorithm. If we do not use the(gamma) - calculus, but translate higher-order expressions intofirst-order expressions by standard translation techniques, we haveto translate the infinite set of comprehension axioms, too. Ofcourse, in general this is not practicable. Therefore such anapproach requires some restrictions such as the choice of thenecessary axioms by a human user or the restriction to certainproblem classes. This paper will show how the infinite class ofcomprehension axioms can be represented by a finite subclass,so that an automatic translation of finite higher-order prob-lems into finite first-order problems is possible. This trans-lation is sound and complete with respect to a Henkin-stylegeneral model semantics.Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/279Mon, 03 Apr 2000 00:00:00 +0200sound and complete translations from sorted higher-order logic into sorted first-order logic
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/280
Extending existing calculi by sorts is astrong means for improving the deductive power offirst-order theorem provers. Since many mathemat-ical facts can be more easily expressed in higher-orderlogic - aside the greater power of higher-order logicin principle - , it is desirable to transfer the advant-ages of sorts in the first-order case to the higher-ordercase. One possible method for automating higher-order logic is the translation of problem formulationsinto first-order logic and the usage of first-order the-orem provers. For a certain class of problems thismethod can compete with proving theorems directlyin higher-order logic as for instance with the TPStheorem prover of Peter Andrews or with the Nuprlproof development environment of Robert Constable.There are translations from unsorted higher-order lo-gic based on Church's simple theory of types intomany-sorted first-order logic, which are sound andcomplete with respect to a Henkin-style general mod-els semantics. In this paper we extend correspond-ing translations to translations of order-sorted higher-order logic into order-sorted first-order logic, thus weare able to utilize corresponding first-order theoremprover for proving higher-order theorems. We do notuse any (lambda)-expressions, therefore we have to add so-called comprehension axioms, which a priori makethe procedure well-suited only for essentially first-order theorems. However, in practical applicationsof mathematics many theorems are essentially first-order and as it seems to be the case, the comprehen-sion axioms can be mastered too.Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/280Mon, 03 Apr 2000 00:00:00 +0200An Approach of Formalizing Mathematics by Reformulations - A Proposal for QED -
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/281
Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/281Mon, 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 +0200