Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.javascript > #41337 > unrolled thread
| Started by | Mild Shock <janburse@fastmail.fm> |
|---|---|
| First post | 2023-06-18 13:01 +0200 |
| Last post | 2023-07-27 18:24 +0200 |
| Articles | 6 — 3 participants |
Back to article view | Back to comp.lang.javascript
ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) Mild Shock <janburse@fastmail.fm> - 2023-06-18 13:01 +0200
Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) Mostowski Collapse <janburse@fastmail.fm> - 2023-07-06 23:04 +0200
Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) Mild Shock <bursejan@gmail.com> - 2023-07-18 08:47 -0700
Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) Mild Shock <janburse@fastmail.fm> - 2023-07-20 10:49 +0200
Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) Mild Shock <bursejan@gmail.com> - 2023-07-22 08:03 -0700
Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) Mild Shock <janburse@fastmail.fm> - 2023-07-27 18:24 +0200
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2023-06-18 13:01 +0200 |
| Subject | ANN: Dogelog Player 1.0.6 (GNU Prolog Stub) |
| Message-ID | <u6mo6t$1fmii$2@solani.org> |
Dear All,
We are happy to announce a new edition
of the Dogelog player:
- library(react):
The library(markup) library was rewritten
and some new predicates were added. All
predicates related to DOM events are now
available in a new library library(react).
Both libraries also include conveniences for SVG.
- library(json):
The library(json) library, previously
rolled out for Jekejeke Prolog, is also
available for Dogelog Player. The library
has now been extended slightly, so there
is a predicate to convert JSON terms between
atoms, and predicates to address JSON
terms which are objects.
- GNU Prolog Stub:
Libraries like library(json) can also be
used from GNU Prolog if ensure_loaded/1 is
replaced with include/1. GNU Prolog results
have been added to the benchmark and
compliance testing suites. Perhaps it will
soon be possible to compile Dogelog Player
with GNU Prolog.
Have Fun!
Jan Burse, 18.06.2023, http://www.xlog.ch/
[toc] | [next] | [standalone]
| From | Mostowski Collapse <janburse@fastmail.fm> |
|---|---|
| Date | 2023-07-06 23:04 +0200 |
| Message-ID | <u87a9i$284c6$2@solani.org> |
| In reply to | #41337 |
In this article we provide a sequel to our automated first order theorem proover. The initial version was only based on the implicational fragment of first order logic. We changed the prover to also support conjunction. The result is a new prover again written in Dogelog Player, a Prolog system for the JavaScript and Python platform. For the JavaScript platform, the prover can be run in the browser completely client side. The exact same conjunction rules can be also added to intuitionistic logic. Here in classical logic conjunction is rather redundant, since we have the dual ¬(A ∧ B) = (A ⊃ ¬B). If we would further add disjunction, we would end in bi-cartesian logic. See also: Cartesian Logic in Dogelog Player https://twitter.com/dogelogch/status/1677059262734901254 Cartesian Logic in Dogelog Player https://www.facebook.com/groups/dogelog Mild Shock wrote: > Dear All, > > We are happy to announce a new edition > of the Dogelog player: > > - library(react): > The library(markup) library was rewritten > and some new predicates were added. All > predicates related to DOM events are now > available in a new library library(react). > Both libraries also include conveniences for SVG. > > - library(json): > The library(json) library, previously > rolled out for Jekejeke Prolog, is also > available for Dogelog Player. The library > has now been extended slightly, so there > is a predicate to convert JSON terms between > atoms, and predicates to address JSON > terms which are objects. > > - GNU Prolog Stub: > Libraries like library(json) can also be > used from GNU Prolog if ensure_loaded/1 is > replaced with include/1. GNU Prolog results > have been added to the benchmark and > compliance testing suites. Perhaps it will > soon be possible to compile Dogelog Player > with GNU Prolog. > > Have Fun! > Jan Burse, 18.06.2023, http://www.xlog.ch/
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <bursejan@gmail.com> |
|---|---|
| Date | 2023-07-18 08:47 -0700 |
| Message-ID | <19ed63f4-e1da-48f9-90fc-22cb9bed8319n@googlegroups.com> |
| In reply to | #41346 |
We are currently investigating cartesian logic. To reduce the complexity of our endeavour we explored embedded implication as a means to provide a logic framework. We can show natural deduction and gentzen style proof search, as well as fitch proof rendering. We use a proof renderer that is based the rule/2 clauses for natural deduction and not by the right/2 and left/4 clauses for Gentzen style. Toying with our ~(A->B) = (A/\~B) example, we find that Gentzen style, although still non- deterministic, is 25-times faster than natural deduction. See also: Embedded Implication as a Logic Framework https://twitter.com/dogelogch/status/1681326945701593088 Embedded Implication as a Logic Framework https://www.facebook.com/groups/dogelog Mostowski Collapse schrieb am Donnerstag, 6. Juli 2023 um 23:04:58 UTC+2: > In this article we provide a sequel to our automated > first order theorem proover. The initial version > was only based on the implicational fragment of > first order logic. We changed the prover to also support > conjunction. > > The result is a new prover again written in Dogelog > Player, a Prolog system for the JavaScript and Python > platform. For the JavaScript platform, the prover can > be run in the browser completely client side. > > The exact same conjunction rules can be also added > to intuitionistic logic. Here in classical logic > conjunction is rather redundant, since we have the > dual ¬(A ∧ B) = (A ⊃ ¬B). If we would further add > disjunction, we would end in bi-cartesian logic. > > See also: > > Cartesian Logic in Dogelog Player > https://twitter.com/dogelogch/status/1677059262734901254 > > Cartesian Logic in Dogelog Player > https://www.facebook.com/groups/dogelog > Mild Shock wrote: > > Dear All, > > > > We are happy to announce a new edition > > of the Dogelog player: > > > > - library(react): > > The library(markup) library was rewritten > > and some new predicates were added. All > > predicates related to DOM events are now > > available in a new library library(react). > > Both libraries also include conveniences for SVG. > > > > - library(json): > > The library(json) library, previously > > rolled out for Jekejeke Prolog, is also > > available for Dogelog Player. The library > > has now been extended slightly, so there > > is a predicate to convert JSON terms between > > atoms, and predicates to address JSON > > terms which are objects. > > > > - GNU Prolog Stub: > > Libraries like library(json) can also be > > used from GNU Prolog if ensure_loaded/1 is > > replaced with include/1. GNU Prolog results > > have been added to the benchmark and > > compliance testing suites. Perhaps it will > > soon be possible to compile Dogelog Player > > with GNU Prolog. > > > > Have Fun! > > Jan Burse, 18.06.2023, http://www.xlog.ch/
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2023-07-20 10:49 +0200 |
| Message-ID | <u9ase8$3ce7$2@solani.org> |
| In reply to | #41366 |
Now that we have a logic framework for propositional logics, we use it to explore genuine negation in cartesian logic. So far we use ~A = A -> f as an abbrevation, so ~A was replaced before starting the proof search. Now we present a cartesian logic that has genuinly formulas of the form ~A. We use a notation change idea burried in Johansson Ingebrigts Minimal Logic Paper from 1937. Further the logic framework was extended by a generic usage analysis. Our ~(A=>B) = A/\~B duality investigation could be replicated with the new genuine negation. See also: Genuine Negation in Cartesian Logic https://twitter.com/dogelogch/status/1681701492435058695 Genuine Negation in Cartesian Logic https://www.facebook.com/groups/dogelog Mild Shock schrieb: > > We are currently investigating cartesian logic. To > reduce the complexity of our endeavour we explored > embedded implication as a means to provide a logic > framework. We can show natural deduction and gentzen > style proof search, as well as fitch proof rendering. > > We use a proof renderer that is based the rule/2 clauses > for natural deduction and not by the right/2 and left/4 > clauses for Gentzen style. Toying with our ~(A->B) = (A/\~B) > example, we find that Gentzen style, although still non- > deterministic, is 25-times faster than natural deduction. > > See also: > > Embedded Implication as a Logic Framework > https://twitter.com/dogelogch/status/1681326945701593088 > > Embedded Implication as a Logic Framework > https://www.facebook.com/groups/dogelog
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <bursejan@gmail.com> |
|---|---|
| Date | 2023-07-22 08:03 -0700 |
| Message-ID | <a511e068-f963-41b8-b224-2860603da942n@googlegroups.com> |
| In reply to | #41367 |
We recently introduce a Prolog logic framework based on extended Clauses that provide embedded implication. We could also demonstrate minimal and classical cartesian logic with it. As a GUI improvement, you have to put down your rose coloured glasses to see the proof terms. When desired we can now let the logic framework show proof terms in color red besides the types in color blue. A classical proof is seen in that the Felleisen C operator appears. As an exercise we investigate a claim by Ingebrigt Johansson that falsum is dispensable. See also: Wadler Glasses for Mathematical Logic https://twitter.com/dogelogch/status/1682756064020758530 Wadler Glasses for Mathematical Logic https://www.facebook.com/groups/dogelog Mild Shock schrieb am Donnerstag, 20. Juli 2023 um 10:49:21 UTC+2: > Now that we have a logic framework for propositional > logics, we use it to explore genuine negation in > cartesian logic. So far we use ~A = A -> f as an > abbrevation, so ~A was replaced before starting > the proof search. Now we present a cartesian logic > that has genuinly formulas of the form ~A. > > We use a notation change idea burried in Johansson > Ingebrigts Minimal Logic Paper from 1937. Further > the logic framework was extended by a generic > usage analysis. Our ~(A=>B) = A/\~B duality > investigation could be replicated with the > new genuine negation. > > See also: > > Genuine Negation in Cartesian Logic > https://twitter.com/dogelogch/status/1681701492435058695 > > Genuine Negation in Cartesian Logic > https://www.facebook.com/groups/dogelog > > Mild Shock schrieb: > > > > We are currently investigating cartesian logic. To > > reduce the complexity of our endeavour we explored > > embedded implication as a means to provide a logic > > framework. We can show natural deduction and gentzen > > style proof search, as well as fitch proof rendering. > > > > We use a proof renderer that is based the rule/2 clauses > > for natural deduction and not by the right/2 and left/4 > > clauses for Gentzen style. Toying with our ~(A->B) = (A/\~B) > > example, we find that Gentzen style, although still non- > > deterministic, is 25-times faster than natural deduction. > > > > See also: > > > > Embedded Implication as a Logic Framework > > https://twitter.com/dogelogch/status/1681326945701593088 > > > > Embedded Implication as a Logic Framework > > https://www.facebook.com/groups/dogelog
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2023-07-27 18:24 +0200 |
| Message-ID | <u9u5nj$da9s$3@solani.org> |
| In reply to | #41368 |
Dogelog Player is a Prolog system that targets the JavaScript and the Python platform. We extended the core system by a machanism for multilingual strings. As a use case we show a first take on the internationalization of the Dogelog Player error messages. Instead of a spider web of DCG calls we went for a flat structure that only retrieves strings. To allow localization we gave Dogelog Player the Prolog flag sys_locale. We could already execute a proof of concept and plan to make it the infrastructure of formerly Jekejeke Prolog as well. See also: Multilingual Strings in Dogelog Player https://twitter.com/dogelogch/status/1684598906582073345 Multilingual Strings in Dogelog Player https://www.facebook.com/groups/dogelog
[toc] | [prev] | [standalone]
Back to top | Article view | comp.lang.javascript
csiph-web