;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*- 

;;; definitions that are general enough to be part of KIF. 

(in-package "ONTOLINGUA-USER") 

(in-theory 'kif-relations) 

(define-function REDUCTION (?oper ?func ?start-int ?end-int) :-> ?s 
  "REDUCTION is a way to map a binary operator over a sequence. 
The operator is applied to the first two items in the sequence, 
then it is applied to the result and the third item in the sequence, 
and so forth, until the end of the sequence is reached." 
  :iff-def (and (total-on ?oper (exact-range ?func)) 
		(unary-function ?func) 
		(domain ?func integer) 
		(integer ?start-int) 
		(integer ?end-int) 
		(=< ?start-int ?end-int) 
		(=> (= ?start-int ?end-int) 
		    (= ?s (value ?func ?start-int))) 
		(=> (< ?start-int ?end-int) 
		    (= ?s (value ?oper 
				 (value ?func ?start-int) 
				 (reduction ?oper  
					    ?func  
					    (1+ ?start-int) 
					    ?end-int)))))) 

(define-function SUMMATION (?func ?start ?end) :-> ?q 

  "Summation operator for a function that represents an integer 
indexed quantity." 

  :iff-def (and (unary-function ?func) 
		(domain ?func integer) 
		(integer ?start) 
		(integer ?end) 
		(=< ?start ?end) 
		(= ?q (reduction + ?func ?start ?end)))) 

(in-theory 'kif-numbers) 

(define-instance PI (real-number) 
  "PI is an approximation of the number PI, which is the ratio 
of the perimeter of a circle to its diameter." 
  := 3.1415926535897936) 

(in-theory 'kif-meta) 

(define-function ANTECEDENT (?implication) 
  "the antecedent sentence of a KIF implication." 
  :lambda-body (cond ((and (implication ?implication) 
                           (triple ?implication)) 
                      (first (rest ?implication))) 
                     ((implication ?implication) 
                      (cons 'AND (butlast (rest ?implication)))))) 

(define-function CONSEQUENT (?implication) 
  "the consequent sentence of a KIF implication." 
  :lambda-body (if (implication ?implication) 
                   (last ?implication))) 

(define-function RELSENT.RELCONST (?relation-sentence) 
  "extracts the relation constant from a relational sentence." 
  :lambda-body (if (relsent ?implication) 
                   (first ?implication)))