Filtern
Dokumenttyp
- Preprint (21) (entfernen)
Schlagworte
- resolution (2)
- Declarative and Procedural Knowledge (1)
- Deduction (1)
- Methods (1)
- Partial functions (1)
- Planning and Verification (1)
- Tactics (1)
- analogy (1)
- case-based reasoning (1)
- concept representation (1)
-
Analogical Reasoning with Typical Examples
(1999)
- 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.
-
Reuse of Proofs by Meta-Methods
(1999)
- 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.
-
Die Beweisentwicklungsumgebung Omega-MKRK
(1999)
- 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.
-
Mechanising Partiality without Re-Implementation
(1999)
- 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.
-
Two Kinds of Non-Monotonic Analogical Inference ?
(1999)
- 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.
- Planverfahren (1999)
