Interfaces to External Sources

External Specifications

• fof(creators,external,
      ! [Thing] : ? [Name] : 
        s__creatorOf(Name,Thing),
      external(exec,'DBServer CreatorDB',tptp_qa,
        [xdb(limit,number(1000)),xdb(limit,cpu(4))]) ).

• Points to note
  • external role
  • Formula body as a template
  • Universal (!) and existential (?) quantification
  • external() term to specify manifestation
    • tptp_qa protocol
    • xdb() terms to provide auxilliary information
  • A problem file can contain multiple specifications

Requests for External Axioms

• fof(who,question,
      ? [Name] : 
        s__creatorOf(Name,s__YAGOOntology),
      spass,
      [xdb(limit,number(1000)),xdb(limit,cpu(4))] ).

• Points to note
  • question role, from TPTP Q&A standards
  • xdb() terms copied from specification

Delivery of External Axioms

• % SZS status Success for spass
  % SZS answers start InstantiatedFormulae for spass
  fof(creators,answer,
      s__creatorOf(s__FabianMartinSuchanek,s__YAGOOntology),
      answer_to(who,[]),[]).
  fof(creators,answer,
      s__creatorOf(s__GjergjiKasneci,s__YAGOOntology),
      answer_to(who,[]),[]).
  % SZS answers end InstantiatedFormulae for spass

• Points to note
  • SZS ontology values and standards
  • answer role, from TPTP Q&A standards
  • "Useful info" fields for passing back auxilliary information