Theory ABSTRACT-ALGEBRA

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

Source code: abstract-algebra.lisp
List of other known theories

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

25 relations defined:

Abelian-Group
Abelian-Semigroup
Antisymmetric
Associative
Asymmetric
Binary-Operator-On
Commutative
Commutative-Ring
Distributes
Division-Ring
Field
Group
Identity-Element-For
Integral-Domain
Invertible
Irreflexive
Linear-Order
Linear-Space
Partial-Order
Reflexive
Ring
Semigroup
Symmetric
Transitive
Trichotomizes

No functions defined.

No instances defined.

The following constants were used from included theories:

Arity defined as a function in theory Frame-Ontology
Binary-Function defined as a class in theory Kif-Relations
Binary-Relation defined as a class in theory Kif-Relations
Binary-Relation defined as a class in theory Frame-Ontology
Class defined as a class in theory Frame-Ontology
Documentation defined as a relation in theory Frame-Ontology
Domain defined as a relation in theory Frame-Ontology
Holds defined as a relation in theory Kif-Relations
Instance-Of defined as a relation in theory Frame-Ontology
Nth-Domain defined as a relation in theory Frame-Ontology
Relation defined as a class in theory Kif-Relations
Relation defined as a class in theory Frame-Ontology
Subrelation-Of defined as a relation in theory Frame-Ontology
Value defined as a function in theory Kif-Relations

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

Relation SEMIGROUP

Arity: 3

Axioms:

(<=> (Semigroup ?Domain ?Op ?Id) 
     (And (Binary-Operator-On ?Op ?Domain) 
          (Associative ?Op ?Domain) 
          (Identity-Element-For ?Id ?Op ?Domain) ))

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

Relation ABELIAN-SEMIGROUP

Arity: 3
Subrelation-Of: Semigroup

Axioms:

(<=> (Abelian-Semigroup ?Domain ?Op ?Id) 
     (And (Semigroup ?Domain ?Op ?Id) (Commutative ?Op ?Domain)) )

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

Relation ABELIAN-GROUP

Arity: 3
Subrelation-Of: Group

Axioms:

(<=> (Abelian-Group ?Domain ?Op ?Id) 
     (And (Group ?Domain ?Op ?Id) (Commutative ?Op ?Domain)) )

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

Relation PARTIAL-ORDER

Arity: 2

Axioms:

(<=> (Partial-Order ?Domain ?Rel) 
     (And (Irreflexive ?Rel ?Domain) 
          (Asymmetric ?Rel ?Domain) 
          (Transitive ?Rel ?Domain) ))

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

Relation LINEAR-ORDER

Arity: 2

Axioms:

(<=> (Linear-Order ?Domain ?Rel) 
     (And (Irreflexive ?Rel ?Domain) 
          (Asymmetric ?Rel ?Domain) 
          (Transitive ?Rel ?Domain) 
          (Trichotomizes ?Rel ?Domain) ))

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

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
                   ?Add)
     (And (Class ?Scalar-Domain) 
          (Class ?Vector-Domain) 
          (Field ?Scalar-Domain ?Add ?S-Zero ?Mult ?S-One) 
          (Abelian-Group ?Vector-Domain ?Add ?V-Zero) 
          (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 ?Add
                                (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 ?Add
                                (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) )))))

Defined in theory: Abstract-algebra
Source code: abstract-algebra.lisp

This document was generated using Ontolingua.
Formatting and translation code was written by

François Gerbaux and Tom Gruber