|
| 1 | +<!DOCTYPE html> |
| 2 | +<html lang="en"> |
| 3 | +<head> |
| 4 | + <meta charset="UTF-8"> |
| 5 | + <meta name="viewport" content="width=device-width, initial-scale=1.0"> |
| 6 | + <title>py-typedlogic: Bridging Formal Logic and Typed Python</title> |
| 7 | + <style> |
| 8 | + body { |
| 9 | + font-family: 'Segoe UI', Tahoma, Geneva, Verdana, sans-serif; |
| 10 | + line-height: 1.6; |
| 11 | + color: #333; |
| 12 | + max-width: 1200px; |
| 13 | + margin: 0 auto; |
| 14 | + padding: 20px; |
| 15 | + background-color: #f4f4f4; |
| 16 | + } |
| 17 | + .container { |
| 18 | + background-color: white; |
| 19 | + border-radius: 8px; |
| 20 | + box-shadow: 0 4px 6px rgba(0, 0, 0, 0.1); |
| 21 | + padding: 40px; |
| 22 | + } |
| 23 | + h1 { |
| 24 | + color: #2c3e50; |
| 25 | + text-align: center; |
| 26 | + font-size: 2.5em; |
| 27 | + margin-bottom: 20px; |
| 28 | + } |
| 29 | + .tagline { |
| 30 | + text-align: center; |
| 31 | + font-size: 1.2em; |
| 32 | + color: #34495e; |
| 33 | + margin-bottom: 40px; |
| 34 | + } |
| 35 | + .features { |
| 36 | + display: flex; |
| 37 | + justify-content: space-around; |
| 38 | + flex-wrap: wrap; |
| 39 | + margin-bottom: 40px; |
| 40 | + } |
| 41 | + .feature { |
| 42 | + flex-basis: 30%; |
| 43 | + text-align: center; |
| 44 | + margin-bottom: 20px; |
| 45 | + } |
| 46 | + .feature h3 { |
| 47 | + color: #3498db; |
| 48 | + } |
| 49 | + .code-tabs { |
| 50 | + margin-top: 20px; |
| 51 | + } |
| 52 | + .tab-buttons { |
| 53 | + display: flex; |
| 54 | + border-bottom: 2px solid #3498db; |
| 55 | + } |
| 56 | + .tab-button { |
| 57 | + background-color: #f8f8f8; |
| 58 | + border: none; |
| 59 | + outline: none; |
| 60 | + cursor: pointer; |
| 61 | + padding: 10px 20px; |
| 62 | + transition: 0.3s; |
| 63 | + font-size: 17px; |
| 64 | + border-top-left-radius: 5px; |
| 65 | + border-top-right-radius: 5px; |
| 66 | + } |
| 67 | + .tab-button:hover { |
| 68 | + background-color: #ddd; |
| 69 | + } |
| 70 | + .tab-button.active { |
| 71 | + background-color: #3498db; |
| 72 | + color: white; |
| 73 | + } |
| 74 | + .code-sample { |
| 75 | + display: none; |
| 76 | + padding: 20px; |
| 77 | + border: 1px solid #ddd; |
| 78 | + border-top: none; |
| 79 | + background-color: #f8f8f8; |
| 80 | + } |
| 81 | + .code-sample.active { |
| 82 | + display: block; |
| 83 | + } |
| 84 | + pre { |
| 85 | + margin: 0; |
| 86 | + white-space: pre-wrap; |
| 87 | + word-wrap: break-word; |
| 88 | + } |
| 89 | + code { |
| 90 | + font-family: 'Courier New', Courier, monospace; |
| 91 | + } |
| 92 | + .cta { |
| 93 | + text-align: center; |
| 94 | + margin-top: 40px; |
| 95 | + } |
| 96 | + .button { |
| 97 | + display: inline-block; |
| 98 | + background-color: #3498db; |
| 99 | + color: white; |
| 100 | + padding: 10px 20px; |
| 101 | + text-decoration: none; |
| 102 | + border-radius: 5px; |
| 103 | + font-weight: bold; |
| 104 | + transition: background-color 0.3s ease; |
| 105 | + } |
| 106 | + .button:hover { |
| 107 | + background-color: #2980b9; |
| 108 | + } |
| 109 | + </style> |
| 110 | +</head> |
| 111 | +<body> |
| 112 | + <div class="container"> |
| 113 | + <h1>py-typedlogic</h1> |
| 114 | + <p class="tagline">Bridging Logic and Python</p> |
| 115 | + |
| 116 | + <div class="features"> |
| 117 | + <div class="feature"> |
| 118 | + <h3>Python Syntax</h3> |
| 119 | + <p>Write logical axioms using <a href="https://py-typedlogic.github.io/py-typedlogic/tutorial/01-first-program/">familiar Python constructs</a></p> |
| 120 | + </div> |
| 121 | + <div class="feature"> |
| 122 | + <h3>Strong Typing</h3> |
| 123 | + <p>Benefit from mypy validation and catch errors early</p> |
| 124 | + </div> |
| 125 | + <div class="feature"> |
| 126 | + <h3>Integrations</h3> |
| 127 | + <p>Integration |
| 128 | + with <a href="https://py-typedlogic.github.io/py-typedlogic/integrations/solvers/souffle/">datalog |
| 129 | + engines</a>, <a href="https://py-typedlogic.github.io/py-typedlogic/integrations/solvers/clingo/">answer-set |
| 130 | + programming</a>, <a href="https://py-typedlogic.github.io/py-typedlogic/integrations/solvers/z3/">theorem |
| 131 | + provers</a>, and <a href="https://py-typedlogic.github.io/py-typedlogic/integrations/frameworks/owldl/owldl-tutorial/">OWL-DL</a></p> |
| 132 | + </div> |
| 133 | + </div> |
| 134 | + |
| 135 | + <h2>See py-typedlogic in Action</h2> |
| 136 | + <div class="code-tabs"> |
| 137 | + <div class="tab-buttons"> |
| 138 | + <button class="tab-button active" |
| 139 | + onclick="openTab(event, 'python-logic')">Python Theory</button> |
| 140 | + <button class="tab-button" onclick="openTab(event, 'execution')">Reasoning</button> |
| 141 | + <button class="tab-button" onclick="openTab(event, 'output')">Output</button> |
| 142 | + <button class="tab-button" onclick="openTab(event, 'axioms')">Axioms</button> |
| 143 | + </div> |
| 144 | + |
| 145 | + <div id="python-logic" class="code-sample active"> |
| 146 | + <pre><code>from pydantic import BaseModel |
| 147 | +from typedlogic import FactMixin, Term |
| 148 | +from typedlogic.decorators import axiom |
| 149 | + |
| 150 | +ID = str |
| 151 | + |
| 152 | +class Link(BaseModel, FactMixin): |
| 153 | + """A link between two entities""" |
| 154 | + source: ID |
| 155 | + target: ID |
| 156 | + |
| 157 | +class Path(BaseModel, FactMixin): |
| 158 | + """An N-hop path between two entities""" |
| 159 | + source: ID |
| 160 | + target: ID |
| 161 | + hops: int |
| 162 | + |
| 163 | +@axiom |
| 164 | +def path_from_link(x: ID, y: ID): |
| 165 | + """If there is a link from x to y, there is a path from x to y""" |
| 166 | + assert Link(source=x, target=y) >> Path(source=x, target=y, hops=1) |
| 167 | + |
| 168 | +@axiom |
| 169 | +def transitivity(x: ID, y: ID, z: ID, d1: int, d2: int): |
| 170 | + """Transitivity of paths, plus hop counting""" |
| 171 | + assert ((Path(source=x, target=y, hops=d1) & Path(source=y, target=z, hops=d2)) >> |
| 172 | + Path(source=x, target=z, hops=d1+d2))</code></pre> |
| 173 | + </div> |
| 174 | + |
| 175 | + <div id="execution" class="code-sample"> |
| 176 | + <pre><code>from typedlogic.integrations.souffle_solver import SouffleSolver |
| 177 | +from links import Link |
| 178 | +import links as links |
| 179 | + |
| 180 | +solver = SouffleSolver() |
| 181 | +solver.load(links) ## source for definitions and axioms |
| 182 | +# Add data |
| 183 | +links = [Link(source='CA', target='OR'), Link(source='OR', target='WA')] |
| 184 | +for link in links: |
| 185 | + solver.add(link) |
| 186 | +model = solver.model() |
| 187 | +for fact in model.iter_retrieve("Path"): |
| 188 | + print(fact)</code></pre> |
| 189 | + </div> |
| 190 | + |
| 191 | + <div id="output" class="code-sample"> |
| 192 | + <pre><code>Path(source='CA', target='OR', hops=1) |
| 193 | +Path(source='OR', target='WA', hops=1) |
| 194 | +Path(source='CA', target='WA', hops=2)</code></pre> |
| 195 | + </div> |
| 196 | + |
| 197 | + <div id="axioms" class="code-sample"> |
| 198 | + <pre><code>∀[x:ID y:ID]. Link(x, y) → Path(x, y, 1) |
| 199 | +∀[x:ID y:ID z:ID d1:int d2:int]. Path(x, y, d1) ∧ Path(y, z, d2) → Path(x, z, d1+d2) |
| 200 | +</code></pre> |
| 201 | + </div> |
| 202 | + </div> |
| 203 | + |
| 204 | + <div class="cta"> |
| 205 | + <a href="https://py-typedlogic.github.io/py-typedlogic/" class="button">Get Started with py-typedlogic</a> |
| 206 | + </div> |
| 207 | + </div> |
| 208 | + |
| 209 | + <script> |
| 210 | + function openTab(evt, tabName) { |
| 211 | + var i, codeSamples, tabButtons; |
| 212 | + codeSamples = document.getElementsByClassName("code-sample"); |
| 213 | + for (i = 0; i < codeSamples.length; i++) { |
| 214 | + codeSamples[i].className = codeSamples[i].className.replace(" active", ""); |
| 215 | + } |
| 216 | + tabButtons = document.getElementsByClassName("tab-button"); |
| 217 | + for (i = 0; i < tabButtons.length; i++) { |
| 218 | + tabButtons[i].className = tabButtons[i].className.replace(" active", ""); |
| 219 | + } |
| 220 | + document.getElementById(tabName).className += " active"; |
| 221 | + evt.currentTarget.className += " active"; |
| 222 | + } |
| 223 | + </script> |
| 224 | +</body> |
| 225 | +</html> |
0 commit comments