Computer supported mathematics with Ωmega

Classical automated theorem proving of today is based on ingenious search techniques to find a proof for a given theorem in very large search spaces—often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited.The shift from search based methods to more abstract planning techniques however opened up a paradigm for mathematical reasoning on a computer and several systems of that kind now employ a mix of interactive, search based as well as proof planning techniques.The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for a working mathematician as well as a software engineer when employing formal methods for quality assurance. In particular, Ωmega supports proof development at a human-oriented abstract level of proof granularity. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL, CoQ, Hol, Pvs, and Isabelle. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh.     

An example of formalizing recent mathematical results in Mizar

This paper describes an example of the successful formalization of quite advanced and new mathematics using the Mizar system. It shows that although much effort is required to formalize nontrivial facts in a formal computer deduction system, still it is possible to obtain the level of full logical correctness of all inference steps. We also discuss some problems encountered during the formalization, and try to point out some of the features of the Mizar system responsible for that. The formalization described in this paper allows also for contrasting the linguistic capability of the Mizar language and some of the phrases commonly used in “informal” mathematical papers that the Mizar system lacks, and consequently presents the methods of how to cope with it during the formalization. Yet, apart from the problems, this paper shows some definite benefits from using a formal computer system in the work of a mathematician.     

Cogex: A semantically and contextually enriched logic prover for question answering

This paper presents the architecture and functionality of a logic prover designed for question answering. The approach transforms questions and answer passages into logic representations based on syntactic, semantic and contextual information. World knowledge supplements the linguistic, ontological, and temporal axioms supplied to the prover which renders a deep understanding of the relationship between the question and answer text. The trace of the proofs provides a basis for generating human comprehensible answer justifications. The results show that the prover boosts the performance of the Question Answering system on TREC 2004 questions by 12%.     

Publisher's notice 1993 Publication programme

Publisher's notice1993 Publication programme