Technische Universität
             Darmstadt nanoCoP Logo University of Oslo

Non-clausal Connection-Based Theorem Proving

  What is leanCoP?  
What is nanoCoP-M?

nanoCoP-M is a compact automated theorem prover for modal first-order logic. It is based on the non-clausal connection calculus for modal logic and extends the classical nanoCoP prover. More details about the calculus can be found in the documentation.

Features of nanoCoP-M

  • Theorem prover for modal first-order logic.
  • Supports the modal logics D, T, S4, and S5.
  • Supports constant, cumulative, and varying domains.
  • Based on the modal non-clausal connection calculus.
  • Proof search on the original formula structure.
  • Implemented in Prolog.
  • Sound and complete.
  • Leading performance.
  • Simple input format (nanoCoP-M or QMLTP syntax).
  • Output of compact modal non-clausal connection proof.


nanoCoP-M is optimized for the open source Prolog system ECLiPSe. It should run on other Prolog systems as well. The following package includes a ReadMe file containing more information.

Jens Otten · Institutt for informatikk · University of Oslo · 05.05.2017