Search Results for "theorem prover"
Sort By:
Showing 21 open source projects for "theorem prover"
View related business solutions-
The All-in-One Commerce Platform for Businesses - ShopifyShopify is a leading all-in-one commerce platform that enables businesses to start, build, and grow their online and physical stores. It offers tools to create customized websites, manage inventory, process payments, and sell across multiple channels including online, in-person, wholesale, and global markets. The platform includes integrated marketing tools, analytics, and customer engagement features to help merchants reach and retain customers. Shopify supports thousands of third-party apps and offers developer-friendly APIs for custom solutions. With world-class checkout technology, Shopify powers over 150 million high-intent shoppers worldwide. Its reliable, scalable infrastructure ensures fast performance and seamless operations at any business size.
-
Gen AI apps are built with MongoDB AtlasMongoDB Atlas is the developer-friendly database used to build, scale, and run gen AI and LLM-powered apps—without needing a separate vector database. Atlas offers built-in vector search, global availability across 115+ regions, and flexible document modeling. Start building AI apps faster, all in one place.
-
1
DeepSeek Prover V2
Advancing Formal Mathematical Reasoning via Reinforcement Learning
DeepSeek-Prover-V2 is DeepSeek’s specialized model for formal theorem proving, particularly targeting proof in Lean 4. The repository describes how they use recursive proof decomposition by prompting DeepSeek-V3 to break complex theorems into subgoals, synthesize proof sketches, and then combine them to bootstrap training data. They then fine-tune via reinforcement learning with binary correct/incorrect feedback to integrate informal reasoning with formal proof behavior. The repo releases two... -
2
Agda
Agda is a dependently typed programming language
Agda is a dependently typed, total functional programming language and interactive theorem prover based on Martin-Löf’s type theory. It allows expressing programs and proofs in the same language, using the Curry–Howard correspondence. It features interactive development via Emacs, Atom, or VS Code. Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has... -
3
Archive of Formal Proofs
A collection of machine-checkend mathematical proofs
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientifc developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal. Submissions are refereed. -
4
CTL-RP
CTL-RP is a theorem prover for Computation Tree Logic (CTL)
CTL-RP stands for Computation Tree Logic Resolution Prover. Computation Tree Logic (CTL) is a branching-time temporal logic. CTL-RP is a resolution based theorem prover for CTL, which utilises a first-order theorem prover, SPASS, as a core engine for inference. Please see the following link for more details. http://cueb.science/web/software/ (if you are inside China.) http://ctlrp.sourceforge.net (if you are not inside China.) -
Level Up Your Cyber Defense with External Threat ManagementMove beyond alerts. Gain full visibility, context, and control over your external attack surface to stay ahead of every threat.
-
5
-
6
IsaPlanner is a collection of reasoning tools: a proof planner for Isabelle, implementing a Rippling based inductive theorem prover; theory synthesis tools for Isabelle; an open-graph based tool for reasoning about quantum information (quantomatic);
-
7
metarec
algorithmic rule systems for Isabelle
The animation of algorithmic rule systems based on the Isabelle theorem prover. -
8
-
9
-
Simple, Secure Domain RegistrationRegister or renew your domain and pay only what we pay. No markups, hidden fees, or surprise add-ons. Choose from over 400 TLDs (.com, .ai, .dev). Every domain is integrated with Cloudflare's industry-leading DNS, CDN, and free SSL to make your site faster and more secure. Simple, secure, at-cost domain registration.
-
10
This page contains tools for applying automated reasoning to Bluespec SystemVerilog (BSV) hardware designs. We provide code for importing BSV designs into the PVS theorem prover and the SAL model checker.
-
11
-
12
An ML-based automated theorem prover for propositional logic making use of an algorithm in the intercalation calculus.
-
13
The Eagle automated theorem prover is a system for developing proofs for theorems in predicate logic.
-
14
Automated Theorem Prover implemented in Java and using clause trees. This software will be able to read mathematical theorems from TPTP and prove or disprove them.
-
15
-
16
-
17
This project will develop a graphical front-end environment using Java for a First Order Logic theorem prover called Otter. Otter is a free scientific tool that is open source, written in C, and command line only. It will support Linux, OSX, and Win
-
18
Spassgui is a Perl/Tk based Gui for SPASS (An Automated Theorem Prover for First-Order Logic with Equality) by http://spass.mpi-sb.mpg.de .
-
19
ManTa is an equational specification language and tools to support it: theorem prover, code generators (C and Ocaml), frontends.
-
20
A beginners' level theorem prover project for logic students. Okitsune is written in Haskell and open for contributions.
-
21
Kammerjäger
Kammerjäger is a debugging tool with integrated correctness proving.
Kammerjäger is a debugging and testing tool that enables you to prove the correctness of your code. In our C like programming language named "SimPL" you can easily and simply annotate your code with preconditions and assertions (also with forall and exists expressions). We then use Microsofts Z3 theorem prover to prove if the behaviour of your program matches what you expected. The easy to use GUI with an integrated Interpreter and Debugger (with a Stackview and HotCodeReplacement) makes...
- Previous
- You're on page 1
- Next
