Download PDFOpen PDF in browser

lazyCoP 0.1

EasyChair Preprint no. 3926

7 pagesDate: July 22, 2020


We describe lazyCoP, a fully-automatic theorem prover for first-order logic with equality. The system implements a connection-tableau calculus with a specific variant of ordered paramodulation inference rules, rather than the usual preprocessing approaches. We explore practical aspects and refinements of this calculus. The system also implements fully-parallel proof search and support for the integration of learned search heuristics.

Keyphrases: connection calculus, parallelism, paramodulation

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Michael Rawson and Giles Reger},
  title = {lazyCoP 0.1},
  howpublished = {EasyChair Preprint no. 3926},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browser