|
1 år sedan | |
---|---|---|
project | 1 år sedan | |
src | 1 år sedan | |
.gitignore | 1 år sedan | |
README.md | 1 år sedan | |
build.sbt | 1 år sedan |
rogram szukający dowodów w dla wyrażeń logiki pierwszego rzędu metodą tableau.
Umie na przykład dowieść, że istnieje liczba 3:
N(O) ∧ ∀i.((N(i) ⇒ N(s(i)))) ⇒ N(s(s(s(O)))),
albo, że
jeśli w barze jest ktoś, kto pije, to wszyscy w barze piją:
exists x. forall y. (Pije(x) => Pije(y)).
Jeśli chcesz zobaczyć poważną implementację, to polecam tpg, albo poczytać "Handbook of Tableau Methods" (ISBN: 978-94-017-1754-0). Kolega mówił, że ta książka jest na LibGenie, ale ja nie polecam ściągać z tamtąd książek, bo to nielegalne.
Najszybciej (wymaga SBT):
sbt run
sbt 'Docker / publishLocal'
W logach dostaniesz namiar na wybudowany obraz, n.p. localhost/tableaux:0.2.0-SNAPSHOT
.
Potem już tylko odpalić:
podman run -it --rm localhost/tableaux:0.4.0-SNAPSHOT
Możesz se wybudować zip
a z potrzebnymi jarkami i skryptem uruchomieniowym:
sbt 'show Universal / packageBin'
W logach dostaniesz namiar na plik.
Tylko dla użytkowników Graala:
sbt 'show GraalVMNativeImage / packageBin'
Tableaux
jako biblioteki w moim programieObczaj pakiet z API: pl.wojciechkarpiel.tableaux.api i przykład użycia.
Sam se musisz opublikować tę bibliotekę:
sbt publishLocal
Rozszerzam program tak, żeby wspierał logikę modalną. Tymczasowo następuje bałagan w kodzie źródłowym i spadek wydajności, ale za to już można udowadniać rzeczy typu:
∀x.□F(x) ⇒ □∀x.F(x)
◇(p ⇒ q) ⇒ □p ⇒ ◇q
◇ (możliwość) można zapisać jako <>
, a □ (konieczność) jako []
. Przykłady wziąłem
z tpg.
Jeśli chodzi o logikę modalną, to można powiedzieć, że jestem jaroszem. Jestem też koniem. Jestem mocno niepewny poprawności rozwiązania w ogólnym przypadku, robię na pałę, proszę się nie sugerować
Oprócz tego muszę zacząć sensownie prezentować drzewo dowodu, tera to tylko opowiadam że coś jest prawdą a nie mówię czemu xD