TPTP Standards for Questions and Answers

Questions

• Conjecture with outermost existentially quantified answer variables
• Given the role question
• E.g.,

  fof(pXY,question,   ? [X,Y] : p(X,Y)  ).

Short Answers

• SZS answers short list_of_definite_answer_tuples
• E.g.,

  SZS answers short for ANS001+1 [[a,b],[b,Z],[a,c]]

Long Answers

• SZS answers start for problem_file_name
  fof(some_name,answer,
      quantification_from_question
          disjunction_of_conjunctions_of_binding_equations & the_question,
      answer_to(name_of_question,[])).
  ...
  ...
  SZS answers end for problem_file_name
• E.g..,

  SZS answers start for ANS001+1
  fof(1,answer,
      ? [X,Y] :
        ( X = a & Y = b & p(X,Y) ),
      answer_to(pXY,[])).
  fof(2,answer,
      ? [X,Y] :
        ( X = b & Y = Z & p(X,Y) ),
      answer_to(pXY,[])).
  fof(3,answer,
      ? [X,Y] :
        ( X = a & Y = c & p(X,Y) ),
      answer_to(pXY,[])).
  SZS answers end for ANS001+1

• Intermediate forms possible