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:
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
Oyvind Tafjord, Bhavana Dalvi Mishra, Peter Clark