chakshugupta13 / propositional-logic-theorem-prover-using-resolution-refutation Goto Github PK

View Code? Open in Web Editor NEW

Propositional Logic Theorem Prover using Resolution-Refutation takes Knowledge Base (i.e., formulae) and Query as input and implement a refutation proof (by first converting the given formulae into CNF), and report the result (1 if the query holds, and 0 otherwise). Additionally, the program have an option to print the resolution steps used in the proof.

Python 100.00%

propositional-logic-theorem-prover-using-resolution-refutation's Introduction

Propositional Logic Theorem Prover using Resolution-Refutation

Method main in main.py is responsible for taking Knowledge Base (i.e., formulae) and Query as input and implement a refutation proof (by first converting the given formulae into CNF), and report the result (1 if the query holds, and 0 otherwise). Additionally, the program have an option to print the resolution steps used in the proof.

Input Format

First line contains two integer value 'n' the number of formulae and 'm' the mode.
Followed by the formulae (propositional sentences) in the next 'n' lines.
Last line would contain the propositional sentence that needs to be proved.
We will use the following characters for different operators/symbols:
- OR : |
- AND : &
- NOT : !
- IMPLIES : >
- IFF (bidirectional) : =
- OPENING BRACKET : (
- CLOSING BRACKET : )

Recommend Projects

chakshugupta13 / propositional-logic-theorem-prover-using-resolution-refutation Goto Github PK