ProofWriter

Click “Download” for the dataset or “View Website” to try the live demo!

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. See the README for more details.

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