lazyCoP 0.1

EasyChair Preprint 3926

Abstract

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

@booklet{EasyChair:3926,
  author    = {Michael Rawson and Giles Reger},
  title     = {lazyCoP 0.1},
  howpublished = {EasyChair Preprint 3926},
  year      = {EasyChair, 2020}}