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

Skeptik[1] is a tool focused on compression of proofs, but it's also possible to generate proofs using it's infrastructure.

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.

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.

• [1] https://github.com/Paradoxika/Skeptik
• [2] http://arxiv.org/pdf/1602.04568v1.pdf
• [3] https://en.wikipedia.org/wiki/DPLL_algorithm
• [4] https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning