ProofWriter

The ProofWriter dataset contains many small rulebases of facts and rules, expressed in English. Each rulebase also has a set of questions (English statements) which can either be proven true or false using proofs of various depths, or the answer is “Unknown” (in open-world setting, OWA) or assumed negative (in closed-world setting, CWA).

The dataset includes full proofs with intermediate conclusions, which models can try to reproduce.

The dataset supports various tasks:

• Given rulebase + question, what is answer + proof (w/intermediates)?
• Given rulebase, what are all the provable implications?
• Given rulebase + question without proof, what single fact can be added to make the question true?

Here is a simple example from the depth-2 dataset D2(OWA):

Rulebase:

triple1: The cow is big.  
triple2: The cow needs the dog.  
triple3: The dog sees the rabbit.  
triple4: The rabbit chases the cow.  
triple5: The rabbit chases the dog.  
triple6: The rabbit is big.  
triple7: The rabbit sees the dog.  
rule1: If the cow is blue and the cow needs the rabbit then the cow needs the dog.
rule2: If the cow chases the dog then the cow sees the rabbit.
rule3: If something is big then it chases the dog.

Question with answer + proof:

Question: The cow sees the rabbit?
Answer: true
Proof: (((triple1) -> (rule3 % int2))) -> (rule2 % int1) ; with int1 = The cow sees the rabbit. ; int2 = The cow chases the dog.

Generate all implications (only 2 in this case, can be as high as 21 in D5 theories):

All implications: The cow chases the dog. The cow sees the rabbit.

Use abduction to find a missing fact which will make something true:

Question to make true: The dog chases the dog.
Missing fact: The dog is big.   (denoted tripleM)
Proof: (tripleM) -> rule3