Wolfram Function Repository
Instant-use add-on functions for the Wolfram Language
Function Repository Resource:
Find 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 two 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 are 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[22]= | ![]() |
In[23]:= | ![]() |
Out[24]= | ![]() |
Setting the option "Parallelize" to True may speed up computation:
In[25]:= | ![]() |
Out[25]= | ![]() |
In[26]:= | ![]() |
Out[26]= | ![]() |
In[27]:= | ![]() |
Out[27]= | ![]() |
In[28]:= | ![]() |
Out[28]= | ![]() |
Limiting a number of returned models reduces an amount of performed computation:
In[29]:= | ![]() |
Out[30]= | ![]() |
Define functions to be used throughout this example:
In[31]:= | ![]() |
Find models for abelian semigroup theory axioms:
In[32]:= | ![]() |
Out[32]= | ![]() |
Reproduce and extend some NKS book examples:
In[33]:= | ![]() |
In[34]:= | ![]() |
In[35]:= | ![]() |
In[36]:= | ![]() |
In[37]:= | ![]() |
Find models for the Wolfram axiom:
In[38]:= | ![]() |
Out[38]= | ![]() |
In[39]:= | ![]() |
Out[39]= | ![]() |
In[40]:= | ![]() |
Out[40]= | ![]() |
AxiomaticTheory examples:
In[41]:= | ![]() |
Out[41]= | ![]() |
In[42]:= | ![]() |
Out[42]= | ![]() |
In[43]:= | ![]() |
Out[44]= | ![]() |
In[45]:= | ![]() |
Out[45]= | ![]() |
In[46]:= | ![]() |
Out[46]= | ![]() |
In[47]:= | ![]() |
Out[47]= | ![]() |
In[48]:= | ![]() |
Out[48]= | ![]() |
This work is licensed under a Creative Commons Attribution 4.0 International License