Automated theorem proving by translation to description logic.

摘要

Many Automated Theorem Proving (ATP) systems for different logical forms, and translators for translating different logical forms from one to another, have been developed and are now available. Some logical forms are more expressive than others, and it is easier to express problems in those logical forms. On the other hand, the ATP systems for less expressive forms have benefited from more years of development and testing. There is a trade-off between the expressivity of a logical form, and the capabilities of the available ATP systems. Different ATP systems and translators can be combined to solve a problem expressed in a given logical form. In this research, an experiment has been designed and carried out to compare all different possible ways of trying to solve a problem, using the following logical forms in increasing order of expressivity: Propositional Logic, Description Logic, Effectively Propositional form, Conjunctive Normal Form, First Order Form, Typed First order form-monomorphic, Typed First order form-polymorphic, Typed Higher order form-monomorphic. In this dissertation, the properties, syntax, and semantics of each target logical form are briefly described. For each form, the most popular ATP systems and translators for translating to less expressive forms are introduced.;Problems in logics more expressive than Conjunctive Normal Form can be translated directly to Conjunctive Normal Form, or indirectly by translation via intermediate logics. No translator was available to translate from Conjunctive Normal Form to Description Logic, which sits between Effectively Propositional form and Propositional Logic in terms of expressivity. Saffron a Conjunctive Normal Form to Description Logic translator, has been developed, which fills the gap between Conjunctive Normal Form and Description Logic. Moreover, Description Logic Form (DLF), a new syntax for Description Logic, has been designed. Automated theorem proving by translation to Description Logic is now an alternative way of solving problems expressed in logics more expressive than Description Logic, by combining necessary translators from those logics to Conjunctive Normal Form, Saffron, and a Description Logic ATP system.