Publication Date

2014-04-23

Availability

Open access

Embargo Period

2014-04-23

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

Burton Rosenberg

Third Committee Member

Victor J. Milenkovic

Abstract

The TPTP (Thousands of Problems forTheorem Provers) World is a well established infrastructure for Automated Theorem Proving (ATP). In the context of the TPTP World, a command language was needed to make possible the easy manipulation of logical formulae and provide better control over the use of ATP systems. The TPTP Process Instruction (TPI) language provides such capabilities. It is used to input, output and organize logical formulae, and control the execution of ATP systems. This thesis presents the work done for building and testing a shell interpreter for the TPI language. The thesis is divided into five parts. The first part provides a review of ATP, ATP systems, and the TPTP World. The second part provides an overview of the related work and presents the TPI language. The third part introduces the ATP process and discusses its benefits. The fourth part presents the shell interpreter that has been developed for the TPI language, describes its implementation and provides examples of how it can be used in theorem proving. The last part discusses generic control of ATP systems and demonstrates how such control is achieved through an extension to the TPI language.

Keywords

Automated Theorem Proving; The TPTP World; Logic; TPTP Process Instruction Language, ATP Process

Download

Share

COinS