Function Repository Resource:

# FindCombinatorProof

Attempt to find a proof of a theorem in combinatory logic using a given combinatory calculus

Contributed by: Jonathan Gorard
 ResourceFunction["FindCombinatorProof"][thm,<|"Combinators"→comb,"Rules"→rules|>] tries to find an equational proof of the combinatory logic theorem thm using the combinators comb and reduction rules rules. ResourceFunction["FindCombinatorProof"][thm,calc] tries to find an equational proof of the combinatory logic theorem thm using the named combinatory calculus calc.

## Details and Options

If ResourceFunction["FindCombinatorProof"][thm,calc] succeeds in deriving the theorem thm from the combinatory calculus calc, then it returns a ProofObject expression. If it succeeds in showing that the theorem cannot be derived from the combinatory calculus, it returns a Failure object. Otherwise, it may not terminate unless time constrained.
ResourceFunction["FindCombinatorProof"] accepts both standard (named) combinatory calculi and arbitrary calculi specified via combinator reduction rules.
ResourceFunction["FindCombinatorProof"] accepts both individual theorems and lists of theorems.
ResourceFunction["FindCombinatorProof"] has the following options:
 TimeConstraint Infinity how much time to allow
If ResourceFunction["FindCombinatorProof"] exceeds the specified time constraint, it returns a Failure object.
ResourceFunction["FindCombinatorProof"][thm,calc] uses the Knuth-Bendix completion algorithm to prove that the theorem thm follows from the reduction rules of the combinatory calculus calc.

## Examples

### Basic Examples (3)

Prove an elementary theorem about the single-variable fixed-point (y) combinator, with the reduction rule explicitly specified:

 In[1]:=
 Out[1]=

Show the abstract proof network, with tooltips showing the intermediate expressions:

 In[2]:=
 Out[2]=

Show the complete list of proof steps as a Dataset object:

 In[3]:=
 Out[3]=

Typeset a natural language argument:

 In[4]:=
 Out[4]=

Prove a more sophisticated theorem involving the S-K combinatory calculus:

 In[5]:=
 Out[5]=

Show the abstract proof network:

 In[6]:=
 Out[6]=

Prove a theorem using one of FindCombinatorProof's built-in combinatory calculi (Schönfinkel's B-C-I calculus):

 In[7]:=
 Out[7]=

Show the abstract proof network:

 In[8]:=
 Out[8]=

### Scope (7)

Show that a combinator equivalence proposition cannot be derived from a given combinatory calculus:

 In[9]:=
 Out[9]=

#### Named Combinatory Calculi (6)

FindCombinatorProof supports a variety of named combinatory calculi, including the single-variable fixed-point (y) combinator:

 In[10]:=
 Out[10]=

The two-variable fixed-point (y) combinator:

 In[11]:=
 Out[11]=

The S-K calculus:

 In[12]:=
 Out[12]=

The S-K-I calculus:

 In[13]:=
 Out[13]=

Schönfinkel's B and C combinators:

 In[14]:=
 Out[14]=

The B-C-I calculus:

 In[15]:=
 Out[15]=

#### Initial Conditions (1)

FindCombinatorProof accepts both individual theorems and lists of theorems:

 In[16]:=
 Out[16]=
 In[17]:=
 Out[17]=

### Options (1)

#### TimeConstraint (1)

Use to limit the computation time to t seconds:

 In[18]:=
 Out[18]=
 In[19]:=
 Out[19]=

### Properties and Relations (1)

FindCombinatorProof will return a proof object for a particular theorem if and only if the associated path exists in the corresponding multiway system:

 In[20]:=
 Out[20]=
 In[21]:=
 Out[21]=
 In[22]:=
 Out[22]=
 In[23]:=
 Out[23]=

Jonathan Gorard

## Version History

• 1.0.0 – 04 December 2020