;;; -*- Mode:Lisp; Syntax: Common-lisp; Package:ONTOLINGUA-USER; Base:10 -*-
;;; Abstract algebra ontology.
;;; Defines the basic vocabulary for describing algebraic operators, domains,
;;; and structures such as fields, rings, and groups.
;;; Based on the example given as an appendix to the KIF3.0 manual.
;;; Modified to work over classes instead of sets, to be consistent
;;; with the frame ontology.
;;; --- Change history ---
;;; Original: August 1992 by Genesereth in KIF 3.0 spec
;;; 10/6/92 Gruber: converted to classes, fixed bugs, minor renaming
;;; 12/1/92 Gruber & Olsen: added identity-element-for and linear-space
;;; 6/30/93 Gruber: removed constraint on binary relations that precluded
;;; polymorphism. Now functions and relations can be
;;; "defined" as algebraic operators over multiple domains.
(in-package "ONTOLINGUA-USER")
(define-theory ABSTRACT-ALGEBRA (frame-ontology)
"Defines the basic vocabulary for describing algebraic operators, domains,
and structures such as fields, rings, and groups."
:issues ("Originally based on the example given as an appendix
to the KIF3.0 manual. Modified to work over classes instead of sets,
to be consistent with the frame-ontology."))
(in-theory 'abstract-algebra)
(define-relation BINARY-OPERATOR-ON (?function ?domain)
"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."
:iff-def
(and (binary-function ?function)
(forall (?x ?y)
(=> (and (instance-of ?x ?domain)
(instance-of ?y ?domain))
(instance-of (value ?function ?x ?y) ?domain)))))
(define-relation ASSOCIATIVE (?op ?domain)
:iff-def
(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)))))
(define-relation COMMUTATIVE (?op ?domain)
:iff-def
(forall (?x ?y)
(=> (instance-of ?x ?domain) (instance-of ?y ?domain)
(= (value ?op ?x ?y) (value ?op ?y ?x)))))
(define-relation INVERTIBLE (?op ?id ?domain)
:iff-def
(forall (?x)
(=> (instance-of ?x ?domain)
(exists (?y)
(and (instance-of ?y ?domain)
(= (value ?op ?x ?y) ?id) (= (value ?op ?y ?x) ?id))))))
(define-relation DISTRIBUTES (?op ?g ?domain)
:iff-def
(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)))))))
(define-relation IDENTITY-ELEMENT-FOR (?id ?op ?domain)
"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."
:iff-def
(and (instance-of ?id ?domain)
(binary-operator-on ?op ?domain)
(forall ?x
(=> (instance-of ?x ?domain)
(= (value ?op ?id ?x) ?x)))))
;;; properties of Binary Relations
(define-relation REFLEXIVE (?rel ?domain)
:iff-def
(and (binary-relation ?rel)
(forall ?x
(=> (instance-of ?x ?domain)
(holds ?rel ?x ?x)))))
(define-relation IRREFLEXIVE (?rel ?domain)
:iff-def
(and (binary-relation ?rel)
(forall (?x)
(=> (instance-of ?x ?domain)
(not (holds ?rel ?x ?x))))))
(define-relation SYMMETRIC (?rel ?domain)
:iff-def
(and (binary-relation ?rel)
(forall (?x ?y)
(=> (and (instance-of ?x ?domain)
(instance-of ?y ?domain)
(holds ?rel ?x ?y))
(holds ?rel ?y ?x)))))
(define-relation ASYMMETRIC (?rel ?domain)
:iff-def
(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))))))
(define-relation ANTISYMMETRIC (?rel ?domain)
:iff-def
(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)))))
(define-relation TRICHOTOMIZES (?rel ?domain)
:iff-def
(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))))))
(define-relation TRANSITIVE (?rel ?domain)
:iff-def
(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)))))
;;; Algebraic Structures
(define-relation SEMIGROUP (?domain ?op ?id)
:iff-def
(and (binary-operator-on ?op ?domain)
(associative ?op ?domain)
(identity-element-for ?id ?op ?domain)))
(define-relation ABELIAN-SEMIGROUP (?domain ?op ?id)
:iff-def
(and (semigroup ?domain ?op ?id)
(commutative ?op ?domain)))
(define-relation GROUP (?domain ?op ?id)
:iff-def
(and (binary-operator-on ?op ?domain)
(associative ?op ?domain)
(identity-element-for ?id ?op ?domain)
(invertible ?op ?id ?domain)))
(define-relation ABELIAN-GROUP (?domain ?op ?id)
:iff-def
(and (group ?domain ?op ?id)
(commutative ?op ?domain)))
(define-relation RING (?domain ?plus-op ?zero-id ?mult-op ?one-id)
:iff-def
(and (abelian-group ?domain ?plus-op ?zero-id)
(semigroup ?domain ?mult-op ?one-id)
(distributes ?mult-op ?plus-op ?domain)))
(define-relation COMMUTATIVE-RING (?domain ?plus-op ?zero-id ?mult-op ?one-id)
:iff-def
(and (abelian-group ?domain ?plus-op ?zero-id)
(abelian-semigroup ?domain ?mult-op ?one-id)
(distributes ?mult-op ?plus-op ?domain)))
(define-relation INTEGRAL-DOMAIN (?domain ?plus-op ?zero-id ?mult-op ?one-id)
:iff-def
(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))))))
(define-relation DIVISION-RING (?domain ?plus-op ?zero-id ?mult-op ?one-id)
:iff-def
(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)))
(define-relation FIELD (?domain ?plus-op ?zero-id ?mult-op ?one-id)
:iff-def
(and (division-ring ?domain ?plus-op ?zero-id ?mult-op ?one-id)
(commutative ?plus-op ?domain)))
(define-relation PARTIAL-ORDER (?domain ?rel)
:iff-def
(and (irreflexive ?rel ?domain)
(asymmetric ?rel ?domain)
(transitive ?rel ?domain)))
(define-relation LINEAR-ORDER (?domain ?rel)
:iff-def
(and (irreflexive ?rel ?domain)
(asymmetric ?rel ?domain)
(transitive ?rel ?domain)
(trichotomizes ?rel ?domain)))
(define-relation LINEAR-SPACE (?scalar-domain ?vector-domain ?s-zero ?s-one ?v-zero ?mult ?add)
"Abstract linear or vector space of arbitrary dimension. Defines operations
on vectors over a scalar field."
:iff-def
(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))))))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber