Online Encyclopedia of
Mathematical 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. |

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.

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.

- 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.

- 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.

- 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`

.

- Symbols
- Variables occurances must be quantified i.e. no "free" variable occurances allowed. Free variables result in undefined behavior.

- 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.

- Like axioms but with keyword
`sentence`

. - Must appear after all models which they were tested against.

```
#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
```

```
Firefox: Options -> Customize -> Text Encoding -> Select text encoding -> Unicode.
```

Chromium: Options -> More Tools -> Encoding -> Unicode.

```
```