(define-theory web-notions (Localization Representation))
(in-theory 'web-notions)


(DEFINE-FUNCTION LAST-CHECKED (?A) :-> ?B :DEF
 (AND (TIME-VALUE ?A ?B) (DATE-VALUE-FILLER ?B)))
(DEFINE-RELATION LAST-DATE-OF-CHECKING-OF (?A ?B) :IFF-DEF
 (= (INVERSE LAST-CHECKED) LAST-DATE-OF-CHECKING-OF))
(DEFINE-RELATION WEB-ADDRESS (?A ?B) :IFF-DEF
 (= (INVERSE WEB-ADDRESS-OF) WEB-ADDRESS))
(DEFINE-RELATION WEB-ADDRESS-OF (?A ?B) :DEF
 (EXTRINSIC-STRUCTURING-RELATION ?A ?B) :AXIOM-CONSTRAINTS
 (AND (RANGE WEB-ADDRESS-OF OBJECT)
      (DOMAIN WEB-ADDRESS-OF URL)))
(DEFINE-RELATION WEB-REFERENCE (?A ?B) :IFF-DEF
 (= (INVERSE WEB-REFERENCE-OF) WEB-REFERENCE))
(DEFINE-RELATION WEB-REFERENCE-OF (?A ?B)
 "This is useful to talk of the content
of web material in a generic way."
 :DEF
 (AND (EXTRINSIC-STRUCTURING-RELATION ?A ?B)
      (EXISTS (?C) (AND (WEB-ADDRESS-OF ?A ?C) (INTERPRETANT-OF ?C ?B)))))
(DEFINE-CLASS FTP-URL (?SELF) "File transfer protocol url class."
 :DEF (URL ?SELF))
(DEFINE-CLASS HTTP-URL (?SELF)
 "Root class of hypertext transfer protocol urls." :DEF (URL ?SELF))
(DEFINE-CLASS NEWS-ARTICLE (?SELF)
:DEF (NEWS-URL ?SELF))
(DEFINE-CLASS NEWS-GROUP (?SELF)
:DEF (NEWS-URL ?SELF))
(DEFINE-CLASS NEWS-URL (?SELF)
:DEF (URL ?SELF))
(DEFINE-CLASS TELNET-URL (?SELF) "Telnet url class." :DEF
 (URL ?SELF))
(DEFINE-CLASS URI (?SELF)
 "Root class of Uniform Resource Identifiers." :DEF (SYMBOLIC-STRING ?SELF))
(DEFINE-CLASS URL (?SELF) "Root class of Uniform Resource Locators."
 :IFF-DEF
 (AND (URI ?SELF) (MINIMUM-SLOT-CARDINALITY ?SELF WEB-ADDRESS-OF 1)))
(DEFINE-CLASS WEB (?SELF)
:DEF
 (AND (REGION ?SELF)
      (VALUE-CARDINALITY ?SELF _ABSTRACT 1)
      (EXISTS (?A) (AND (STRICTLY-DEPENDS-ON ?SELF ?A) (SOFTWARE-PROGRAM ?A)))))
(DEFINE-CLASS WEB-SITE (?SELF)
:DEF
 (AND (REGION ?SELF)
      (VALUE-CARDINALITY ?SELF _ABSTRACT 1)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (WEB ?A)))))