# Theory ABSTRACT-ALGEBRA

Defines the basic vocabulary for describing algebraic operators, domains, and structures such as fields, rings, and groups.

### Theories included by Abstract-Algebra:

```    Frame-Ontology
Kif-Relations
Kif-Sets
Kif-Lists
Kif-Numbers```

### Theories that include Abstract-Algebra:

```    Physical-Quantities
Unary-Scalar-Functions
Cml
Thermodynamics
Dme
Thermodynamics
Standard-Units
Simple-Bikes
Cml ...
Vt-Design
Simple-Bikes
Vt-Domain
Vt-Example
Unary-Scalar-Functions ...
Scalar-Quantities
Vt-Design ...
Vector-Quantities```

### No instances defined.

The following constants were used from included theories:

All constants that were mentioned were defined.

## Relation BINARY-OPERATOR-ON

A function is a binary operator on a domain if it is closed on the domain, that is, it is defined for all pairs of objects that are instances of the domain and its value on all such pairs is an instance of the domain.
Arity: 2
Domain: Binary-function
Axioms:
```(<=> (Binary-Operator-On ?Function ?Domain)
(And (Binary-Function ?Function)
(Forall (?X ?Y)
(=> (And (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain) )
(Instance-Of (Value ?Function ?X ?Y) ?Domain) ))))

```

## Relation ASSOCIATIVE

Arity: 2
Axioms:
```(<=> (Associative ?Op ?Domain)
(Forall (?X ?Y ?Z)
(=> (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(Instance-Of ?Z ?Domain)
(= (Value ?Op ?X (Value ?Op ?Y ?Z))
(Value ?Op (Value ?Op ?X ?Y) ?Z) ))))

```

## Relation COMMUTATIVE

Arity: 2
Axioms:
```(<=> (Commutative ?Op ?Domain)
(Forall (?X ?Y)
(=> (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(= (Value ?Op ?X ?Y) (Value ?Op ?Y ?X)) )))

```

## Relation INVERTIBLE

Arity: 3
Axioms:
```(<=> (Invertible ?Op ?Id ?Domain)
(Forall (?X)
(=> (Instance-Of ?X ?Domain)
(Exists (?Y)
(And (Instance-Of ?Y ?Domain)
(= (Value ?Op ?X ?Y) ?Id)
(= (Value ?Op ?Y ?X) ?Id) )))))

```

## Relation DISTRIBUTES

Arity: 3
Axioms:
```(<=> (Distributes ?Op ?G ?Domain)
(And (Binary-Operator-On ?Op ?Domain)
(Binary-Operator-On ?G ?Domain)
(Forall (?X ?Y ?Z)
(=> (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(Instance-Of ?Z ?Domain)
(= (Value ?Op (Value ?G ?X ?Y) ?Z)
(Value ?G
(Value ?Op ?X ?Z)
(Value ?Op ?Y ?Z) ))))))

```

## Relation IDENTITY-ELEMENT-FOR

An object ?id is the identity element for binary operator ?o over domain ?d iff for every instance ?x of ?d, applying ?o to ?x and ?id results in ?x.
Arity: 3
Axioms:
```(<=> (Identity-Element-For ?Id ?Op ?Domain)
(And (Instance-Of ?Id ?Domain)
(Binary-Operator-On ?Op ?Domain)
(Forall (?X)
(=> (Instance-Of ?X ?Domain)
(= (Value ?Op ?Id ?X) ?X) ))))

```

## Relation REFLEXIVE

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Reflexive ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X)
(=> (Instance-Of ?X ?Domain) (Holds ?Rel ?X ?X)) )))

```

## Relation IRREFLEXIVE

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Irreflexive ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X)
(=> (Instance-Of ?X ?Domain)
(Not (Holds ?Rel ?X ?X)) ))))

```

## Relation SYMMETRIC

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Symmetric ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X ?Y)
(=> (And (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(Holds ?Rel ?X ?Y) )
(Holds ?Rel ?Y ?X) ))))

```

## Relation ASYMMETRIC

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Asymmetric ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X ?Y)
(=> (And (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(Holds ?Rel ?X ?Y) )
(Not (Holds ?Rel ?Y ?X)) ))))

```

## Relation ANTISYMMETRIC

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Antisymmetric ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X ?Y)
(=> (And (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(Holds ?Rel ?X ?Y)
(Holds ?Rel ?Y ?X) )
(= ?X ?Y) ))))

```

## Relation TRICHOTOMIZES

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Trichotomizes ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X ?Y)
(=> (And (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain) )
(Or (Holds ?Rel ?X ?Y)
(= ?X ?Y)
(Holds ?Rel ?Y ?X) )))))

```

## Relation TRANSITIVE

Arity: 2
Domain: Binary-relation
Axioms:
```(<=> (Transitive ?Rel ?Domain)
(And (Binary-Relation ?Rel)
(Forall (?X ?Y ?Z)
(=> (And (Instance-Of ?X ?Domain)
(Instance-Of ?Y ?Domain)
(Instance-Of ?Z ?Domain)
(Holds ?Rel ?X ?Y)
(Holds ?Rel ?Y ?Z) )
(Holds ?Rel ?X ?Z) ))))

```

## Relation SEMIGROUP

Arity: 3
Axioms:
```(<=> (Semigroup ?Domain ?Op ?Id)
(And (Binary-Operator-On ?Op ?Domain)
(Associative ?Op ?Domain)
(Identity-Element-For ?Id ?Op ?Domain) ))

```

## Relation ABELIAN-SEMIGROUP

Arity: 3
Subrelation-Of: Semigroup
Axioms:
```(<=> (Abelian-Semigroup ?Domain ?Op ?Id)
(And (Semigroup ?Domain ?Op ?Id) (Commutative ?Op ?Domain)) )

```

## Relation GROUP

Arity: 3
Axioms:
```(<=> (Group ?Domain ?Op ?Id)
(And (Binary-Operator-On ?Op ?Domain)
(Associative ?Op ?Domain)
(Identity-Element-For ?Id ?Op ?Domain)
(Invertible ?Op ?Id ?Domain) ))

```

## Relation ABELIAN-GROUP

Arity: 3
Subrelation-Of: Group
Axioms:
```(<=> (Abelian-Group ?Domain ?Op ?Id)
(And (Group ?Domain ?Op ?Id) (Commutative ?Op ?Domain)) )

```

## Relation RING

Arity: 5
Axioms:
```(<=> (Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id)
(Semigroup ?Domain ?Mult-Op ?One-Id)
(Distributes ?Mult-Op ?Plus-Op ?Domain) ))

```

## Relation COMMUTATIVE-RING

Arity: 5
Axioms:
```(<=> (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id)
(Abelian-Semigroup ?Domain ?Mult-Op ?One-Id)
(Distributes ?Mult-Op ?Plus-Op ?Domain) ))

```

## Relation INTEGRAL-DOMAIN

Arity: 5
Subrelation-Of: Commutative-ring
Axioms:
```(<=> (Integral-Domain ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Commutative-Ring ?Domain
?Plus-Op
?Zero-Id
?Mult-Op
?One-Id)
(Binary-Operator-On ?Mult-Op
(Kappa (?X)
(And (Instance-Of ?X ?Domain)
(/= ?X ?Zero-Id) )))))

```

## Relation DIVISION-RING

Arity: 5
Subrelation-Of: Ring
Axioms:
```(<=> (Division-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(Group (Kappa (?X)
(And (Instance-Of ?X ?Domain)
(/= ?X ?Zero-Id) ))
?Mult-Op
?One-Id)))

```

## Relation FIELD

Arity: 5
Subrelation-Of: Division-ring
Axioms:
```(<=> (Field ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(And (Division-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
(Commutative ?Plus-Op ?Domain) ))

```

## Relation PARTIAL-ORDER

Arity: 2
Axioms:
```(<=> (Partial-Order ?Domain ?Rel)
(And (Irreflexive ?Rel ?Domain)
(Asymmetric ?Rel ?Domain)
(Transitive ?Rel ?Domain) ))

```

## Relation LINEAR-ORDER

Arity: 2
Axioms:
```(<=> (Linear-Order ?Domain ?Rel)
(And (Irreflexive ?Rel ?Domain)
(Asymmetric ?Rel ?Domain)
(Transitive ?Rel ?Domain)
(Trichotomizes ?Rel ?Domain) ))

```

## Relation LINEAR-SPACE

Abstract linear or vector space of arbitrary dimension. Defines operations on vectors over a scalar field.
Arity: 7
Axioms:
```(Nth-Domain Linear-Space 2 Class)

(Nth-Domain Linear-Space 1 Class)

(<=> (Linear-Space ?Scalar-Domain
?Vector-Domain
?S-Zero
?S-One
?V-Zero
?Mult
(And (Class ?Scalar-Domain)
(Class ?Vector-Domain)
(Field ?Scalar-Domain ?Add ?S-Zero ?Mult ?S-One)
(Forall (?S ?V)
(=> (And (Instance-Of ?S ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain) )
(Instance-Of (Value ?Mult ?S ?V)
?Vector-Domain)))
(Forall (?S ?V1 ?V2)
(=> (And (Instance-Of ?S ?Scalar-Domain)
(Instance-Of ?V1 ?Vector-Domain)
(Instance-Of ?V2 ?Vector-Domain) )
(= (Value ?Mult ?S (Value ?Add ?V1 ?V2))
(Value ?Mult ?S ?V1)
(Value ?Mult ?S ?V2) ))))
(Forall (?S1 ?S2 ?V)
(=> (And (Instance-Of ?S1 ?Scalar-Domain)
(Instance-Of ?S2 ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain) )
(= (Value ?Mult (Value ?Add ?S1 ?S2) ?V)
(Value ?Mult ?S1 ?V)
(Value ?Mult ?S2 ?V) ))))
(Forall (?S1 ?S2 ?V)
(=> (And (Instance-Of ?S1 ?Scalar-Domain)
(Instance-Of ?S2 ?Scalar-Domain)
(Instance-Of ?V ?Vector-Domain) )
(= (Value ?Mult (Value ?Mult ?S1 ?S2) ?V)
(Value ?Mult ?S1 (Value ?Mult ?S2 ?V)) )))
(Forall (?V)
(=> (Instance-Of ?V ?Vector-Domain)
(And (= (Value ?Mult ?S-One ?V) ?V)
(= (Value ?Mult ?S-Zero ?V) ?V-Zero) )))))

```

This document was generated using Ontolingua.
Formatting and translation code was written by
François Gerbaux and Tom Gruber