TPTP

This package provides a client for the TPTP that facilitates access to the TPTP's comprehensive collection of ATP problems and ATP systems.

Note: If you want to run the tests included in this package (using npm test) be aware that environment variable HTTP_PROXY must be set to define a proxy if and only if a proxy is required. The proxy defined this way may include the port (separated from the host by a colon). If no port is given it defaults to 8080.

Quick Run

tptpClient.js can be used to explore the basics of the TPTP client. Run

$ node tptpClient

for usage information.

Usage

const tptp = require('./'); // assuming this code is executed in the installation directory of package tptp
const tptpClient = tptp.tptpClient;
const converter = tptp.converter;

Object tptpClient

Object tptpClient represents a TPTP client and provides TPTP access through the following functions (listed in alphabetical order). Most of these functions are asynchronous. They return a Promise unless a callback function is supplied. In the latter case the callback function should accept two arguments, the first one being an error object. If no error occurred the error object is null and the second argument is the result of the asynchronous call. Let us look at a simple example that fetches all domains and prints the number of domains on the console, or an error if the call failed. First without a callback function:

tptpClient.getDomainNames().then(domains => console.log(domains.length)).catch(err => console.log(err));

and secondly with classic callback:

tptpClient.getDomainNames((err, domains) => {
  if (err)
    console.log(err);
  else
    console.log(domains.length);
});

The callback parameter (cb) will be shown in brackets wherever it occurs to indicate that it is optional, and that by omitting it a Promise will be returned.

createQuery (stringent)

Creates a query that can be used to submit a query (see submitQuery). The query created is an object that offers the following functions to set (or unset) query parameters, thereby shaping the result returned by submitQuery when given this query object. All these methods take one or no parameter (a string). If a parameter is provided its value is set as the value of the respective property unless the value is invalid, in which case the property is deleted (if stringent is anything equivalent to false) or an exception is thrown detailing the cause and remedy (if stringent is anything equivalent to true). If no parameter is given the respective property is deleted.

• setForm: valid parameter values are 'TH0', 'TF0', 'FOF', 'CNF'

• setStatus: valid parameter values are 'THM', 'CSA', 'UNK', 'UNS', 'SAT', 'OPN'

• setOrder: valid parameter values are 'PRP', 'EPR', 'FHU', 'RFO'

• setPredicates: valid parameter values are 'PC1', 'PCN'

• setEquality: valid parameter values are 'NEQ', 'SEQ', 'PEQ', 'EQU'

• setUnitEquality: valid parameter values are 'NUE', 'UEQ'

• setArithmetic: valid parameter values are 'NAR', 'ARI'

• setHorn: valid parameter values are 'HRN', 'NHN'

• setRRClauses: valid parameter values are 'RRE', 'NRR'

• setFormulae: valid parameter values are 'SML', 'MED', 'LRE', 'XLG'

• setClauses: valid parameter values are 'CSM', 'CMD', 'CLG', 'CXD'

• setDiscreteRating: valid parameter values are 'ESY', 'DIF', 'USO'

• setVersion: valid parameter values are 'STD', 'INC', 'AUG', 'ESP', 'BIA', 'UNB'

To invert or negate a property the functions setFormNeg, setStatusNeg, etc can be used. Supply a parameter representing true to activate negation, no parameter or false to deactivate negation.

The functions all return the query object itself to permit "method chaining."

On top of these functions there are two functions for white or black listing domains:

• restrictedToDomains

• excludeDomains

Both functions accept any number of domain names or an array of domain names.

Example: The following query is set up to search for non-satisfiable propositional problems given in CNF restricted to the domains 'PUZ' and 'NUM':

let query = tptpClient.createQuery()
  .setForm('CNF')
  .setOrder('PRP')
  .setStatus('SAT')
  .setStatusNeg(true)
  .restrictedToDomains('PUZ', 'NUM');

getAxiomSet (name[, cb])

Gets the axiom set file specified by its name. The result of this call is the contents of the axiom set file as a string.

getAxiomSetNames ([cb])

Gets the names of all axiom sets. The result of this call is an array of string values, each of which is the name of an axiom set.

getDomainNames ([cb])

Gets all domain names. The result of this call is an array of string values, each of which is the name of a domain.

getProblem (domain, name[, cb])

Gets the problem file specified by its domain and name. The result of this call are the contents of the specified problem file (a string).

getProblemNames (domain[, cb])

Gets the problem names for the specified domain. The result of this call is an array of string values, each of which is a problem name of the given domain.

getProblemWithAxiomSetsIncluded (domain, name[, cb])

Gets the problem file specified by its domain and name with all axiom sets included. The result of this call are the contents of the specified problem file (a string) with all occurrences of the include command for axiom sets replaced with the contents of the respective axiom set file.

See also: includeAxiomSets

getProxy ()

Gets the proxy currently used by the TPTP client to send HTTP requests. It returns null if no proxy has been set (and hence no proxy is used), or a string of the form '<hostName>:<port>'.

includeAxiomSets (problem[, cb])

Includes axiom sets for the given problem (contents of a problem file, i.e. a string). In other words all occurrences of the include command are replaced with the contents of the respective axiom set file. The result of this call are the contents of the problem file with all axiom set inclusions replaced.

See also: getProblemWithAxiomSetsIncluded

runParallel (problem, nSys, options[, cb])

Runs the systems considered most suitable for solving the given problem.

Parameter problem is a string that can be either a problem file name of the TPTP (with or without extension .p), a problem in TPTP syntax, or a local file name containing such a problem.

The number of systems to run in parallel is specified through nSys (default is 1).

The result of this call is the result of the system run. See runSystem for details on the result object. (Note that in parallel mode systemOutput is never supplied.)

Options can be provided through the properties of an object options. The following properties are recognized:

• timeout: a number specifying the timeout or time limit in seconds; the default is 300 seconds

runSuggestedSystem (problem, options[, cb])

Runs the system considered best suited for the given problem. This is a convenience method for calling

tptpClient.runParallel(problem, 1, options, cb);

runSystem (system, problem, options[, cb])

Runs the given system to solve the given problem (cp. System on TPTP).

Parameter system can be specified through an object returned by suggestSystem or suggestSystemList, or a system name understood by the TPTP (such as 'E---1.8', for instance).

Parameter problem is a string that can be either a problem file name of the TPTP (with or without extension .p), a problem in TPTP syntax, or a local file name containing such a problem.

The result of this call is the result of the system run. The result is an object that summarizes the system run through the following properties:

• problemName: the name of the problem

• systemName: the name of the system that solved (or attempted to solve) the problem

• result: the outcome of the system run (such as Satisfiable, for instance)

• cpuTime: the CPU time

• wallClockTime: the wall clock time

• systemOutput: the system-specific output (only if requested through option flag includeSystemOutput)

Note that in particular the values of properties result and of course systemOutput vary from system to system.

Options can be provided through the properties of an object options. The following properties are recognized:

• command: the command used to run the given system; the default is system-specific (see System on TPTP)

• format: the input format; the default is system-specific (typically 'tptp:raw'; see System on TPTP)

• includeSystemOutput: a flag indicating that system output should be included in the result object

• timeout: a number specifying the timeout or time limit in seconds; the default is 60 seconds

See also: runSuggestedSystem, suggestSystem, suggestSystemList

setProxy (hostName, port)

Sets the proxy to be used by the TPTP client for sending HTTP requests. If hostName is null or undefined no proxy is set or used. Otherwise the proxy is set as specified by hostName. Note that hostName may include the port (separated from the actual host name by a colon). If the second parameter port is supplied it will override any port specified through parameter hostName. If no port is specified it will default to 8080.

submitQuery (query, problemNamesOnly[, cb])

Submits the given query to search the TPTP for problems satisfying the constraints specified through the query parameters, i.e. properties of the query.

The result of this call is the result of the search. If parameter problemNamesOnly is not supplied or false the result is an array containing objects, one for each domain that contributes search results. Each such object has two properties, namely domain and problemNames, the name of the domain and an array of problem names, respectively. If parameter problemNamesOnly is true then the result is an array containing the names of all qualifying problems. Thus there is no domain information in this latter case.

The query object is best created with createQuery. It may of course also be produced in a different manner reflecting the conventions employed by tptp2T Online.

suggestSystem (problem[, cb])

Suggests a system considered best suited to solve the given problem.

Parameter problem is a string that can be either a problem file name of the TPTP (with or without extension .p), a problem in TPTP syntax, or a local file name containing such a problem.

TThe result of this call is an object representing the suggested system. If no suitable system could be found the object returned null. Otherwise the object can be used as parameter system of runSystem. Such an object offers the following methods (all returning a string):

• getName(): the name of the system (without version or an optional suffix)

• getVersion(): the version of the system

• getSuffix(): the (optional) suffix of the system (null if there is no suffix)

• getFullName(): the full name of the system including version (and suffix)

• getTptpName(): the name understood by the TPTP (see also runSystem)

• getStatus(): the status of the system (either 'recommended' or 'subsumed')

• getSpc(): the SPC (a number, albeit a string, ranging from '0.00' to '1.00')

See also: suggestSystemList, runSystem

suggestSystemList (problem[, cb])

Suggests a list of systems considered suitable to solve the given problem, in descending order of suitability. (In other words, the best suited system is the first in the list.)

Parameter problem is a string that can be either a problem file name of the TPTP (with or without extension .p), a problem in TPTP syntax, or a local file name containing such a problem.

The result of this call is an array of objects, each representing a suitable system. If no suitable system could be found then the array is empty. Each of the objects in the array returned can be used as parameter system of runSystem. (Consult the documentation of suggestSystem for more details on such an object.) The array itself has a method toString() that produces a formatted list of the systems in the array.

See also: suggestSystem, runSystem

Object converter

Object converter offers conversion facilities for converting between TPTP syntax and other well established formats. For instance, the data read by tptpClient could be piped into a converter as shown in the following example:

tptpClient.getProblemWithAxiomSetsIncluded('GRA','GRA001-1.p')
  .then(data => console.log(converter.tptpToDimacs(data)))
  .catch(err => console.log(err));

or with the classic callback function:

tptpClient.getProblemWithAxiomSetsIncluded(
  'GRA',
  'GRA001-1.p',
  function (err,data)
  {
    if (err)
      console.log(err);
    else
      console.log(converter.tptpToDimacs(data));
  }
);

The above piece of code will convert TPTP problem GRA001-1.p into DIMACS format and write the result to the console. For conversion into JSON replace converter.tptpToDimacs with converter.tptpToJson.

Conversely, a DIMACS problem can be submitted to the TPTP and solved using

tptpClient.runSystem('E---', converter.dimacsToTptp('1 2 0 -1 0 -2 0'))
  .then(data => console.log(data.systemName, 'says', data.result))
  .catch(err => console.log(err));

or again with the classic callback function:

tptpClient.runSystem(
  'E---',
  converter.dimacsToTptp('1 2 0 -1 0 -2 0'),
  function(err,data)
  {
    if (err)
      console.log(err);
    else
      console.log(data.systemName, 'says', data.result);
  }
);

dimacsToTptp (data, dropComments)

Converts the data (a string) given in the CNF format for propositional problems proposed by DIMACS and used by SATLib into TPTP syntax.

Note that the converter assumes proper DIMACS syntax (clauses terminated by the digit 0), but is rather lenient regarding the specification line (starting with p) in that its existence is neither enforced nor is it used for checking the number of clauses or literals.

Comments are preserved unless parameter dropComments is supplied and evaluates to true.

peqToTptp (axioms, goals, varNamePattern)

Converts a pure (unit) equality problem into TPTP first-order form (fof). At the moment, neither types nor built-in theories are supported, and all variables are assumed to be universally quantified. (I.e., there is no support for quantifiers either.)

The conversion algorithm assumes standard syntax for unit equality, such as f(x,a) = x or f(x,inv(x)) = a(), for instance. Any characters except for opening and closing parenthesis, comma, '=', '!', and white spaces can be part of a name (of a variable, constant, or function). All white spaces are ignored.

If no pattern (regex) for variable names is provided through parameter varNamePattern, any name not followed by an opening parenthesis is assumed to be a variable. If a pattern is provided, then the name must additionally match the pattern to be a variable (see examples below).

Axioms can be given as a single string if there is but one axiom. Otherwise axioms must be provided as an array of strings. The same goes for goals. Goals may be provided as positive equations (using '=') or negative equations (using '!=') resulting in fof roles conjecture or negated_conjecture, respectively.

All variables are converted into X1, X2, and so on, depending on the order of appearance. Names of constants and functions are preserved as long as they comply with TPTP syntax. Otherwise they are replaced with lw_1, lw_2, and so on, depending on the order of appearance.

Examples:

If no pattern for variable names is given, any constants must be followed by an opening (and closing) parenthesis. Any other name is considered a variable. Thus,

console.log(converter.peqToTptp('f(a,b())=a','f(b(),x)=b()'));

produces

fof(ax1,axiom,(![X1]:f(X1,b)=X1)).
fof(goal1,conjecture,(![X1]:f(b,X1)=b)).

If a pattern is provided, constants can also be given without parentheses. In this example, a name starting with 'x', 'y', or 'z' (followed by zero or more digits) is considered a variable. Thus,

console.log(converter.peqToTptp(
  ['f(x,a)=x','f(x,i(x))=a','f(f(x,y),z)=f(x,f(y,z))'],
  ['f(a,x)=x','i(i(c))!=c'],
  /^[xyz]\d*$/)
);

produces

fof(ax1,axiom,(![X1]:f(X1,a)=X1)).
fof(ax2,axiom,(![X1]:f(X1,i(X1))=a)).
fof(ax3,axiom,(![X1,X2,X3]:f(f(X1,X2),X3)=f(X1,f(X2,X3)))).
fof(goal1,conjecture,(![X1]:f(a,X1)=X1)).
fof(goal2,negated_conjecture,(i(i(c))!=c)).

tptpToDimacs (data)

Converts the given data (a string) into the CNF format for propositional problems proposed by DIMACS and used by SATLib. The data must be a propositional problem specified in CNF (with all axiom sets included).

tptpToJson (data, dropTopLevelParentheses)

Converts the given data (a string) into the JSON format. The data can be an arbitrary TPTP problem, but all axiom sets must be included. This function returns an array of objects. Each object represents a formula of the given problem through the following properties:

• type: the type of the formula ('cnf', 'fof', etc)

• name: the name of the formula

• role: the role of the formula ('axiom', 'conjecture', etc)

• formula: the formula itself (all line feed characters, leading spaces, and comments have been removed)

• source: the source of the formula (this property may be undefined)

• info: optional information (this property may be undefined)

The type of all these property values is string.

If the optional parameter dropTopLevelParentheses is provided and evaluates to true then top-level parentheses enclosing formulas are removed. In both cases leading and trailing spaces are trimmed.