This repository contains a resolution-based propositional logic reasoner, consisting of:
- a converter of logical sentences from ropositional logic into CNF (Causal Normal Form);
- a theorem prover for propositional logicm based on the resolution principle.
This work was developed by João Louro and Emanuel Fernandes as a project for the Artificial Intelligence and Decision Systems course at Instituto Superior Técnico.
More detailed documentaion can be found at doc/report.pdf.