Tags : Browse Projects

Select a tag to browse associated projects and drill deeper into the tag cloud.

Coq proof assistant

Compare

  Analyzed about 11 hours ago

Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * to define functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to ... [More] check these proofs by a relatively small certification "kernel". [Less]

416K lines of code

87 current contributors

about 15 hours since last commit

18 users on Open Hub

Very High Activity
4.85714
   
I Use This

Skeptik

Compare

  Analyzed about 14 hours ago

Proof theory and automated deduction framework focused on proof compression techniques and implemented in Scala.

10.9K lines of code

0 current contributors

about 3 years since last commit

1 users on Open Hub

Inactive
5.0
 
I Use This

paradox

Compare

  Analyzed almost 5 years ago

Paradox is a finite-domain model finder for pure first-order logic with equality. Paradox is a MACE-style model finder, which means that it translates a first-order problem into a sequence of SAT problems, which are solved by a SAT solver (in our case MiniSat). Paradox is the proud winner of ... [More] the SAT/Models division of the CASC World Championship on First-Order Automated Theorem Proving in 2003, 2004, 2005 and 2006. [Less]

7.68K lines of code

0 current contributors

over 11 years since last commit

0 users on Open Hub

Activity Not Available
0.0
 
I Use This

C-CoRN

Compare

  Analyzed almost 5 years ago

The Constructive Coq Repository at Nijmegen, C-CoRN, aims at building a computer based library of constructive mathematics, formalized in the theorem prover Coq.

113K lines of code

0 current contributors

over 8 years since last commit

0 users on Open Hub

Activity Not Available
0.0
 
I Use This
Licenses: No declared licenses

BRILLANT

Compare

  Analyzed about 12 hours ago

B : research and software innovations with the help of new technologies. Free and open-source tools around the B Formal Method.

0 lines of code

0 current contributors

0 since last commit

0 users on Open Hub

Activity Not Available
0.0
 
I Use This
Mostly written in language not available
Licenses: No declared licenses