Title

The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics

Publication Date

2014-10-09

Availability

Open access

Embargo Period

2014-10-09

Degree Name

Master of Science (MS)

Department

Computer Science (Arts and Sciences)

Date of Defense

2014-04-16

First Committee Member

Geoff Sutcliffe

Second Committee Member

Ubbo Visser

Third Committee Member

Peter Lewis

Abstract

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.

Keywords

Automated Theorem Proving; Description Logic; Logic Translation; Conjunctive Normal Form (CNF); Logical Form; Automated Reasoning; Saffron DL Translator

This document is currently not available here.

Share

COinS