PL1RES

Find proofs in first-order predicate logic including equality using resolution and paramodulation, or find models for given sets of first-order clauses (with equality).

Quick Run

The proof search can be run from the command line. Run

$ node prove

for usage information.

Similarly, the model search can be run from the command line. Run

$ node find

for usage information.

Sample files can be found in the subdirectories of directory samples, organized into problems without equality (noeq) or with equality (eq), which are split into satisfiable (sat) and unsatisfiable (unsat) sets of clauses or formulas, respectively. The syntax of clauses and formulas is described below.

See appendix Run From Command Line for more details.

Clause Syntax

The syntax of clauses is based on a subset of the TPTP syntax for formulas in CNF.

In a nutshell, TPTP syntax adopts Prolog conventions. Hence, variable names start with an upper case letter (from the Latin alphabet). Function and predicate names start with a lower case letter (from the Latin alphabet). All names may contain digits, but not at the first position. We deviate slightly from the TPTP syntax in that we allow variables to begin with the underscore character '_'. The underscore character may also occur in predicate and function names except at the first position. Single-quoted predicate and function names are supported.

The logical disjunction that connects the literals of a clause is expressed through character '|', while negation is expressed through '~'.

As an example, take this set of three clauses: ['p(X_men) | q(X_men,Y)', '~q(a1,a2)', '~p(a1)']. There are two predicate symbols p and q, and two constants a1 and a2. The first clause has two literals and two variables X_men and Y.

Formula Syntax

The syntax of a first-order formula is based on a subset of the TPTP syntax for logic formulas. It is acceptable to omit the brackets surrounding the list of variables following a quantifier. For more details on predicate, function, or variable names consult Clause Syntax above.

Module Usage

const pl1res = require('pl1res');

pl1res exposes the functions

• createProver: to create a prover for a given set of first-order clauses (in CNF)
• createModelFinder: to search for a model of a given set of first-order clauses (in CNF)
• fofListToCnf: to convert first-order formulas (FOF) into an equivalent set of clauses (in CNF)
• tptpToCnf: to convert a TPTP problem into a set of clauses (in CNF)

Details are explained below.

createProver (clauses, options)

This function creates a prover for the given clauses in CNF. The clauses are supplied as an array of strings, with each string representing a clause. See Clause Syntax above for details. Use fofListToCnf to convert first-order formulas into a set of clauses in CNF. Use tptpToCnf to convert a TPTP problem into a set of clauses in CNF.

Note that we refer to a clause as an active clause if all possible factors and all possible resolvents between that clause and all other active clauses were created and added to the set of non-active or passive clauses. At the start of the proof search (i.e., when starting from scratch), there are no active clauses, and the set of passive clauses consists of all given or input clauses. One by one, employing heuristic selection criteria, passive clauses migrate to the set of active clauses, or in other words are activated. Active clauses take part in resolution and factorization (factoring), which derives new clauses that are added to the set of passive clauses. This procedure is typically referred to as saturation, and it continues until the empty clause is derived. Hence the prover is a saturation-based theorem prover.

A clause can be associated with a role. This can be achieved by providing a clause as an object instead of a string. The object must have the two properties clause and role, the former holding the clause as described above. The value of property role is also a string and must be one of the following TPTP roles: 'axiom', 'hypothesis', 'lemma', 'theorem', 'corollary', 'negated_conjecture'. Apart from these roles the role 'sos' is also recognized.

An alternative to the object is to add a role as a prefix to the string representing a clause, preceded by the character # and separated from the clause by at least one SPACE character, e.g.

'#axiom ~p(X) | p(s(X))'

which is equivalent to

{
  clause:'~p(X) | p(s(X))',
  role:'axiom'
}

Roles are employed to facilitate usage of the so-called Set of Support (SOS) strategy. See option sos of prover function run described below.

Parameter options is optional. If supplied it must be an object that can have the following properties:

• logger: a function that takes one string argument and consumes the provided information in a suitable way, e.g. console.log. The default is null.

• logLevel: the log level that determines the amount or detail of logged information; it should be a an integer between 0 and 5 (inclusive). The default is 0 and means no logging.

The return value of createProver is an object that acts as a prover. It offers the following properties, all of which are functions:

• run(options): starts or resumes a proof run. It returns the state of the prover, which is one of the following strings:

  • 'consistent': the set of clauses is consistent

  • 'inconsistent': the set of clauses is inconsistent, i.e. the empty clause was derived

  • 'stopped': the limit set through option maxClausesActivated or timeout was exceeded (see below)

  Parameter options is optional. If provided it must be an object that can have the properties listed below. Note that all options except logger, logLevel, maxClausesActivated and timeout are taken into account only when starting from scratch, i.e. the very first execution of run or any execution of rerun (described below).

  • logger: see option logger of createProver options; use this option to overwrite the currently used logger.

  • logLevel: see option logLevel of createProver options; use this option to overwrite the currently used log level.

  • maxClausesActivated: the maximal number of clauses that can be activated before the prover enters state stopped. Accepted values are integers greater than 0. Any other value grants the prover an unlimited number of clause activations. The default is no limit.

  • timeout: a timeout in milliseconds. Accepted values are non-negative integers. Any other value means no timeout. The default is no timeout.

  • fctWeight: the weight of predicate and function symbols used when computing the heuristic weight of a clause. It must be an integer greater than 0. The default is 2.

  • varWeight: the weight of variables used when computing the heuristic weight of a clause. It must be an integer greater than 0. The default is 1.

  • depthWeight: the weight of the depth component of the heuristic weight of a clause. It must be a non-negative integer. The default is 0, i.e. the depth of a clause is irrelevant. The depth of an input clause is 0. The depth of a derived clause is the maximum of the depths of its parent clauses (or clause in case of factorization) plus 1.

  • minWeightGiven: a flag that when set to a value equivalent to true assigns the minimal weight of 1 to all input clauses, with the effect that all input clauses will be activated before any other (derived) clause. The default is false.

  • sos: a specification for employing the Set of Support (SOS) strategy. If provided it must be an object with some or all of the following properties: ownSelectionWeight, otherSelectionWeight, roles. See appendix Set of Support for details.

  • useFVIndex: a flag that when set to a value equivalent to true enables the use of the feature vector indexing technique to speed up subsumption activities by reducing the number of failing subsumption attempts. See for instance this paper for details. The default is false.

  • patterns: defines a set of patterns employed to modify the weights of clauses exhibiting at least one of these patterns, typically to increase the weight and hence delay the selection of clauses deemed to be an impediment or distraction during proof search. See appendix Patterns for details.

  • preorder: an array of function symbols (i.e. strings) that provides the preorder of function symbols in descending order (i.e., greater symbols first) for the LPO (Lexicographic Path Ordering) that is employed for inferences and operations associated with equational reasoning in general and rewriting in particular. If no preorder is provided or the preorder is incomplete, the preorder will be set up or completed automatically simply by adding missing function symbols to the end of the array. This may lead to unpredictable or unwanted behavior, so the recommendation is to supply a complete preorder whenever equations are present.

  • indexingMatch: a flag that when set to a value equivalent to true enables the use of term indexing techniques for matching operations. The default is false.

• rerun(options): starts or restarts a proof run. It always starts from scratch and discards any data or results of a previous run. Parameter options is optional. For details see the description of parameter options of run. The return value of this function is the state of the prover. See run for details.

• getState(): returns the state of the prover as one of the strings 'consistent', 'inconsistent', or 'stopped'. See return value of run above for more details.

• getGivenClausesCount(): returns the number of given or input clauses

• getGivenClauses(withRole): returns the given or input clauses as an array of strings. If parameter withRole evaluates to true the role of each clause (that was assigned a role) is prepended as #<role>.

• getActiveClausesCount(): returns the number of active clauses

• getActiveClauses(): returns the active clauses as an array of strings

• getStatistics(): returns statistics as an object (properties with numerical values)

• getStatisticsAsString(): returns statistics as a formatted string

• getTimeElapsed(): returns the time elapsed during the most recent run as a human-readable string

• getHrtimeElapsed(): returns the time elapsed during the most recent run in process.hrtime format

• getProof(): returns the proof found. If no proof was found then null is returned. Otherwise the proof is returned as an object with the following properties, all of which are functions:

  • length(): returns the length of the proof, or in other words the total number of clauses involved in the proof (including the empty clause)

  • depth(): returns the depth of the proof, which is maximal depth of a leaf node when viewing the proof as a directed graph with the empty clause as its root, and input clauses as its leaves

  • efficiency(): returns the quotient between the proof length and the total number of clauses activated during proof search. This quotient is greater than 0 and not greater than 1. A quotient of 1 signifies a 'perfect' search in the sense that every activated clause contributed to the proof found.

  • efficiencyAsString(fl): returns the proof efficiency as a string, limiting the number of fractions to a maximum of 3, or as per fl if supplied as an integer number greater than zero

  • toString(): returns a string representation of the proof, which is a list of the clauses that constitute the proof, listed in the order in which they were activated, including information on their origins (i.e., whether a clause is an input clause, or whether it was derived from which clause or clauses through factorization or resolution); a clause ID preceded by the character '*' signifies that the clause is a member of the set of support.

• nonProofClausesCount(): returns the number of active clauses that did not play a role in the proof found. If no proof was found then the return value is undefined.

• nonProofClauses(): returns the set of active clauses that did not play a role in the proof found. If no proof was found then the return value is undefined. Otherwise the set of unused active clauses is returned as an array of strings. Each string represents an unused active clause. Note that the character '*' preceding the ID of a clause signifies that the clause is a member of the set of support. Furthermore we want to point out that the origin of a clause may refer to clauses that are neither in the proof found nor in this set of clauses. Such clauses were removed on account of backward subsumption.

• getSosOptions: returns the set-of-support options that were employed; the return value is null if the set-of-support strategy was not active. Otherwise it returns an object with the properties ownSelectionWeight, otherSelectionWeight, roles (cp. option sos of run and rerun; see appendix Set of Support for details).

Example

The following lines of code create a prover for a simple propositional problem, prove the inconsistency of the set of clauses with little output to the console, and then rerun the problem with more output to the console, and finally show the proof of inconsistency on the console:

const pl1res = require('pl1res'); // or whichever way the index module can be loaded
let prover = pl1res.createProver(['p1', '~p1 | p2', '~p2'],{logger:console.log, logLevel:1});
prover.run();
prover.rerun({logLevel:2});
console.log(prover.getProof().toString());

createModelFinder(clauses, options)

This function creates a model finder for the given clauses in CNF. See appendix Models and Sorts for details. The clauses are supplied as an array of strings, with each string representing a clause. See Clause Syntax above for details. Use fofListToCnf to convert first-order formulas into a set of clauses in CNF. Use tptpToCnf to convert a TPTP problem into a set of clauses in CNF.

Parameter options is optional. If supplied it must be an object that can have the following properties:

• logger: a function that takes one string argument and consumes the provided information in a suitable way, e.g. console.log. The default is null.

• logLevel: the log level that determines the amount or detail of logged information; it should be a an integer between 0 and 2 (inclusive). The default is 0 and means no logging.

The return value of createModelFinder is an object that acts as a model finder. It offers the following properties, all of which are functions:

• run(options): starts the model-finding procedure. It returns true if a model was found, false otherwise. Failure to find a model, even though a finite model exists and could theoretically be found, can have several reasons. If a timeout is set, then the timeout could be the reason. See also timeoutOccurred. Otherwise, the sizes of sorts may be unsuitable. Note that it is not necessarily the case that sort sizes are too small. TPTP problem KRS026+1.p, for instance, has a model that can be found if the size of the single sort involved is 1. When choosing sort size 2 or greater no model is found.

  Parameter options is optional. If supplied it must be an object that can have the following properties:

  • logger: see option logger of createModelFinder options; use this option to overwrite the currently used logger.

  • logLevel: see option logLevel of createModelFinder options; use this option to overwrite the currently used log level.

  • timeout: a timeout in milliseconds. Accepted values are non-negative integers. Any other value means no timeout. The default is no timeout.

  • sortsSizes: an array of integers to change the current sizes of sorts. An integer n greater than 0 at index i is accepted and overwrites the current sort size of sort i. Any other value retains the current size of sort i. See also getSortsCount and getSortSize, as well as setSortsSizes and setSortSize.

• getGivenClauses(withRole): returns the given clauses as an array of strings, optionally with their respective roles if parameter withRole is true.

• getGivenClausesCount(): returns the number of given clauses

• getSortsCount(): returns the number of sorts

• getSortSize(i): returns the sort size of the sort with index i. Valid sort indices range from 0 to getSortsCount() - 1. Note that the sort sizes may be different before and after a run depending on option sortsSizes.

• setSortsSizes(sizes): sets the sizes of sorts, where sizes is an array of integers. An integer greater than 0 at index i is accepted and overwrites the current sort size of sort i. Any other value retains the current size of sort i. The sizes of sorts can also be modified through option sortsSizes when running the model finder. However, when only model checking is required, this is a way to change sizes of sorts. See also setSortSize.

• setSortSize(i, s): sets the size of sort i to be s, where s must be an integer greater than 0. Any other value will be ignored. The sizes of sorts can also be modified through option sortsSizes when running the model finder. However, when only model checking is required, this is a way to change the size of a sort. See also setSortsSizes.

• getPredicates(): returns the predicate names as an alphabetically sorted array of strings

• getPredicateArgSorts(name): returns the argument sorts of the predicate specified through parameter name as an array of integers (i.e., sort indices)

• getFunctions(): returns the function names as an alphabetically sorted array of strings

• getFunctionArgSorts(name): returns the argument sorts of the function specified through parameter name as an array of integers (i.e., sort indices)

• getFunctionValSort(name): returns the sort of the function value of the function specified through parameter name as an integer (i.e., a sort index)

• getTimeElapsed(): returns the time elapsed during the most recent run as a human-readable string

• getHrtimeElapsed(): returns the time elapsed during the most recent run in process.hrtime format

• timeoutOccurred(): returns true if the most recent run timed out, false otherwise. See also run.

• getModel(): returns the model found in the most recent run, null otherwise. If a model was found it is an instance of Model (described below).

• getModelTemplate(): returns an instance of Model (described below). The model returned is initialized with undefined values for all predicates and functions. Sort sizes are inherited from the model finder. Use the setSortSize or setSortsSizes to modify sort sizes of this model instance. Such a model can be used as a template to set function and predicate values and check whether the model thus configured satisfies the given clauses.

• getModelSearchStatistics(): returns search statistics as an object with the following properties (use the object's toString() to obtain the statistics in a formatted and comprehensible form):

  • literalsVisited: the number of clause literals processed during the search

  • backwardSteps: the number of backtracking steps

Model

An instance of Model offers the following functions to modify or query the model it represents (see also appendix Models and Sorts):

• getSortsCount(): returns the number of sorts

• getSortSize(i): returns the sort size of the sort with index i. Valid sort indices range from 0 to getSortsCount() - 1.

• setSortsSizes(sizes): sets the sizes of sorts, where sizes is an array of integers. An integer greater than 0 at index i is accepted and overwrites the current sort size of sort i. Any other value retains the current size of sort i. See also setSortSize.

• setSortSize(i, s): sets the size of sort i to be s, where s must be an integer greater than 0. Any other value will be ignored. See also setSortsSizes.

• check(): returns true if this model satisfies the given clauses (of the associated model finder this model or template was obtained from), false otherwise. This method throws an exception if the satisfiability status cannot be ascertained because of undefined values.

• getPredicateValue(name, ...): returns the current value of the predicate with the given name and the given argument sort elements (represented by '...'). The value can be either true, false, or null, the latter representing undefined.

• getFunctionValue(name, ...): returns the current value of the function with the given name and the given argument sort elements (represented by '...'). The value can be either an integer, i.e. an element of the sort of the respective function value, or null, the latter representing undefined.

• setPredicateValue(name, b, ...): sets the Boolean value b for the predicate with the given name and the given argument sort elements (represented by '...')

• setFunctionValue(name, e, ...): sets the value e for the function with the given name and the given argument sort elements (represented by '...'). Value e must be an index for the value sort

• set(modelSpec): sets predicates or function values as per modelSpec. Parameter modelSpec can be an array of strings, where each string defines a function or predicate value, or alternatively modelSpec can be a string where the definition of function or predicate values are separated through the linefeed character. See appendix Models and Sorts for details.

• clear(): removes all values, thus making all predicates and functions undefined

• toString(): returns a human-readable string version of the model which can be used as parameter modelSpec of set

fofListToCnf (fofList)

This function converts a list of first-order formulas (see Formula Syntax above) into a logically equivalent set of clauses (in CNF). In other words the return value of this function is an array that can be used as parameter clauses of createProver or createModelFinder. A list of formulas is supplied through parameter fofList as an array. Each element of the array represents a formula. Similar to clauses (cp. parameter clauses of function createProver) a formula can be specified as a string with the optional role prefix, e.g.

#conjecture ?X:(isCretan(X) & ~isLiar(X))

or an object (representing the same formula as the one above):

{
  formula: '?X:(isCretan(X) & isLiar(X))',
  role: 'conjecture'
}

The following TPTP roles are accepted: 'axiom', 'hypothesis', 'lemma', 'theorem', 'corollary', 'conjecture', 'negated_conjecture'. Apart from these roles the role 'sos' is also recognized.

tptpToCnf (tptpProblem)

This function converts a TPTP problem (given as a string) into a set of clauses that can be passed to createProver or createModelFinder. In other words the return value of this function is an array that can be used as parameter clauses of createProver or createModelFinder.

All include statements of the TPTP problem (if any) must have been resolved prior to calling this function. A given TPTP problem may contain only the TPTP languages cnf or fof. The roles of clauses or formulas in the original TPTP problem are inherited by the clauses in the returned array. Formulas with the role conjecture are transformed into clauses with the role negated_conjecture.

If you wish to download a TPTP problem (with all include statements resolved) we recommend using package tptp, and in particular function getProblemWithAxiomSetsIncluded of the tptpClient.

Appendix

Run From Command Line

Use prove.js to run the prover from the command line. prove.js is a convenience program that utilizes the index module to tackle problems in CNF or FOF. Execute

node prove

for usage information.

Similarly, find.js can be used to run the model finder from the command line.

Problems can be specified in a simple format or in the TPTP format. (See files in directory samples/noeq/unsat and samples/noeq/sat, containing unsatisfiable and satisfiable problems without equality, respectively. See files in directory samples/eq/unsat and samples/eq/sat, containing unsatisfiable and satisfiable problems with equality, respectively.) If a file name fits the TPTP problem name format, it is assumed to be a TPTP problem. File names for the simple format should use the extensions .cnf and .fof if CNF or FOF is used, respectively.

It is worth noting that it is possible to pipe problems, and in particular TPTP problems, to prove or find, which comes in particularly handy if a TPTP client such as the client provided by package tptp is available. Assuming package tptp is installed side-by-side with package pl1res the following command line downloads TPTP problem MSC001-1.p, lists the initial set of clauses and proves it to be inconsistent:

node ../tptp/tptpClient -pi MSC MSC001-1.p | node prove -li -l1 =tptp

Similarly, the following command line downloads TPTP problem LCL078-1.p, lists the initial set of clauses, finds a model and shows that model:

node ../tptp/tptpClient -pi LCL LCL078-1.p  | node find -li -l1 -m =

Note that the TPTP format is the default for the piping operation. Hence using = is equivalent to =tptp. If files of the simple format are to be piped use =cnf or =fof, respectively.

Set of Support

The set of support strategy, or its variant implemented here, proceeds as follows. In the beginning, it labels certain initial clauses as members of the set of support. They nonetheless start out as passive clauses in the sense outlined above. Members of the set of support, and other passive clauses, are selected based on a weighting scheme, e.g. two passive clauses from the set of support for each other passive clause.

A selected clause of the (passive) set of support becomes an active set of support clause. A clauses derived with the help of at least one clause from the set of support will itself also become a clause of the (at first passive) set of support. Should the passive set of support run dry at some point the weighting scheme is suspended until such clauses become available again. In other words the prover will not stop because there are no more set of support clauses, and simply continue with whatever clauses are at its disposition.

The weighting scheme is specified through the properties ownSelectionWeight and otherSelectionWeight. Thus, if you want the scheme to be two set of support clauses for one other clause, then specify option sos to be

sos:{
  ownSelectionWeight: 2,
  otherSelectionWeight: 1
}

If not supplied each of these weights defaults to 1. Note that it is possible to choose the weight 0 in both cases. Weight 0 implies that the respective type of clause is selected only if there are no more passive clauses of the other kind. Choosing 0 for both weights is effectively the same as

sos:{
  ownSelectionWeight: 1,
  otherSelectionWeight: 0
}

Keep in mind that a weight of 0 can easily destroy completeness of the prover in the sense that a proof will never be found, even if one exists.

The initial assignment to the set of support is accomplished through the roles of the clauses. The special role sos always puts the respective clause into the set of support. Other roles are treated like role sos with the help of property roles, an array of role names. For instance, the following set of support specification puts all negated conjectures and lemmas into the set of support (as well as all clauses with roles sos), and sets up a weighting scheme of 3:1 in favor of set of support clauses:

sos:{
  ownSelectionWeight: 3,
  otherSelectionWeight: 1,
  roles:['negated_conjecture', 'lemma']
}

Note that the set of support strategy is active only if option sos is present. Hence having clauses with role sos does not suffice. Option sos must be supplied, if only as an empty object.

Finally, a set of support clause is shown with character '*' preceding its ID when logging at level 2 or greater during a proof run, or when obtaining the list of clauses that did or did not contribute to a proof eventually found.

Patterns

A pattern is specified through an object with the properties pattern and mod. The set of patterns is an array of such objects. The value of property pattern is a string that defines a pattern. A pattern is a term construed with functions symbols and the following special symbols:

• *: matches any term

• +: matches any term except variables

• ?: matches any variable

As an example consider sub(sub(*)), for instance. This pattern matches any term of the form sub(sub(t)), where t is any arbitray term. A pattern matches a clause if it matches any of the terms occurring in that clause, or more precisely in arguments of the literals of that clause.

The first pattern of the set of patterns to match a clause determines the weight modification of that clause. The modification of the weight is controlled through the second property mod. It can be a number or a function that accepts one argument, namely the original weight of the clause, and returns the modified weight for that clause. Providing a number n is a shortcut for the function w => w + n.

Let us take a look at TPTP problem PUZ005-1.p from domain PUZ. With the standard weighted symbol count this problem is rather elusive to classic resolution. It is well known that the appearance of numerous clauses with nested occurrences of the function symbol yesterday uses up resources to no avail. The following set of patterns (consisting of just one pattern) counters this problem:

patterns: [{
  pattern:'yesterday(yesterday(*))',
  mod:30
}]

Combine this pattern with the set of support strategy:

sos:{
  roles:['negated_conjecture'],
  ownSelectionWeight:1,
  otherSelectionWeight:1
}

and PUZ005-1.p can be proved to be inconsistent in no time at all. See also samples/noeq/unsat/options.json or execute

node prove samples/noeq/unsat/PUZ005-1.p -O samples/noeq/unsat/options.json

The concept of patterns in its current simple form can and may be extended and enhanced in the future.

Models and Sorts

The model finder implemented here can find simple finite models. It begins by extracting the signature from the set of given clauses, and computing a set of sorts and assigning a number of elements (default sizes) to each sort. Finally the algorithm attempts to construct a model within the limits of the sort information and backtracks if it hits a deadend. The algorithm is guaranteed to stop after finding a model or after exploring all branches without success, or incurring a timeout, if a timeout was set.

Disclaimer: The simple algorithm currently implemented falls prey to the so-called combinatorial explosion very easily. It may occasionally be possible to mitigate the effects of said "explosion" by curbing the sizes of sorts when the default sizes are greater than necessary. Note that the default sizes originate from a heuristic that may of course pick a wrong number, which is not necessarily a number that is too small, although that is the most likely scenario.

Example: Let there be the two clauses p(f(X),X) | q(X) and ~q(a). Predicate p has two argument sorts, q has one, function f has one argument sort and one value sort, and constant a has a value sort. The nesting of the function and constant, as well as the use of variable X in the first clause results in two sorts represented by their zero-based indices 0 and 1, where the argument sorts of p are 0 and 1, the argument sort of q is 1, the argument sort of f is 1 and its value sort 0, and the value sort of a is 1. Using a mathematical notation style, with sorts 0 and 1 represented by S0 and S1, respectively, the full signature with sorts looks like this

p : S0 x S1 --> Boolean
q : S1 --> Boolean
f : S1 --> S0
a : --> S1

Assuming that mf is the model finder, then this information can be retrieved as follows:

• mf.getPredicateArgSorts('p') which will return [0, 1]
• mf.getPredicateArgSorts('q') which will return [1]
• mf.getFunctionArgSorts('f') which will return [1]
• mf.getFunctionValSort('f') which will return 0
• mf.getFunctionValSort('a') which will return 1

Each sort holds a number of elements that are determined heuristically. For the example above this means that sort 0 holds two elements, whereas sort 1 has a single element. The number of elements of each sort can be overwritten with option sortsSizes as explained in section createModelFinder. Note that elements of sorts are also represented through their zero-based indices, i.e. 0 and 1 for the example. Despite the same index, elements of two different sorts are technically two different entities.

We should point out at this stage that there is of course no guarantee that a finite model exists to begin with, or that one exists for the default or chosen sort sizes.

After running the model finder mf for the clauses of the example, mf.getModel() returns a model m so that the following is true:

• m.getSortsCount() === 2, i.e. there are two sorts
• m.getSortSize(0) === 2, i.e. sort 0 has two elements (determined heuristically)
• m.getSortSize(1) === 1, i.e. sort 1 has one element (determined heuristically)
• m.check() === true, which confirms that the model satistfies the given clauses
• m.getPredicateValue('p', 0, 0) === true, i.e. predicate p is true for elements 0 and 0 of sorts 0 and 1, respectively
• m.getPredicateValue('p', 1, 0) === null, i.e. predicate p is undefined for elements 1 and 0 of sorts 0 and 1, respectively
• m.getPredicateValue('q', 0) === false, i.e. predicate q is false for element 0 of sort 1
• m.getFunctionValue('f', 0) === 0, i.e. function f maps element 0 of sort 1 to element 0 of sort 0
• m.getFunctionValue('a') === 0, i.e. constant a has element 0 of sort 1 as its value
• m.toString() === 'a => 0\nf(0) => 0\np(0,0) => true\np(1,0) => *\nq(0) => false'

Note that an undefined value simply means that the respective value is irrelevant and could be any value. In this simple example the size of sort 0 can be reduced to 1 and still a model will be found.

It is also possible to try one's hand at model creation from scratch. In the example below the same set of claues is used as before, and the size of sort 0 is reduced to 1, which means that both sorts only have one element referenced through index 0:

const { createModelFinder } = require('pl1res'); // or whichever way the index module can be loaded
const m = createModelFinder(['p(f(X),X) | q(X)', '~q(a)']).getModelTemplate();
m.setSortSize(0, 1);
m.set(['p(0,0) => T', 'q(0) => F', 'f(0) => 0', 'a => 0']);

Running m.check() returns true. Note that apart from T and F for the Boolean values true and false, respectively, it is also possible to use true and false. That is,

m.set(['p(0,0) => true', 'q(0) => false', 'f(0) => 0', 'a => 0']);

accomplishes the same. Undefined values can, but do not have to, be explicitly provided using the asterisk, e.g. f(0) => *. Note that set works incrementally in that it adds or maybe overwrites, but never removes previously set values. Use clear to remove all previously set values.