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.

Student

itegulov

Mentors

  • Katya
  • Bruno Woltzenlogel Paleo
close

2016