Inference Using Resolution and First Order Logic.

1. Background

Developed a program that checks whether a given query holds True in a given Knowledge Base which consisted of sentences with operators : AND, OR ,NOT. Implemented using Resolution Refutation.

2. Format

• Each query is in the form of a single literal
• Variables are lower case
• Each predicate has at least one argument. A predicate takes at most 100 arguments.
• There will be at most 100 queries and 1000 sentences in Knowledge Base.

3. Example Input and Output

Input

Output

Check out the implementation here