search

salmans / Razor

5 stars 0 forks source link

Support for TPTP inputs #66

Closed salmans closed 9 years ago

salmans commented 9 years ago

I propose the following steps or implementing this feature:

  1. Implemeting a TPTP parser and functions for converting TPTP inputs to Razor's input language, for inputs that are in the geometric form.
  2. Implementing an interface for supporting TPTP inputs in the high-level APIs and the REPL.
  3. Adding support for TPTP formulas that are not in the geometric form. For this, we need to develop an algorithm for identifying existential quantifiers that must be Skolemized.
salmans commented 9 years ago

I just added new files to Syntax that provide parsing for TPTP and a best-effort algorithm for converting the resulting FOL formulas to a geometric theory. The conversion algorithm is sound but it is not efficient. At the moment, the conversion algorithm fails if the input is not equivalent to a geometric theory. Eventually, we will force the conversion by Skolemizing the input. @ryandanas I think the next step is to add support for TPTP in the high-level API layer and the REPL. I have some legacy code to show how the conversion should be done.

dandougherty commented 9 years ago

Good job.

Dan (taking a micro-break to read email)

On Sat, Jan 17, 2015 at 7:19 PM, Salman Saghafi notifications@github.com wrote:

I just added new files to Syntax that provide parsing for TPTP and a best-effort algorithm for converting the resulting FOL formulas to a geometric theory. The conversion algorithm is sound but it is not efficient. At the moment, the conversion algorithm fails if the input is not equivalent to a geometric theory. Eventually, we will force the conversion by Skolemizing the input. @ryandanas https://github.com/ryandanas I think the next step is to add support for TPTP in the high-level API layer and the REPL. I have some legacy code to show how the conversion should be done.

Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/66#issuecomment-70390799.

thedotmatrix commented 9 years ago

Closing for now. I think to extend the support of any language, including TPTP, is best kept to issue #57 .