The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
Master of Science (MS)
Computer Science (Arts and Sciences)
Date of Defense
First Committee Member
Second Committee Member
Third Committee Member
Many Automated Theorem Prover (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 forms. On the other hand, the ATP systems for less expressive forms have been tested for many years, and are more powerful and reliable. There is a trade-off between expressivity of a logical form, and power and reliability of the available ATP systems. Different ATP systems and translators can be combined to solve a problem expressed in a logic. In this research, an experiment has been designed and carried out to compare all different possible ways of trying to solve a problem. The possibilities are either to use an ATP system for the original form, or translate the problem to a less expressive form. If the problem is translated to a less expressive form, then again the same two possibilities are available, until no further translation is possible. No translator was available to translate from Conjunctive Normal Form to Description Logic, which sits between Effectively Propositional Logic and Propositional Logic in terms of expressivity. A translation procedure for translating Conjunctive Normal Form to Description Logic, and its implementation as Saffron are presented. Additionally, this research includes a survey of different logical forms. Propositional Logic, Description Logic, First Order Form, Conjunctive Normal Form, Effectively Propositional, Typed First order Form - monomorphic, Typed First order Form - polymorphic, Typed Higher order Form - monomorphic. The properties, syntax, and semantics of each logical form are briefly described. For each form, the most popular ATP systems and translators for translating to a less expressive forms are introduced.
Automated Theorem Proving; Description Logic; Logic Translation; Conjunctive Normal Form (CNF); Logical Form; Automated Reasoning; Saffron DL Translator
Arhami, Negin, "The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics" (2014). Open Access Theses. 519.