Implementation of theorem prover based on Skeptik's data structures and Conflict Resolution algorithm

<p>Skeptik[1] is a tool focused on compression of proofs, but it's also possible to generate proofs using it's infrastructure.</p> <p>There is a new algorithm developed by ANU employees, called Conflict Resolution algorithm[2], which has no implementation yet and can generate proofs in first-order logic.</p> <p>Conflict Resolution algorithm extends well­known SAT ­solver DPLL[3] and CDCL[4] algorithm and tries to generalize it’s ideas for first­-order logic. In CR we negate instances (substitutions) of decision literals (unlike CDCL where we negate decision literals), but main idea is the same: we decide to assign truthness to some atom and then try to propagate and achieve truthness of some other atoms. Eventually, we will reach a conflict or satisfactions and generate some conflict clauses if reached conflict.</p> <ul> <li>[1] <a href="https://github.com/Paradoxika/Skeptik" target="_blank">https://github.com/Paradoxika/Skeptik</a></li> <li>[2] <a href="http://arxiv.org/pdf/1602.04568v1.pdf" target="_blank">http://arxiv.org/pdf/1602.04568v1.pdf</a></li> <li>[3] <a href="https://en.wikipedia.org/wiki/DPLL_algorithm" target="_blank">https://en.wikipedia.org/wiki/DPLL_algorithm</a></li> <li>[4] <a href="https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning" target="_blank">https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning</a></li> </ul>