The Automated Theorem Proving System CARINE

   CARINE is a first-order automated theorem prover designed and implemented by Paul Haroun as an experimental system for the study of the impact of delayed clause-construction and attribute sequences on the performance of  first-order resolution-refutation theorem provers that perform extensive linear derivations.

   CARINE is the application of the theory from the Ph.D. thesis of the author. The first working version of the program is version 0.72. It was submitted to the CADE-19 competition CASC-19. CARINE can be tested online at Systems on TPTP.

This site is still under construction. Thank you for your patience and for your interest in the ATP CARINE.