From 2c1587a00623650e13c2a7dcf9dddfa95910c9a5 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Thu, 21 Aug 2025 18:02:34 -0600 Subject: [PATCH] Close #18 --- new-tool.md | 4 +++- tools/sat-smt/agda.md | 18 ++++++++++++++++++ tools/sat-smt/chyp.md | 18 ++++++++++++++++++ tools/sat-smt/hilbert.md | 21 +++++++++++++++++++++ tools/sat-smt/isabelle.md | 18 ++++++++++++++++++ tools/sat-smt/megalodon.md | 18 ++++++++++++++++++ tools/sat-smt/otter.md | 21 +++++++++++++++++++++ tools/sat-smt/prover9.md | 17 +++++++++++++++++ tools/sat-smt/pvs.md | 18 ++++++++++++++++++ tools/sat-smt/setheo.md | 19 +++++++++++++++++++ tools/sat-smt/wytp.md | 18 ++++++++++++++++++ 11 files changed, 189 insertions(+), 1 deletion(-) create mode 100644 tools/sat-smt/agda.md create mode 100644 tools/sat-smt/chyp.md create mode 100644 tools/sat-smt/hilbert.md create mode 100644 tools/sat-smt/isabelle.md create mode 100644 tools/sat-smt/megalodon.md create mode 100644 tools/sat-smt/otter.md create mode 100644 tools/sat-smt/prover9.md create mode 100644 tools/sat-smt/pvs.md create mode 100644 tools/sat-smt/setheo.md create mode 100644 tools/sat-smt/wytp.md diff --git a/new-tool.md b/new-tool.md index 77687a9..ec5c36b 100644 --- a/new-tool.md +++ b/new-tool.md @@ -37,11 +37,12 @@ function generateMarkdown() { const currentYear = new Date().getFullYear(); let maintenance = "Actively Maintained"; let maintenance_year = ""; + let description = document.getElementById('description').value; if (updatedYear && currentYear - updatedYear > 5) { maintenance = "Not Maintained"; maintenance_year = `updated_year = ${updatedYear}\n`; + description = `\{\{\}\}\n\n` + description } - const description = document.getElementById('description').value; let md = `+++ title = '${title}' subtitle = '${subtitle}' @@ -55,6 +56,7 @@ maintenance = [${JSON.stringify(maintenance)}] ${maintenance_year}draft = false date = ${date} +++\n\n`; + md += description; document.getElementById('output').textContent = md; } diff --git a/tools/sat-smt/agda.md b/tools/sat-smt/agda.md new file mode 100644 index 0000000..32c3ba6 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/sat-smt/chyp.md b/tools/sat-smt/chyp.md new file mode 100644 index 0000000..b5877a6 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/sat-smt/hilbert.md b/tools/sat-smt/hilbert.md new file mode 100644 index 0000000..254c025 --- /dev/null +++ b/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 ++++ + +{{}} + +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. \ No newline at end of file diff --git a/tools/sat-smt/isabelle.md b/tools/sat-smt/isabelle.md new file mode 100644 index 0000000..faa4049 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/sat-smt/megalodon.md b/tools/sat-smt/megalodon.md new file mode 100644 index 0000000..2eeaa94 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/sat-smt/otter.md b/tools/sat-smt/otter.md new file mode 100644 index 0000000..882c222 --- /dev/null +++ b/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 ++++ + +{{}} + + Otter/Mace2 are no longer being actively developed, and maintenance and support minimal. +We recommend using Otter/Mace2's successor Prover9/Mace4 instead. \ No newline at end of file diff --git a/tools/sat-smt/prover9.md b/tools/sat-smt/prover9.md new file mode 100644 index 0000000..315b80c --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/sat-smt/pvs.md b/tools/sat-smt/pvs.md new file mode 100644 index 0000000..1e10b2c --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tools/sat-smt/setheo.md b/tools/sat-smt/setheo.md new file mode 100644 index 0000000..1cde6c4 --- /dev/null +++ b/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 ++++ + +{{}} + +SETHEO is a theorem prover for first-order logic based on some variant of the connection method. \ No newline at end of file diff --git a/tools/sat-smt/wytp.md b/tools/sat-smt/wytp.md new file mode 100644 index 0000000..b215ec3 --- /dev/null +++ b/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. \ No newline at end of file