Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub)

Path	csiph.com!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.javascript
Subject	Re: ANN: Dogelog Player 1.0.6 (GNU Prolog Stub)
Date	Thu, 20 Jul 2023 10:49:12 +0200
Message-ID	<u9ase8$3ce7$2@solani.org> (permalink)
References	<u6mo6t$1fmii$2@solani.org> <u87a9i$284c6$2@solani.org> <19ed63f4-e1da-48f9-90fc-22cb9bed8319n@googlegroups.com>
Mime-Version	1.0
Content-Type	text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding	7bit
Injection-Date	Thu, 20 Jul 2023 08:49:12 -0000 (UTC)
Injection-Info	solani.org; logging-data="111047"; mail-complaints-to="abuse@news.solani.org"
User-Agent	Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.16
Cancel-Lock	sha1:Ms+HT1O/1nlwd5WFrPBM+3VjphA=
In-Reply-To	<19ed63f4-e1da-48f9-90fc-22cb9bed8319n@googlegroups.com>
X-User-ID	eJwFwQkBACAIBLBKvAfEUZD+EdxcwegwOMzXl6026UE7rjwpkbLYmHMye25ha+I6izYpgSW1AmlvRkDkH0BFFIc=
Xref	csiph.com comp.lang.javascript:41367

Show key headers only | View raw

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

Thread

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

csiph-web