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):
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