;;Based on discussions with Jose Meseguer.

;;Descriptions of publications are modeled on that in Bibtex. There
;;are books, conference papers, journal articles, theses, etc.
  
;;  (declare-disjoint-subsorts 'publication
;;			     'series 'book 'article 'paper 'thesis)

;;Distinct from actual books are book references (of sort "bookq"), which
;;are descriptions of books.  Book references are a subsort of data, as
;;are titles, etc.:

;;  (declare-disjoint-subsorts 'data
;;   'title 'volume 'number 'edition 'note 'bookq)

;;A book reference is constructed by the function "bookq" (distinct from
;;the sort) declared as follows:


;;  (declare-function-symbol
;;   'bookq :plist
;;   :sort '(bookq
;;	   (author agent)
;;	   (editor agent)
;;	   (title title)
;;	   (publisher publisher)
;;	   (year year)
;;	   (volume volume)
;;	   (number number)
;;	   (series series)
;;	   (address address)
;;	   (edition edition)
;;	   (month month)
;;	   (note note)))

;;The plist is a SNARK structure that allows a property-list notation,
;;with alternating keys and values.  Some key and value pairs may be
;;omitted.  Arguments may occur in any order.  The first four are
;;required, but this is not yet adequately described by the notation.
;;(Meseguer has an approach to this.)

;;Not every book reference describes an actual book; it is easy to
;;concoct fictitious references.  Also, there may be different
;; references that describe the same book.  The relationship between
;; a book reference and an actual book is characterized by the relation
;;book-val:

;;  (declare-predicate-symbol
;;   'book-val 2
;;   :sort '((1 bookq)
;;	   (2 book)))


;;Every book has an author or editor, which can be an arbitrary agent.
;;Agents can be person, an organization, or a
;;list of these:

;;  (declare-subsorts 'agent
;;		    'person 'person-list 'organization 'organization-list)

;;A book has a publisher, which is a kind of organization:

;;  (declare-subsorts 'organization 'publisher)

;;A book has a title, which is obtained from a title-string.

;;  (declare-disjoint-subsorts 'data
;;          'title 'volume 'number 'edition 'note 'picture)

;;  (declare-subsorts 'string 'title-string 'publisher-name)
 
;;A title is not identical to a title string, but there is a function
;;that maps strings into titles: 

;;  (declare-function-symbol
;;   'titleq 1
;;   :sort '(title
;;	   (1 title-string)))

;;Other functions might map the same string into an author or a publisher,
;;in some cases; that is why we cannot identify the string with the
;;title, author, etc.


;;For example, 
;;   (titleq "William Shakespeare")
;;is a title, not an author.

;;There is a function bookq-to-title that maps a book reference into
;;the corresponding title.
  
;;  (declare-function-symbol
;;   'bookq-to-title 1
;;   :sort '(title
;;	   (1 bookq)))

;;Similarly, there is a function bookq-to-author that maps a
;;book reference into its author,

;;These are described by the following axioms:

;;  (assert
;;   '(=
;;     ?title
;;     (bookq-to-title
;;      (bookq title ?title . ?)))
;;   :name 'title-of-book)

;;  (assert
;;   '(=
;;     ?agent
;;     (bookq-to-author
;;      (bookq author ?agent . ?)))
;;   :name 'author-of-book)

;;In other words, the title of a book reference (bookq title ?title ...)
;;is ?title.  Similarly for the author.  The ? stands for "...", the
;;unspecified arguments of bookq.

;;The "names:" are for human consumption only; they have no logical
;;impact. They will appear in the trace, as you shall see.

;;We might state fact that the Latex Manual is described by a certain
;;reference by the axiom

;;  (assert
;;   '(book-val
;;     (bookq
;;      author (personq "Leslie Lamport")
;;      title (titleq "Latex: A Document Preparation System")
;;      year (year-fn 1986)
;;      publisher (publisherq "Addison-Wesley Publishing Company"))
;;     latex-manual
;;     )
;;   :name 'latex-manual-reference)

;;This might be the internal form of a marked up entry in a publication
;;list.  One might generate DamL from this and the other formulas in
;;this note.

;;Now, suppose we would like to find out who wrote the Latex manual.
;;Then we can formulate the query

;;  (prove '(and
;;	   (book-val ?bookq ?book)
;;	   (=
;;	    (bookq-to-title ?bookq)
;;	    (titleq "Latex: A Document Preparation System"))
;;	   (=
;;	    (bookq-to-author-or-editor ?bookq)
;;	    (personq ?person-name)))
;;	 :answer '(val ?person-name)
;;	 :name 'who-wrote-latex-manual)

;;In other words we want to find a book whose title is
;; "Latex: A Document Preparation System", and we want to know the
;;author of that book.  

;;The SNARK solution to this problem is

;;(Refutation
;; (Row author-of-book
;;      (= ?agent (bookq-to-author (bookq author ?agent . ?x)))
;;      assertion)
;; (Row title-of-book
;;      (= ?title (bookq-to-title (bookq title ?title . ?x)))
;;      assertion)
;; (Row latex-manual-reference
;;      (book-val
;;       (bookq author (personq "Leslie Lamport")
;;	      title
;;	       (titleq "Latex: A Document Preparation System")
;;	      year (year-fn 1986)
;;	      publisher (publisherq "Addison-Wesley Publishing Company"))
;;       latex-manual)
;;      assertion)
;; (Row who-wrote-latex-manual
;;      (or (not (book-val ?bookq ?book))
;;	  (not (= (bookq-to-title ?bookq)
;;		  (titleq "Latex: A Document Preparation System")))
;;	  (not (= (bookq-to-author ?bookq) (personq ?person-name))))
;;      ~conclusion
;;      Answer (val ?person-name))
;; (Row 134
;;      (not (= (personq "Leslie Lamport") (personq ?person-name)))
;;      (rewrite (resolve who-wrote-latex-manual
;;			latex-manual-reference)
;;	       title-of-book
;;	       :code-for-=
;;	       author-of-book)
;;      Answer (val ?person-name))
;; (Row 135
;;      false
;;      (resolve 134 :code-for-=)
;;      Answer (val "Leslie Lamport"))
;; )

;;  ;;; deriving "false" means that a contradiction has been
;;  ;;; successfully obtained.  The corresponding answer is
;;  ;;; Leslie Lamport.  

;;The theory that this is based on appears in
;;~waldinger/artifact/homepage.lisp

;;;; -*- Mode: Lisp; Syntax: Common-lisp; Package: SNARK -*-
;;; File: artifact/homepage.lisp
;;; loaded into artifact/theory.lisp


(in-package :SNARK)

(defun HOMEPAGE-SORTS ()
  
  (declare-subsorts 'entity 'publication)
  
  (declare-disjoint-subsorts 'publication
			     'series 'book 'article 'paper 'thesis)

  (declare-subsorts 'agent
		    'person 'person-list 'organization 'organization-list)

  (declare-subsorts 'organization 'publisher)

  (declare-disjoint-subsorts 'data 'title 'volume 'number 'edition 'note
			     'bookq 'picture)

  (declare-subsorts 'string 'title-string 'publisher-name )

  )

(defun HOMEPAGE-SYMBOLS ()

  (declare-constant-symbol 'latex-manual :sort 'book)

  (declare-constant-symbol "Latex: A Document Preparation System"
			   :sort 'title-string)

  (declare-constant-symbol 'addison-wesley :sort 'publisher)

  (declare-constant-symbol "Addison-Wesley Publishing Company"
 :sort 'publisher-name)

  (declare-constant-symbol "Leslie Lamport"
 :sort 'person-name)

  (declare-predicate-symbol
   'book-val 2
   :sort '((1 bookq)
	   (2 book))) 
 
  (declare-function-symbol
   'bookq :plist
   :sort '(bookq
	   (author agent)
	   (editor agent)
	   (title title)
	   (publisher publisher)
	   (year year)
	   (volume volume)
	   (number number)
	   (series series)
	   (address address)
	   (edition edition)
	   (month month)
	   (note note)

	   )
   )
  
  (declare-function-symbol
   'titleq 1
   :sort '(title
	   (1 title-string)))
  
  (declare-function-symbol
   'publisherq 1
   :sort '(publisher
	   (1 publisher-name)))
  
  (declare-function-symbol
   'volumeq 1
   :sort '(volume
	   (1 natural)))
  
  (declare-function-symbol
   'booknumberq 1
   :sort '(booknumber
	   (1 natural)))
  
  (declare-function-symbol
   'bookq-to-author 1
   :sort '(agent
	   (1 bookq)))
  
  (declare-function-symbol
   'bookq-to-editor 1
   :sort '(agent
	   (1 bookq)))
  
  (declare-function-symbol
   'bookq-to-title 1
   :sort '(title
	   (1 bookq)))

  
   )

(defun HOMEPAGE-ASSERTIONS ()

  (assert
   '(=
     ?agent
     (bookq-to-author
      (bookq author ?agent . ?)))
   :name 'author-of-book)
  
  (assert
   '(=
     ?agent
     (bookq-to-editor
      (bookq editor ?agent . ?)))
   :name 'editor-of-book)

  (assert
   '(=
     ?title
     (bookq-to-title
      (bookq title ?title . ?)))
   :name 'title-of-book)

  (assert
   '(book-val
     (bookq
      author (personq "Leslie Lamport")
      title (titleq "Latex: A Document Preparation System")
      year (year-fn 1986)
      publisher (publisherq "Addison-Wesley Publishing Company"))
     latex-manual)
   :name 'latex-manual-reference)
  )

;; test case

(defun BOOK-TEST ()
  (theory-setup)
  (theory-sorts)
  (theory-symbols)
  (theory-assertions)
  (prove '(and
	   (book-val ?bookq ?book)
	   (=
	    (bookq-to-title ?bookq)
	    (titleq "Latex: A Document Preparation System"))
	   (=
	    (bookq-to-author ?bookq)
	    (personq ?person-name)))
	 :answer '(val ?person-name)
	 :name 'who-wrote-latex-manual))