rebuild
This commit is contained in:
599
tools/index.html
599
tools/index.html
@@ -25,7 +25,7 @@ Click a colorful item in the">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
@@ -104,6 +104,8 @@ Click a colorful item in the">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -144,6 +146,14 @@ Click a colorful item in the">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -209,7 +219,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/alt-ergo/">Alt-Ergo</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -327,7 +337,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/bitwuzla/">Bitwuzla</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -486,7 +496,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -631,6 +641,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/cadical\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/cadical/">CaDiCaL</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_sat-solver"
|
||||
style="background:rgba(197,220,18,0.4)"
|
||||
href="/applications/sat-solver">
|
||||
SAT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
@@ -642,7 +766,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/colibri/">Colibri</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -747,6 +871,85 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/prob\/comics\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
<a href="/tools/prob/comics/">COMICS</a>
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_counterexample-generator"
|
||||
style="background:rgba(142,120,129,0.4)"
|
||||
href="/applications/counterexample-generator">
|
||||
Counterexample Generator
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
@@ -760,7 +963,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/cryptominisat/">CryptoMiniSat</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -902,7 +1105,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1041,7 +1244,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/cvc5/">cvc5</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1183,7 +1386,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1282,6 +1485,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/e\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/e/">E</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv2"
|
||||
style="background:rgba(220,234,19,0.4)"
|
||||
href="/licenses/gplv2">
|
||||
GPLv2
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
@@ -1293,7 +1610,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/glucose/">Glucose</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1411,7 +1728,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/lingeling/">Lingeling</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1525,7 +1842,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/mathsat/">MathSAT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1642,7 +1959,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1756,7 +2073,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/opensmt/">OpenSMT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1874,7 +2191,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/parafrost/">ParaFROST</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2000,7 +2317,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/prob/prism/">PRISM</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2125,7 +2442,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2250,7 +2567,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2368,7 +2685,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/mc/sally/">Sally</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2486,7 +2803,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/smt-rat/">SMT-RAT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2625,7 +2942,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/smtinterpol/">SMTInterpol</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2747,7 +3064,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/prob/stamina/">STAMINA</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2886,7 +3203,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/prob/storm/">Storm</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -3008,7 +3325,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/stp/">STP</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -3153,6 +3470,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/vampire\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/vampire/">Vampire</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
@@ -3164,7 +3595,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/verit/">veriT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -3286,7 +3717,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/yices/">Yices 2</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -3425,7 +3856,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/z3/">Z3</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -3570,6 +4001,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/zipperposition\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/zipperposition/">Zipperposition</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
|
||||
@@ -25,7 +25,7 @@ Click a colorful">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
@@ -125,7 +125,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/mc/sally/">Sally</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
237
tools/prob/comics/index.html
Normal file
237
tools/prob/comics/index.html
Normal file
@@ -0,0 +1,237 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>COMICS | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="COMICS">
|
||||
<meta property="og:description" content="COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/prob/comics/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/prob/comics/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>COMICS</h1>
|
||||
|
||||
<span class="subtitle">Probabilistic Model Checker</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://ths.rwth-aachen.de/research/tools/comics/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_counterexample-generator"
|
||||
style="background:rgba(142,120,129,0.4)"
|
||||
href="/applications/counterexample-generator">
|
||||
Counterexample Generator
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_rwth-aachen"
|
||||
style="background:rgba(3,239,109,0.4)"
|
||||
href="/developers/rwth-aachen">
|
||||
RWTH Aachen
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20COMICS" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -25,7 +25,7 @@ Click a colorful">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
@@ -99,6 +99,10 @@ Click a colorful">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -127,13 +131,92 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
</thead>
|
||||
<tbody>
|
||||
|
||||
<tr onclick="window.location='\/tools\/prob\/comics\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
<a href="/tools/prob/comics/">COMICS</a>
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_counterexample-generator"
|
||||
style="background:rgba(142,120,129,0.4)"
|
||||
href="/applications/counterexample-generator">
|
||||
Counterexample Generator
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/prob\/prism\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/prob/prism/">PRISM</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -255,7 +338,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/prob/stamina/">STAMINA</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -394,7 +477,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/prob/storm/">Storm</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
@@ -8,6 +8,13 @@
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/tools/prob/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>COMICS</title>
|
||||
<link>http://localhost:1313/tools/prob/comics/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>http://localhost:1313/tools/prob/comics/</guid>
|
||||
<description><p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>PRISM</title>
|
||||
<link>http://localhost:1313/tools/prob/prism/</link>
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
550
tools/prob/storm-copy/index.html
Normal file
550
tools/prob/storm-copy/index.html
Normal file
@@ -0,0 +1,550 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Storm | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Storm">
|
||||
<meta property="og:description" content="Storm is a tool for the analysis of systems involving random or probabilistic phenomena.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/prob/storm-copy/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/prob/storm-copy/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Storm</h1>
|
||||
|
||||
<span class="subtitle">Probabilistic Model Checker</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://www.stormchecker.org/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/moves-rwth/storm" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_probabilistic-model-checker"
|
||||
style="background:rgba(232,228,128,0.4)"
|
||||
href="/applications/probabilistic-model-checker">
|
||||
Probabilistic Model Checker
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_rwth-aachen"
|
||||
style="background:rgba(3,239,109,0.4)"
|
||||
href="/developers/rwth-aachen">
|
||||
RWTH Aachen
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_galileo"
|
||||
style="background:rgba(56,14,206,0.4)"
|
||||
href="/inputs/galileo">
|
||||
Galileo
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_greatspn"
|
||||
style="background:rgba(33,116,195,0.4)"
|
||||
href="/inputs/greatspn">
|
||||
GreatSPN
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_jani"
|
||||
style="background:rgba(193,44,177,0.4)"
|
||||
href="/inputs/jani">
|
||||
JANI
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_mrmc"
|
||||
style="background:rgba(87,205,92,0.4)"
|
||||
href="/inputs/mrmc">
|
||||
MRMC
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_pnml"
|
||||
style="background:rgba(58,17,88,0.4)"
|
||||
href="/inputs/pnml">
|
||||
PNML
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_prism"
|
||||
style="background:rgba(37,96,141,0.4)"
|
||||
href="/inputs/prism">
|
||||
PRISM
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_c++"
|
||||
style="background:rgba(246,248,124,0.4)"
|
||||
href="/interfaces/c++">
|
||||
C++
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_python"
|
||||
style="background:rgba(167,245,243,0.4)"
|
||||
href="/interfaces/python">
|
||||
Python
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv3"
|
||||
style="background:rgba(182,14,173,0.4)"
|
||||
href="/licenses/gplv3">
|
||||
GPLv3
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>The probabilistic model checker Storm</strong>
|
||||
|
||||
|
||||
(2022)
|
||||
|
||||
|
||||
by Hensel, Christian et. al.
|
||||
|
||||
(589-610)
|
||||
| Appears in <em>International Journal on Software Tools for Technology Transfer</em>
|
||||
| Volume 24
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/s10009-021-00633-z" target="_blank" rel="noopener">10.1007/s10009-021-00633-z</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Storm" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -33,7 +33,7 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
327
tools/sat-smt/cadical/index.html
Normal file
327
tools/sat-smt/cadical/index.html
Normal file
@@ -0,0 +1,327 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>CaDiCaL | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="CaDiCaL">
|
||||
<meta property="og:description" content="CaDiCaL is a simplified satisfiability solver.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/cadical/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/cadical/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>CaDiCaL</h1>
|
||||
|
||||
<span class="subtitle">SAT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://github.com/arminbiere/cadical" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_sat-solver"
|
||||
style="background:rgba(197,220,18,0.4)"
|
||||
href="/applications/sat-solver">
|
||||
SAT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_university-of-freiburg"
|
||||
style="background:rgba(134,74,190,0.4)"
|
||||
href="/developers/university-of-freiburg">
|
||||
University of Freiburg
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>CaDiCaL is a simplified satisfiability solver.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20CaDiCaL" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -28,7 +28,7 @@ Python">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -33,7 +33,7 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -33,7 +33,7 @@ dReal is an automated reasoning tool. It focuses on solving problems that can be
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
329
tools/sat-smt/e-copy/index.html
Normal file
329
tools/sat-smt/e-copy/index.html
Normal file
@@ -0,0 +1,329 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>E | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="E">
|
||||
<meta property="og:description" content="E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/e-copy/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/e-copy/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>E</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/eprover/eprover" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_dhbw-stuttgart"
|
||||
style="background:rgba(88,88,124,0.4)"
|
||||
href="/developers/dhbw-stuttgart">
|
||||
DHBW Stuttgart
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv2"
|
||||
style="background:rgba(220,234,19,0.4)"
|
||||
href="/licenses/gplv2">
|
||||
GPLv2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20E" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
329
tools/sat-smt/e/index.html
Normal file
329
tools/sat-smt/e/index.html
Normal file
@@ -0,0 +1,329 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>E | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="E">
|
||||
<meta property="og:description" content="E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/e/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/e/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>E</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/eprover/eprover" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_dhbw-stuttgart"
|
||||
style="background:rgba(88,88,124,0.4)"
|
||||
href="/developers/dhbw-stuttgart">
|
||||
DHBW Stuttgart
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv2"
|
||||
style="background:rgba(220,234,19,0.4)"
|
||||
href="/licenses/gplv2">
|
||||
GPLv2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20E" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -25,7 +25,7 @@ Click a colorful">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
@@ -159,6 +159,22 @@ Click a colorful">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -209,7 +225,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/alt-ergo/">Alt-Ergo</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -327,7 +343,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/bitwuzla/">Bitwuzla</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -486,7 +502,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -631,6 +647,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/cadical\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/cadical/">CaDiCaL</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_sat-solver"
|
||||
style="background:rgba(197,220,18,0.4)"
|
||||
href="/applications/sat-solver">
|
||||
SAT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
@@ -642,7 +772,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/colibri/">Colibri</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -760,7 +890,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/cryptominisat/">CryptoMiniSat</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -902,7 +1032,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1041,7 +1171,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/cvc5/">cvc5</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1183,7 +1313,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1282,6 +1412,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/e\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/e/">E</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv2"
|
||||
style="background:rgba(220,234,19,0.4)"
|
||||
href="/licenses/gplv2">
|
||||
GPLv2
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
@@ -1293,7 +1537,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/glucose/">Glucose</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1411,7 +1655,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/lingeling/">Lingeling</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1525,7 +1769,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/mathsat/">MathSAT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1642,7 +1886,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1756,7 +2000,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/opensmt/">OpenSMT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -1874,7 +2118,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/parafrost/">ParaFROST</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2003,7 +2247,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2128,7 +2372,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(128, 28, 28);"></span>
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2246,7 +2490,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/smt-rat/">SMT-RAT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2385,7 +2629,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/smtinterpol/">SMTInterpol</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2507,7 +2751,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/stp/">STP</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2652,6 +2896,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/vampire\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/vampire/">Vampire</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
@@ -2663,7 +3021,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/verit/">veriT</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2785,7 +3143,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/yices/">Yices 2</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -2924,7 +3282,7 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
<a href="/tools/sat-smt/z3/">Z3</a>
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
@@ -3069,6 +3427,120 @@ Colors are generated by hashing each term’s name and converting it to RGB
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
</tr>
|
||||
|
||||
<tr onclick="window.location='\/tools\/sat-smt\/zipperposition\/'" style="cursor:pointer;">
|
||||
<td>
|
||||
|
||||
|
||||
<a href="/tools/sat-smt/zipperposition/">Zipperposition</a>
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</td>
|
||||
|
||||
|
||||
|
||||
@@ -29,6 +29,13 @@
|
||||
<guid>http://localhost:1313/tools/sat-smt/boolector/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span>
 
 <span style="display:none">]</span>
</div>
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>CaDiCaL</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/cadical/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>http://localhost:1313/tools/sat-smt/cadical/</guid>
|
||||
<description><p>CaDiCaL is a simplified satisfiability solver.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Colibri</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/colibri/</link>
|
||||
@@ -64,6 +71,13 @@
|
||||
<guid>http://localhost:1313/tools/sat-smt/dreal/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
 
 <span style="display:none">]</span>
</div>
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>E</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/e/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>http://localhost:1313/tools/sat-smt/e/</guid>
|
||||
<description><p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Glucose</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/glucose/</link>
|
||||
@@ -141,6 +155,13 @@
|
||||
<guid>http://localhost:1313/tools/sat-smt/stp/</guid>
|
||||
<description><p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Vampire</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/vampire/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>http://localhost:1313/tools/sat-smt/vampire/</guid>
|
||||
<description><p>Vampire is a theorem prover.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>veriT</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/verit/</link>
|
||||
@@ -162,5 +183,12 @@
|
||||
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
|
||||
<description><p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Zipperposition</title>
|
||||
<link>http://localhost:1313/tools/sat-smt/zipperposition/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>http://localhost:1313/tools/sat-smt/zipperposition/</guid>
|
||||
<description><p>Zipperposition is an automated theorem prover for first-order logic with equality and theories.</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -29,7 +29,7 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -33,7 +33,7 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -33,7 +33,7 @@ Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -33,7 +33,7 @@ Riss is a SAT solving tool collection.">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -28,7 +28,7 @@ C++ API: C++ API Reference
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -25,7 +25,7 @@ This tool is available through the following">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -27,7 +27,7 @@ C API: stp C API">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
329
tools/sat-smt/vampire-copy/index.html
Normal file
329
tools/sat-smt/vampire-copy/index.html
Normal file
@@ -0,0 +1,329 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Vampire | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Vampire">
|
||||
<meta property="og:description" content="Vampire is a theorem prover.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/vampire-copy/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/vampire-copy/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Vampire</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://vprover.github.io/index.html" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/vprover/vampire" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_tu-wien"
|
||||
style="background:rgba(98,85,62,0.4)"
|
||||
href="/developers/tu-wien">
|
||||
TU Wien
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Vampire is a theorem prover.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Vampire" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
329
tools/sat-smt/vampire/index.html
Normal file
329
tools/sat-smt/vampire/index.html
Normal file
@@ -0,0 +1,329 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Vampire | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Vampire">
|
||||
<meta property="og:description" content="Vampire is a theorem prover.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/vampire/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/vampire/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Vampire</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://vprover.github.io/index.html" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/vprover/vampire" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_tu-wien"
|
||||
style="background:rgba(98,85,62,0.4)"
|
||||
href="/developers/tu-wien">
|
||||
TU Wien
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Vampire is a theorem prover.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Vampire" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -23,7 +23,7 @@
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -27,7 +27,7 @@ C API:">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
329
tools/sat-smt/zipperposition/index.html
Normal file
329
tools/sat-smt/zipperposition/index.html
Normal file
@@ -0,0 +1,329 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&path=livereload" data-no-instant defer></script>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Zipperposition | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Zipperposition">
|
||||
<meta property="og:description" content="Zipperposition is an automated theorem prover for first-order logic with equality and theories.">
|
||||
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/zipperposition/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/zipperposition/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
|
||||
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
|
||||
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
|
||||
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
|
||||
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
|
||||
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
|
||||
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
|
||||
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
|
||||
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
|
||||
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
|
||||
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
|
||||
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
|
||||
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
|
||||
<link rel="manifest" href="/manifest.json">
|
||||
<meta name="msapplication-TileColor" content="#ffffff">
|
||||
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
|
||||
<meta name="theme-color" content="#ffffff">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<div class="banner">
|
||||
<span class="banner-text">
|
||||
🚧 This site is a work in progress. Don’t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> 🚧
|
||||
</span>
|
||||
</div>
|
||||
|
||||
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Zipperposition</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://sneeuwballen.github.io/zipperposition/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/sneeuwballen/zipperposition" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_tu-wien"
|
||||
style="background:rgba(98,85,62,0.4)"
|
||||
href="/developers/tu-wien">
|
||||
TU Wien
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Zipperposition is an automated theorem prover for first-order logic with equality and theories.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
|
||||
<div class="footer-links" style="text-align: left;">
|
||||
Help improve this page!<br/>
|
||||
Submit an
|
||||
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Zipperposition" target="_blank">issue</a> or
|
||||
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -25,7 +25,7 @@ Click a colorful">
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
|
||||
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs+wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7+qyZDkRxP19nhSx1jw==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
|
||||
@@ -6,7 +6,6 @@
|
||||
<description>Recent content in Termination Tools on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate></lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/tools/termination/index.xml" rel="self" type="application/rss+xml" />
|
||||
</channel>
|
||||
</rss>
|
||||
|
||||
Reference in New Issue
Block a user