home about



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.







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.

For information about OEMM notation, please see below.

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

3.2 Defining Symbols

3.3 Defining Sentences

3.4 Defining Models

3.5 Defining Conjectures

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





4. Frequently Asked Questions

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.





home about


Public domain. This website is still under construction.