Path: csiph.com!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock 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: References: <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 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