Prove or disprove the given query based on the knowledge base

Decide the given statement is True or False depending on the given knowledge base, restricted to "For All" Statements. The Algorithm converts the given knowledge base into Resolution tree, and using the proof of restitution, we decide if the given statement is true or false.

A tool for automatically verifying whether a given first-order logic formula is a tautology, based on Herbrand's theory and the Davis-Putnam SAT solver. Implemented in C++.

Резолюционный прувер для логики первого порядка

C++ implementations of fundamental algorithms taught on the course. Topics from first order logic and problem specification to time complexity. Algorithms for search and sorting, along with a testing module to verify correctness and efficiency.