From 97a87a16796b033deaf8513aed239d5151fd8ffc Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Thu, 21 Aug 2025 16:14:46 -0600 Subject: [PATCH] Close #17, add tools --- new-tool.md | 12 ++++++++++++ tools/sat-smt/abella.md | 22 ++++++++++++++++++++++ tools/sat-smt/beagle.md | 22 ++++++++++++++++++++++ tools/sat-smt/gappa.md | 22 ++++++++++++++++++++++ tools/sat-smt/metis.md | 22 ++++++++++++++++++++++ tools/sat-smt/metitarski.md | 22 ++++++++++++++++++++++ tools/sat-smt/princess.md | 22 ++++++++++++++++++++++ tools/sat-smt/profound.md | 22 ++++++++++++++++++++++ tools/sat-smt/spass.md | 23 +++++++++++++++++++++++ 9 files changed, 189 insertions(+) create mode 100644 new-tool.md create mode 100644 tools/sat-smt/abella.md create mode 100644 tools/sat-smt/beagle.md create mode 100644 tools/sat-smt/gappa.md create mode 100644 tools/sat-smt/metis.md create mode 100644 tools/sat-smt/metitarski.md create mode 100644 tools/sat-smt/princess.md create mode 100644 tools/sat-smt/profound.md create mode 100644 tools/sat-smt/spass.md diff --git a/new-tool.md b/new-tool.md new file mode 100644 index 0000000..e95f5eb --- /dev/null +++ b/new-tool.md @@ -0,0 +1,12 @@ ++++ +title = 'Contribute' +date = 2025-06-07 ++++ + +This page is useful to generate copy-and-paste source code in Markdown for a new tool. + +## Quick Links + +- Request addding a tool: [Submit Git Issue](https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2fadd_tool.md) +- Request fixing a tool: [Submit Git Issue](https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md) + diff --git a/tools/sat-smt/abella.md b/tools/sat-smt/abella.md new file mode 100644 index 0000000..2bad9ed --- /dev/null +++ b/tools/sat-smt/abella.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Abella' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://abella-prover.org/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "github.com/abella-prover/abella", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Inria'] +licenses = ['GPLv3'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + + +Abella is an interactive theorem prover based on lambda-tree syntax. \ No newline at end of file diff --git a/tools/sat-smt/beagle.md b/tools/sat-smt/beagle.md new file mode 100644 index 0000000..89f21d5 --- /dev/null +++ b/tools/sat-smt/beagle.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'BEAGLE' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://bitbucket.org/peba123/beagle/src/master/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://bitbucket.org/peba123/beagle/src/master/", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['CSIRO'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + + +Beagle is an automated theorem prover for first-order logic with equality over linear integer/rational/real arithmetic. \ No newline at end of file diff --git a/tools/sat-smt/gappa.md b/tools/sat-smt/gappa.md new file mode 100644 index 0000000..09da80d --- /dev/null +++ b/tools/sat-smt/gappa.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Gappa' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://gappa.gitlabpages.inria.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://gitlab.inria.fr/gappa/gappa", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Inria'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3', 'Coq'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + + +Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. \ No newline at end of file diff --git a/tools/sat-smt/metis.md b/tools/sat-smt/metis.md new file mode 100644 index 0000000..54dd4b4 --- /dev/null +++ b/tools/sat-smt/metis.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Metis' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://www.gilith.com/software/metis/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/gilith/metis", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Intel'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + +{{}} +Metis is an automatic theorem prover for first order logic with equality. \ No newline at end of file diff --git a/tools/sat-smt/metitarski.md b/tools/sat-smt/metitarski.md new file mode 100644 index 0000000..241f51a --- /dev/null +++ b/tools/sat-smt/metitarski.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'MetiTarski' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://www.cl.cam.ac.uk/~lp15/papers/Arith/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://bitbucket.org/lcpaulson/metitarski-git", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['University of Cambridge'] +developers = ['Inria'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + + +MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. \ No newline at end of file diff --git a/tools/sat-smt/princess.md b/tools/sat-smt/princess.md new file mode 100644 index 0000000..302fc13 --- /dev/null +++ b/tools/sat-smt/princess.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Princess' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "http://www.philipp.ruemmer.org/princess.shtml", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/uuverifiers/princess", icon = 'fa-solid fa-code' }, + { title = "Playground", url = "https://eldarica.org/princess/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Uppsala University'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + + +Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted predicates, written entirely in Scala. \ No newline at end of file diff --git a/tools/sat-smt/profound.md b/tools/sat-smt/profound.md new file mode 100644 index 0000000..565e4cd --- /dev/null +++ b/tools/sat-smt/profound.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Profound' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://chaudhuri.info/software/profound/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/direct-manipulation/profound", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Inria'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + +{{}} +Profound is an experiment in subformula linking as an interaction method. \ No newline at end of file diff --git a/tools/sat-smt/spass.md b/tools/sat-smt/spass.md new file mode 100644 index 0000000..ee3d9d1 --- /dev/null +++ b/tools/sat-smt/spass.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'SPASS' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover", icon = 'fa-solid fa-home' }, + # { title = "Source Code", url = "https://github.com/abella-prover/abella", icon = 'fa-solid fa-code' }, + # { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Inria'] +licenses = ['All Rights Reserved'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Why3'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + +{{}} + +SPASS: An Automated Theorem Prover for First-Order Logic with Equality \ No newline at end of file