Close #18

tools/sat-smt/agda.md

@@ -0,0 +1,18 @@
++++
+title = 'Agda 2'
+subtitle = ''
+links = [
+	{ title = "Homepage", url = "https://wiki.portal.chalmers.se/agda/pmwiki.php", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/agda/agda", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover","Specification Language"]
+developers = []
+licenses = ["MIT"]
+inputs = ["Agda"]
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+ Agda is a dependently typed programming language / interactive theorem prover. 

tools/sat-smt/chyp.md

@@ -0,0 +1,18 @@
++++
+title = 'Chyp'
+subtitle = 'Interactive Theroem Prover'
+links = [
+	{ title = "Homepage", url = "https://github.com/akissinger/chyp", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/akissinger/chyp", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["University of Oxford"]
+licenses = ["Apache-2.0"]
+inputs = ["Chyp"]
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+Chyp (pronounced "chip") is an interactive theorem prover for symmetric monoidal categories (SMCs), a.k.a. process theories.

tools/sat-smt/hilbert.md

@@ -0,0 +1,21 @@
++++
+title = 'Hilbert'
+subtitle = 'Interactive Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://github.com/liamoc/hilbert", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/liamoc/hilbert", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["ConsenSys"]
+licenses = ["Apache-2.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2014
+draft = false
+date = 2025-08-21
++++
+
+{{<inactive year="2014">}}
+
+Hilbert is a theorem prover designed for people who don't want to learn a theorem prover, specifically students studying formal treatments of programming languages.

tools/sat-smt/isabelle.md

@@ -0,0 +1,18 @@
++++
+title = 'Isabelle'
+subtitle = 'Interactive Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://isabelle.in.tum.de/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://isabelle-dev.sketis.net/source/isabelle", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["University of Cambridge","Technische Universitat Munchen"]
+licenses = ["BSD-2-Clause"]
+inputs = ["Isabelle"]
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.

tools/sat-smt/megalodon.md

@@ -0,0 +1,18 @@
++++
+title = 'Megalodon'
+subtitle = 'Interactive Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://github.com/ai4reason/Megalodon", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/ai4reason/Megalodon", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = []
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+Megalodon is an open source interactive theorem prover and proof checker.

tools/sat-smt/otter.md

@@ -0,0 +1,21 @@
++++
+title = 'Otter'
+subtitle = 'Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://www.cs.unm.edu/~mccune/otter/", icon = 'fa-solid fa-home' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = []
+inputs = []
+interfaces = []
+maintenance = ["Not Maintained"]
+updated_year = 2015
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive>}}
+
+ Otter/Mace2 are no longer being actively developed, and maintenance and support minimal.
+We recommend using Otter/Mace2's successor Prover9/Mace4 instead. 

tools/sat-smt/prover9.md

@@ -0,0 +1,17 @@
++++
+title = 'Prover9'
+subtitle = 'Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://www.cs.unm.edu/~mccune/prover9/", icon = 'fa-solid fa-home' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+ Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover. 

tools/sat-smt/pvs.md

@@ -0,0 +1,18 @@
++++
+title = 'PVS'
+subtitle = 'Interactive Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://pvs.csl.sri.com/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "github.com/SRI-CSL/PVS", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["SRI International"]
+licenses = ["GPL-2.0"]
+inputs = ["PVS"]
+interfaces = ["CLI","GUI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+PVS is a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas.

tools/sat-smt/setheo.md

@@ -0,0 +1,19 @@
++++
+title = 'SETHEO'
+subtitle = 'Theorem Prover'
+links = [	{ title = "Source Code", url = "https://github.com/theoremprover-museum/SETHEO", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2017
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2017">}}
+
+SETHEO is a theorem prover for first-order logic based on some variant of the connection method. 

tools/sat-smt/wytp.md

@@ -0,0 +1,18 @@
++++
+title = 'Whiley Theorem Prover'
+subtitle = 'Interactive Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://github.com/Whiley/WhileyTheoremProver", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/Whiley/WhileyTheoremProver", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["ConsenSys"]
+licenses = ["Apache-2.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+ The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.