Wolfram Function Repository
Instant-use add-on 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