Build Your Own First-Order Prover

These are the slides/examples/provers used in the tutorial.

Part 1: ATP, Proof Calculi and Prolog
Slides: prover_tutorial_CADE19_1.pdf
- Part 1a: ATP and Proof Calculi
- Part 1b: Prolog
  SWI-Prolog homepage
Part 2: Implementing a Sequent Prover
Slides: prover_tutorial_CADE19_2.pdf
- Part 2a: Implementing a Propositional Prover
  Examples: ex_diet1.pl, ex_diet2.pl
  Provers: leanseq_v0.pl, leanseq_v1.pl, leanseq_v2.pl
  Examples: ex_invalid.pl, ex_pigeon3.pl, ex_pigeon4.pl
- Part 2b: Implementing a First-Order Prover
  Example: ex_barber.pl
  Provers: leanseq_v3.pl, leanseq_v4.pl, leanseq_v5.pl
  Examples: ex_quant.pl, ex_f12.pl, ex_f20.pl
Part 3: Tableau and Connection Provers
Slides: prover_tutorial_CADE19_3.pdf
- Part 3a: A Tableau Prover
  Prover: leantap_pure.pl, nnf_pure.pl, unify.pl
  leanTAP homepage
- Part 3b: A Connection Prover
  Prover: leancop_pure.pl, nnf_mm.pl, unify.pl
  leanCoP homepage

Please contact me, if you have questions or need help when implementing a prover based on the presented techniques.

Jens Otten