Wolfram Function Repository
Instantuse addon functions for the Wolfram Language
Function Repository Resource:
Finds finite models consistent with the set of relations
ResourceFunction["FindFiniteModels"][rels] finds models in form of multiplication tables consistent with the relations rels for each operator in rels, assuming each variable can have one of 2 values. 

ResourceFunction["FindFiniteModels"][rels,k] allows k≥2 values for each variable. 

ResourceFunction["FindFiniteModels"][rels,k,prop] returns a specified property prop of found models. 
"Association"  returns an association with multiplication tables as values and indices as keys for each found model (default) 
"Indices"  returns a list of indices for models 
Method  "ExpressionPrune"  the method to use 
"Parallelize"  False  whether to run some operations in parallel 
MaxItems  Infinity  limit the number of returned models 
"ExpressionPrune"  pruned search over relations converted to a conjunction of DNFs 
"BruteForce"  a complete search over all possible models 
Automatic  same as “ExpressionPrune” 
Find binary models for a nullary operator:
In[1]:= 

Out[1]= 

Find ternary models for a nullary operator:
In[2]:= 

Out[2]= 

Find binary models for unary operators:
In[3]:= 

Out[3]= 

In[4]:= 

Out[4]= 

In[5]:= 

Out[5]= 

Find binary models for a binary operator:
In[6]:= 

Out[6]= 

Find ternary models for a binary operator:
In[7]:= 

Out[7]= 

Find binary models for a ternary operator:
In[8]:= 

Out[8]= 

Include constants:
In[9]:= 

Out[9]= 

In absence of operators FindFiniteModels assumes all atoms are nullary operators:
In[10]:= 

Out[10]= 

Multiple operators with different arities is supported:
In[11]:= 

Out[11]= 

Inequalities:
In[12]:= 

Out[12]= 

In[13]:= 

Out[13]= 

In[14]:= 

Out[14]= 

Alternatives:
In[15]:= 

Out[15]= 

Disjunctions:
In[16]:= 

Out[16]= 

Quantifiers:
In[17]:= 

Out[17]= 

In[18]:= 

Out[18]= 

String relations have additional axioms:
In[19]:= 

Out[19]= 

String relations form a monoid with binary associative operator ∘ (\[SmallCircle]) and nullary identity 1:
In[20]:= 

Out[20]= 

"BruteForce" method may be useful if a relation is very general so that enumerating models and finding a small subset of them returns faster:
In[21]:= 

Out[21]= 

In[22]:= 

Out[22]= 

Setting the option "Parallelize" to True may speed up computation:
In[23]:= 

Out[23]= 

In[24]:= 

Out[24]= 

In[25]:= 

Out[25]= 

In[26]:= 

Out[26]= 

Limiting a number of returned models reduces an amount of performed computation:
In[27]:= 

Out[27]= 

Find models for abelian semigroup theory axioms:
In[28]:= 

Out[28]= 

Reproduce and extend some :
In[29]:= 

In[30]:= 

In[31]:= 

In[32]:= 

In[33]:= 

Find models for the Wolfram axiom:
In[34]:= 

Out[34]= 

In[35]:= 

Out[35]= 

In[36]:= 

Out[36]= 

AxiomaticTheory examples:
In[37]:= 

Out[37]= 

In[38]:= 

Out[38]= 

In[39]:= 

Out[39]= 

In[40]:= 

Out[40]= 

In[41]:= 

Out[41]= 

In[42]:= 

Out[42]= 

In[43]:= 

Out[43]= 

This work is licensed under a Creative Commons Attribution 4.0 International License