First-order Logic: Theory and Practice

FU Berlin (WS 2012/2013)

• The DPLL Calculus: atp_fub12_1dpll.pdf

• The Tableau Calculus: atp_fub12_2tap.pdf

• The Connection Calculus: atp_fub12_3cop.pdf

The following provers are written in Prolog. Popular Prolog systems are, e.g., ECLiPSe Prolog, SWI-Prolog or SICStus Prolog. SWI-Prolog is the most user-friendly system.

• leanDPLL: leandpll.pl (for testing: test_dpll.pl)

• leanTAP: leantap.pl, nnf.pl, unify.pl (for testing: test_tap.pl)

• leanCoP: see www.leancop.de