We present a mathematical knowledge base containing the factual know-ledge of the first of three parts of a textbook on semi-groups and automata,namely "P. Deussen: Halbgruppen und Automaten". Like almost all math-ematical textbooks this textbook is not self-contained, but there are somealgebraic and set-theoretical concepts not being explained. These concepts areadded to the knowledge base. Furthermore there is knowledge about the nat-ural numbers, which is formalized following the first paragraph of "E. Landau:Grundlagen der Analysis".The data base is written in a sorted higher-order logic, a variant of POST ,the working language of the proof development environment OmegaGamma mkrp. We dis-tinguish three different types of knowledge: axioms, definitions, and theorems.Up to now, there are only 2 axioms (natural numbers and cardinality), 149definitions (like that for a semi-group), and 165 theorems. The consistency ofsuch knowledge bases cannot be proved in general, but inconsistencies may beimported only by the axioms. Definitions and theorems should not lead to anyinconsistency since definitions form conservative extensions and theorems areproved to be consequences.
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.
A lot of the human ability to prove hard mathematical theorems can be ascribedto a problem-specific problem solving know-how. Such knowledge is intrinsicallyincomplete. In order to prove related problems human mathematicians, however,can go beyond the acquired knowledge by adapting their know-how to new relatedproblems. These two aspects, having rich experience and extending it by need, can besimulated in a proof planning framework: the problem-specific reasoning knowledge isrepresented in form of declarative planning operators, called methods; since these aredeclarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs intheorem proving, first, we present methods for proving the ground completeness ofbinary resolution, which essentially correspond to key lemmata, and then, we showhow these methods can be reused for the proof of the ground completeness of lockresolution.
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.
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.
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.
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.