Online Encyclopedia ofMathematical Models. Models. boolean algebras, lattices, directed sets, equivalence relations, graphs, directed graphs, bipartite graphs, pre-orderings, strict partial orders, strict weak orderings, partial orderings, weak orderings, total orderings, groups, rings, fields, racks, quandles, Tarski's HS Algebra, more coming soon.

## 1. What is OEMM (Online Encyclopedia of Mathematical Models)?

Akin to studying the smallest primes, we study the smallest models of given axioms. We hope to notice patterns in the models which reveal the underlying nature of the models.

OEMM is a repository, indexed by axioms, of finite mathematical models. Also, we are interested in computer programs which enumerate specific models -- for certain axioms, we can limit the search-space, or better yet, construct models without search.

Besides studying models for their own sake, we are interested in applications, including (i) refuting conjectures by finding counterexample models, (ii) searching for alternative equivalent axioms with specific properties, (iii) finding "canonical" models which decide all conjectures up to a given length, and (iv) whether properties of small models also hold for arbitrarily large models. We welcome more applications.

For details, a draft of a whitepaper is also available.

## 2. Manual For The "Tools For Mathematical Models" On The Front Page.

The model enumerator is a naive (but generic) brute-force search. The model enumerator has three steps: (i) a parser reads the symbols and axioms, (ii) a code generarator outputs javascript code to enumerate models, and (iii) this generator enumerates candidate models and only prints those which satisfy the axioms. Although this is a prohibitively slow brute-force search, it works for any given axioms. For debugging, the model enumerator also allows printing the syntax tree and printing generated code. The C code should run faster than the JavaScript which runs in the browser. The order in which the axioms are defined affects the runtime of the model enumerator; the smallest strict axiom should be first, because this allows quickly rejecting candidate models.

The conjecture enumerator builds sentences using the symbols used in the axioms. "Length" is the number of non-parentheses symbols in the sentence.

The conjecture refutor takes the conjectures and checks them against the generated models. If a sentence does not satisfy a single model of the axioms, then it does not follow from the axioms, i.e. it is refuted. The non-refuted conjectures can be proved by hand.

### TroubleShooting

Because the algorithms are exponential in size and time, the browser may only be able to handle the smallest cases. It is useful to monitor the browser developer tools, often accessible with alt+ctrl+i. There, you will see the browser's error messages such as "out of memory". Using different browsers may help, it seems Firefox is better at model enumeration and Chromium is better at conjecture enumeration and refutation.

## 3. The OEMM Notation

OEMM uses text files to store axioms and models. The structure of each text file is as follows.

### 3.1 The Overall File Structure

• Each file contains of a list of definitions, each beginning with a keyword `relation`, `function`, `constant`, `variable`, `axiom`, `sentence`, or `model`.
• Whitespace is ignored. Everything can be defined in one line without spaces. Definitions could last for many lines. But multi-character symbols and keywords must have no whitespaces between characters.
• Comments begin with `#` and last until the end of the line.
• For shorthand notation, if the same keyword is used consecutively, it can be replaced by a comma `,` symbol.

### 3.2 Defining Symbols

• A symbol definition begins with a keyword `relation`, `function`, `constant`, or `variable`.
• Next, the user chooses a "symbol", a string of non-whitespace UTF-8 ("Unicode") character(s). Symbols can be copied/pasted from wikipedia. To avoid ambiguity, no symbol can be the initial substring of any other symbol or keyword, which include `(`, `)`, `~`, `¬`, `/\`, `⋀`, `\/`, `⋁`, `->`, `⟶`, `<->`, `⟷`, `A`, `∀`, `E`, `∃`, `v`, `#`, `constant`, `function`, `relation`, `variable`, `axiom`, `model`, `sentence`.
• Functions and relations require defining their integer ≥1 number of arguments, specified in parentheses following the symbol.
Optionally, the default prefix ("Polish") notation can be overridden for binary symbols to `infix`, allowing e.g. `x+y` instead of `+xy`. This is specified after the number of arguments and a comma.
Optionally, if the behavior of function or relation known beforehand, it can be specified by code in curly brackets which evaluates to their value. This code is a C and Javascript expression, and the arguments of are represented as `a0`, `a1`, ..., `an`. This expression is used blindly, and can result in undefined behavior.
• Defining variable symbols is optional. You can use built-in variable names `v0`, `v1`, `v2`, ... .
• When a constant is defined as a number `0`, `1`, `2`, ..., it takes that value in models. When a constant is known to be non-equal to any other constant, it is wise to define it as the smallest unused non-negative integers.

### 3.3 Defining Sentences

• Logic symbols can be ascii symbols `/\`, `\/`, `->`, `<->`, `A`, `E`, or respective utf-8 symbols `¬`, `⋀`, `⋁`, `⟶`, `⟷`, `∀`, `∃` (whose codepoints are 00ac, 22c0, 22c1, 27f6, 27f7, 2203, 2200).
• The structure of each sentence is defined by the following syntax (the vertical bar | is read "or").
``` formula := (formula) | relation term(s) | term binaryInfixRelation term | ¬ formula | formula ⋀ formula | formula ⋁ formula | formula ⟶ formula | formula ⟷ formula | ∀ variable formula | ∃ variable formula term := (term) | const | var | func term(s) | term binaryInfixFunction term ```
• Precedence:
• Parentheses have the highest precedence.
• Symbols `¬`, `∀`, `∃` have precedence over `⋀`, `⋁`, `⟶`, and `⟷`.
• Symbols `⋀`, `⋁`, `⟶`, and `⟷` have no defined precedence. Use parentheses to specify precedence.
• User-named symbols have no defined precedence. Use prefix notation or use parentheses to specify precedence.
• Associativity: infix logic, funcion, and relation symbols are always left-associative. For example, a+b*c means (a+b)*c. Use parentheses if needed.
• Fixity:
• Symbols `¬`, `∀`, `∃` are prefix.
• Symbols `⋀`, `⋁`, `⟶`, and `⟷` are infix.
• User defined symbols are prefix, unless specified with keyword `infix`.
• Variables occurances must be quantified i.e. no "free" variable occurances allowed. Free variables result in undefined behavior.

### 3.4 Defining Models

• Models are defined with keyword `model` followed by a name of form `n_m` where n is the model size and m is a non-negative integer index for that size. Next is the symbol, and finally an array of space-separated numbers representing the table for that symbol.
• The tables contain numbers from the underlying set, which is `{0,1,2,...,n}` for model size n+1. The model has rows/columns indexed by elements of this set.
• Models must appear after all declarations of symbols and axioms, i.e. the models are with respect to the above symbols and axioms.

### 3.5 Defining Conjectures

• Like axioms but with keyword `sentence`.
• Must appear after all models which they were tested against.

### 3.6 An Reasonably Exhaustive Example

``````#axioms of group theory

relation	=(2,infix)	{a0==a1}
function	⚬(2,infix)
constant	0
variable	x,y,z

axiom   	∀x∀y∀z (x⚬y)⚬z = x⚬(y⚬z)	#associative
axiom   	∀x x⚬0=x			#identity
axiom   	∀x ∃y x⚬y=0			#inverse

model 1_1
⚬
0

model 2_1
⚬
0 1
1 0

model 3_1
⚬
0 1 2
1 2 0
2 0 1

#conjectures tested against above models:
sentence   ∀x∀y x⚬y = y⚬x	#commutative, could be refuted by model of size 6
,          ∀x∀y ¬x⚬y = y⚬x	#anti-commutative, refuted by above models

```
```

### What are these strange box or question mark symbols?

This webpage should automatically use Unicode (UTF-8) for mathematical symbols. If you see question marks, boxes, or strange symbols, please adjust your browser. The following are settings for common browsers.
``` Firefox: Options -> Customize -> Text Encoding -> Select text encoding -> Unicode. Chromium: Options -> More Tools -> Encoding -> Unicode. ```

### What can I do to help?

Come up with some good ways to enumerate models. And apply models to solve problems.
``````
```
```